Skip to content

Commit 8c0e263

Browse files
kroeningkroening
committed
introduce cstrlen_exprt
1 parent ed9dbe4 commit 8c0e263

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+764
-78
lines changed

‎regression/cprover/basic/assume1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ assume1.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ \(\d+\) ∀ ς : state \. true ⇒ SInitial\(ς\)$
6+
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
88
^ \(\d+\) S1 = S0$
99
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$

‎regression/cprover/basic/basic1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ basic1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^ \(\d+\) ∀ ς : state \. true ⇒ SInitial\(ς\)$
6+
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
88
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
99
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$

‎regression/cprover/contracts/check_assigns3.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
void my_function1(int *parameter)
2+
__CPROVER_requires(__CPROVER_w_ok(parameter))
3+
__CPROVER_assigns(*parameter) // passes
4+
{
5+
*parameter = 10;
6+
}
7+
8+
void my_function2(int *parameter)
9+
__CPROVER_requires(__CPROVER_w_ok(parameter))
10+
__CPROVER_assigns() // fails
11+
{
12+
*parameter = 10;
13+
}
14+
15+
void my_function3(int *parameter)
16+
__CPROVER_requires(__CPROVER_w_ok(parameter))
17+
// implicit assigns clause fails
18+
{
19+
*parameter = 10;
20+
}

‎regression/cprover/contracts/check_assigns3.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
check_assigns3.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
7+
^\[my_function2\.assigns\.1\] line \d+ assigns clause: REFUTED
8+
^\[my_function3\.assigns\.1\] line \d+ assigns clause: REFUTED
9+
--

‎regression/cprover/contracts/check_assigns4.c

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
struct S
2+
{
3+
int x, y;
4+
} global;
5+
6+
void my_function1(void)
7+
__CPROVER_assigns(global) // passes
8+
{
9+
global.x = 10;
10+
global.y = 10;
11+
}
12+
13+
void my_function2(void)
14+
__CPROVER_assigns(global.x) // passes
15+
{
16+
global.x = 10;
17+
}
18+
19+
void my_function3(void)
20+
__CPROVER_assigns(global.y) // passes
21+
{
22+
global.y = 10;
23+
}
24+
25+
void my_function4(void)
26+
__CPROVER_assigns(global.y) // fails
27+
{
28+
global.x = 10;
29+
}

‎regression/cprover/contracts/check_assigns4.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
check_assigns4.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
7+
^\[my_function1\.assigns\.2\] line \d+ assigns clause: SUCCESS$
8+
^\[my_function2\.assigns\.1\] line \d+ assigns clause: SUCCESS$
9+
^\[my_function3\.assigns\.1\] line \d+ assigns clause: SUCCESS$
10+
^\[my_function4\.assigns\.1\] line \d+ assigns clause: REFUTED$
11+
--

‎regression/cprover/contracts/check_assigns5.c

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
struct S
2+
{
3+
int x, y;
4+
};
5+
6+
void my_function1(struct S *s)
7+
__CPROVER_assigns(*s) // passes
8+
{
9+
s->x = 10;
10+
s->y = 10;
11+
}
12+
13+
void my_function2(struct S *s)
14+
__CPROVER_assigns(s->x) // passes
15+
{
16+
s->x = 10;
17+
}
18+
19+
void my_function3(struct S *s)
20+
__CPROVER_assigns(s->y) // passes
21+
{
22+
s->y = 10;
23+
}
24+
25+
void my_function4(struct S *s)
26+
__CPROVER_assigns(s->y) // fails
27+
{
28+
s->x = 10;
29+
}

‎regression/cprover/contracts/check_assigns5.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
check_assigns5.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
7+
^\[my_function1\.assigns\.2\] line \d+ assigns clause: SUCCESS$
8+
^\[my_function2\.assigns\.1\] line \d+ assigns clause: SUCCESS$
9+
^\[my_function3\.assigns\.1\] line \d+ assigns clause: SUCCESS$
10+
^\[my_function4\.assigns\.1\] line \d+ assigns clause: REFUTED$
11+
--

‎regression/cprover/contracts/check_assigns6.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int global;
2+
_Bool flag;
3+
4+
void my_function1()
5+
__CPROVER_assigns(flag: global) // passes
6+
{
7+
if(flag)
8+
global = 10;
9+
}
10+
11+
void my_function2()
12+
__CPROVER_assigns(flag: global) // fails
13+
{
14+
global = 10;
15+
}

‎regression/cprover/contracts/check_assigns6.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
check_assigns6.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
7+
^\[my_function2\.assigns\.1\] line \d+ assigns clause: REFUTED$
8+
--

‎regression/cprover/contracts/check_postcondition3.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
check_postcondition3.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6+
^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$
67
^\[my_function1\.postcondition\.1\] line \d+ postcondition: SUCCESS$
8+
^\[my_function2\.assigns\.1\] line \d+ assigns clause: SUCCESS$
79
^\[my_function2\.postcondition\.1\] line \d+ postcondition: REFUTED$
810
--

‎regression/cprover/contracts/check_postcondition4.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int x, y;
2+
3+
void my_function()
4+
__CPROVER_ensures(x == 10) // passes
5+
__CPROVER_ensures(y == 20) // fails
6+
__CPROVER_assigns(x, y)
7+
{
8+
x = 10;
9+
y = 10;
10+
}

‎regression/cprover/contracts/check_postcondition4.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
check_postcondition4.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[my_function\.postcondition\.2\] line \d+ postcondition x == 10: SUCCESS$
7+
^\[my_function\.postcondition\.1\] line \d+ postcondition y == 20: REFUTED$
8+
--

‎regression/cprover/contracts/check_precondition1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ check_precondition1.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.precondition\.1\] line \d+ precondition my_function: REFUTED$
7-
^\[main\.precondition\.2\] line \d+ precondition my_function: SUCCESS$
6+
^\[main\.precondition\.1\] line \d+ my_function precondition .*: REFUTED$
7+
^\[main\.precondition\.2\] line \d+ my_function precondition .*: SUCCESS$
88
--

‎regression/cprover/contracts/check_precondition2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ check_precondition2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[caller\.precondition\.1\] line \d+ precondition callee: SUCCESS$
6+
^\[caller\.precondition\.1\] line \d+ callee precondition parameter >= 10: SUCCESS$
77
--

‎regression/cprover/contracts/nested1.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
void callee(int *p)
2+
__CPROVER_requires(__CPROVER_rw_ok(p))
3+
{
4+
}
5+
6+
void caller(int *p)
7+
__CPROVER_requires(__CPROVER_rw_ok(p))
8+
{
9+
int i;
10+
__CPROVER_assert(__CPROVER_rw_ok(p), "property 1");
11+
callee(&i);
12+
}

‎regression/cprover/contracts/nested1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
nested1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[caller\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[caller\.precondition\.1\] line \d+ callee precondition .*: SUCCESS$
8+
--

‎regression/cprover/contracts/one_function1.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
void my_function1() __CPROVER_ensures(0) // fails
2+
{
3+
}
4+
5+
void my_function2() __CPROVER_ensures(1) // passes
6+
{
7+
}

‎regression/cprover/contracts/one_function1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
one_function1.c
3+
--contract my_function2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[my_function2\.postcondition\.1\] line \d+ postcondition: SUCCESS$
7+
--
8+
^\[my_function1\.postcondition\.1\] line \d+ postcondition: REFUTED$

‎regression/cprover/contracts/recursive_function1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ recursive_function1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[recursive_function\.precondition\.1] line \d+ precondition recursive_function: SUCCESS$
6+
^\[recursive_function\.precondition\.1] line \d+ recursive_function precondition.*: SUCCESS$
77
--

‎regression/cprover/contracts/recursive_function2.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
int recursive_function()
2+
__CPROVER_ensures(__CPROVER_return_value == 10) // passes
3+
{
4+
return recursive_function();
5+
}

‎regression/cprover/contracts/recursive_function2.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
recursive_function2.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[recursive_function\.postcondition\.1] line \d+ postcondition: SUCCESS$
7+
--

‎regression/cprover/contracts/use_precondition2.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
void my_function(const int *p)
2+
__CPROVER_requires(__CPROVER_r_ok(p))
3+
__CPROVER_requires(*p >= 20)
4+
{
5+
__CPROVER_assert(*p != 0, "property 1"); // passes
6+
}

‎regression/cprover/contracts/use_precondition2.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
use_precondition2.c
3+
--safety
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[my_function\.pointer\.1\] line \d+ pointer p safe: SUCCESS$
7+
^\[my_function\.pointer\.2\] line \d+ pointer p safe: SUCCESS$
8+
^\[my_function\.assertion\.1\] line \d+ property 1: SUCCESS$
9+
--

‎regression/cprover/cstrings/strlen2.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
__CPROVER_size_t strlen(const char *);
2+
3+
int main()
4+
{
5+
strlen("foo"); // safe
6+
strlen(0); // unsafe
7+
}

‎regression/cprover/cstrings/strlen2.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
strlen2.c
3+
--safety
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main\.strlen\.1\] line \d+ strlen argument must be C string: SUCCESS$
7+
^\[main\.strlen\.2\] line \d+ strlen argument must be C string: REFUTED$
8+
--

‎regression/cprover/pointers/aliasing1.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main(void)
2+
{
3+
int *p;
4+
__CPROVER_assume(__CPROVER_rw_ok(p));
5+
6+
int i;
7+
__CPROVER_assert(__CPROVER_rw_ok(p), "property 1"); // should pass
8+
9+
p = &i; // take address of i
10+
11+
return 0;
12+
}

‎regression/cprover/pointers/aliasing1.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
aliasing1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
--

‎regression/cprover/pointers/pointer_to_local1.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
void foo(int *p) __CPROVER_requires(__CPROVER_w_ok(p))
1+
void foo(int *p) __CPROVER_requires(__CPROVER_w_ok(p)) __CPROVER_assigns(*p)
22
{
33
int i;
44

‎regression/cprover/pointers/struct_pointer6.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ struct buf {
55
int main()
66
{
77
struct buf *b;
8-
__CPROVER_assume(__CPROVER_r_ok(b));
8+
__CPROVER_assume(__CPROVER_r_ok(b)); // must not alias with x
99
__CPROVER_assume(b->len == 456);
1010

1111
__CPROVER_size_t x, *size_t_ptr = &x;

‎regression/cprover/pointers/struct_pointer6.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
struct_pointer6.c
33

44
^EXIT=0$

‎regression/cprover/safety/local_out_of_scope3.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ int main()
44
__CPROVER_assume(__CPROVER_r_ok(p));
55
{
66
int x;
7+
__CPROVER_assert(p != &x, "property 1"); // passes
78
}
8-
__CPROVER_assert(__CPROVER_r_ok(p), "property 1");
9+
__CPROVER_assert(__CPROVER_r_ok(p), "property 2"); // passes
910
}

‎regression/cprover/safety/local_out_of_scope3.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
local_out_of_scope3.c
33

4-
^EXIT=10$
4+
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.pointer\.1\] line \d+ pointer p safe: SUCCESS$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
78
--

‎regression/cprover/unions/union1.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
union U
2+
{
3+
int i;
4+
char ch;
5+
};
6+
7+
int main()
8+
{
9+
union U u;
10+
11+
u.i = 1;
12+
__CPROVER_assert(u.i==1, "property 1"); // passes
13+
14+
u.ch = 2;
15+
__CPROVER_assert(u.ch==2, "property 2"); // passes
16+
17+
return 0;
18+
}

‎regression/cprover/unions/union1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
union1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
8+
--

0 commit comments

Comments
 (0)