Skip to content

Commit 345f4bf

Browse files
tautschnigtautschnig
authored
Merge pull request #6590 from tautschnig/link-library-functions
Permit initializers in library functions
2 parents a108335 + d849c8f commit 345f4bf

File tree

100 files changed

+604
-499
lines changed

Some content is hidden

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

100 files changed

+604
-499
lines changed

‎regression/cbmc-concurrency/thread_chain_cbmc1/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
typedef unsigned long thread_id_t;
1919

2020
// Internal unbounded array indexed by local thread identifiers
21-
extern __CPROVER_bool __CPROVER_threads_exited[];
21+
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
2222

2323
// A thread_chain is like a chain of threads `f, g, ...` where `f`
2424
// must terminate before `g` can start to run, and so forth.

‎regression/cbmc-concurrency/thread_chain_cbmc2/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
typedef unsigned long thread_id_t;
1919

2020
// Internal unbounded array indexed by local thread identifiers
21-
extern __CPROVER_bool __CPROVER_threads_exited[];
21+
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
2222

2323
// A thread_chain is like a chain of threads `f, g, ...` where `f`
2424
// must terminate before `g` can start to run, and so forth.

‎regression/cbmc-library/__atomic_always_lock_free-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
_Bool __atomic_always_lock_free(__CPROVER_size_t, void *);
5+
#endif
6+
37
int main()
48
{
59
assert(__atomic_always_lock_free(sizeof(int), 0));

‎regression/cbmc-library/__atomic_clear-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
void __atomic_clear(_Bool *, int);
5+
#endif
6+
37
int main()
48
{
59
_Bool n;

‎regression/cbmc-library/__atomic_is_lock_free-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
_Bool __atomic_is_lock_free(__CPROVER_size_t, void *);
5+
#endif
6+
37
int main()
48
{
59
assert(__atomic_is_lock_free(sizeof(int), 0));

‎regression/cbmc-library/__atomic_signal_fence-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
void __atomic_signal_fence(int);
5+
#endif
6+
37
int main()
48
{
59
__atomic_signal_fence(0);

‎regression/cbmc-library/__atomic_test_and_set-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
_Bool __atomic_test_and_set(void *, int);
5+
#endif
6+
37
int main()
48
{
59
char c = 0;

‎regression/cbmc-library/__atomic_thread_fence-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <assert.h>
22

3+
#ifndef __GNUC__
4+
void __atomic_thread_fence(int);
5+
#endif
6+
37
int main()
48
{
59
__atomic_thread_fence(0);

‎regression/cbmc-library/__errno_location-01/main.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
#include <assert.h>
22
#include <errno.h>
33

4-
int main()
4+
int main(int arc, char *argv[])
55
{
6-
__errno_location();
7-
assert(0);
6+
// errno expands to use of __errno_location() with glibc
7+
assert(errno == 0);
88
return 0;
99
}

‎regression/cbmc-library/__errno_location-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

‎regression/cbmc-library/_longjmp-01/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
#include <setjmp.h>
22

3+
#ifndef __GNUC__
4+
# define _longjmp(a, b) longjmp(a, b)
5+
#endif
6+
37
static jmp_buf env;
48

59
int main()

‎regression/cbmc-library/_longjmp-01/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--pointer-check --bounds-check
4-
^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
5-
^\[main.assertion.1\] line 8 unreachable: SUCCESS$
4+
^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$
5+
^\[main.assertion.1\] line 12 unreachable: SUCCESS$
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/cbmc-library/alloca-02/main.c

+5
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,14 @@
44
void *alloca(size_t alloca_size);
55
#endif
66

7+
// intentionally type conflicting: the built-in library uses const void*; this
8+
// is to check that object type updates are performed
9+
extern const char *__CPROVER_alloca_object;
10+
711
int *foo()
812
{
913
int *foo_ptr = alloca(sizeof(int));
14+
__CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
1015
return foo_ptr;
1116
}
1217

‎regression/cbmc-library/alloca-02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--pointer-check
44
dereference failure: dead object in \*from_foo: FAILURE$
5-
^\*\* 1 of 6 failed
5+
^\*\* 2 of 7 failed
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/cbmc-library/memcpy-07/main.c

+1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
// #include <string.h> intentionally omitted
2+
void *memcpy();
23

34
struct c
45
{

‎regression/cbmc/String_Abstraction17/strcpy-no-decl.c

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
void *malloc(unsigned);
1+
#include <stdlib.h>
2+
// string.h intentionally omitted
23

34
char *make_str()
45
{

‎regression/cbmc/String_Abstraction17/test.desc

+6-4
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
CORE
22
strcpy-no-decl.c
33
--string-abstraction --validate-goto-model
4-
Condition: strlen type inconsistency
5-
^EXIT=(127|134)$
4+
^EXIT=10$
65
^SIGNAL=0$
76
--
87
^warning: ignoring
98
--
10-
While this test currently passes when omitting --validate-goto-model, we should
11-
expect a report of type inconsistencies as no forward declarations are present.
9+
The linker is able to fix up type inconsistencies of the missing function
10+
declarations, but the absence of a declaration of strlen results in not picking
11+
up the library model. Consequently the assumption does not work as intended, and
12+
verification fails. Adding #include <string.h> makes verification pass as
13+
expected.

‎regression/cbmc/array_of_bool_as_bitvec/main.c

+1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
#include <stdlib.h>
44

55
__CPROVER_bool w[8];
6+
__CPROVER_bool v[__CPROVER_constant_infinity_uint];
67

78
void main()
89
{

‎regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE broken-smt-backend
22
main.c
33
--smt2 --outfile -
4-
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
5-
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
6-
\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
4+
\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
5+
\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
6+
\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
77
^EXIT=0$
88
^SIGNAL=0$
99
--
10-
\(= \(select array_of\.2 i\) false\)
11-
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
12-
\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
10+
\(= \(select array_of\.0 i\) false\)
11+
\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
12+
\(= \(select array\.1 \(_ bv\d+ 64\)\) false\)
1313
--
1414
This test checks for correctness of BitVec-array encoding of Boolean arrays.
1515

‎regression/cbmc/enum-trace1/main.c

+3
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,9 @@ typedef enum ENUMT
1616

1717
void test(enum ENUM e, enum_t t)
1818
{
19+
// ensure sane input values
20+
__CPROVER_assume(__CPROVER_enum_is_in_range(e));
21+
__CPROVER_assume(__CPROVER_enum_is_in_range(t));
1922
enum ENUM ee = e;
2023
enum_t tt = t;
2124

‎regression/cbmc/xml-escaping/debug_output.desc

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
⇔ false
87
\¬main\:\:1\:\:x\!0\@1\#1
98
--
109
XML does not support escaping non-printable character

‎regression/cbmc/xml-trace/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ activate-multi-line-match
77
VERIFICATION FAILED
88
<assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
99
<value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
10-
<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
10+
<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>(signed long( long)? int|int64_t)</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
1111
--
1212
^warning: ignoring
1313
--

‎regression/cprover/arrays/array1.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ array1.c
33
--text --solve --inline --no-safety
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
7-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
8-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
9-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
10-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
6+
^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
8+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
9+
^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
10+
^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
1313
^\[main\.assertion\.3\] line \d+ property 3: REFUTED$

‎regression/cprover/arrays/array2.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ array2.c
33
--text --solve --inline --no-safety
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
7-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
8-
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
6+
^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
7+
^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
8+
^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
99
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1010
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1111
--

‎regression/cprover/basic/assume1.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ assume1.c
66
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
88
^ \(\d+\) S1 = S0$
9-
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
10-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
9+
^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S11\(ς\)$
10+
^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1414
--

‎regression/cprover/basic/basic1.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ basic1.c
55
^SIGNAL=0$
66
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
8-
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
9-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
8+
^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
9+
^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
10+
^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
--

‎regression/cprover/basic/basic2.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ basic2.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7-
^\(\d+\) S19 = S18$
8-
^\(\d+\) S20 = S19$
9-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10-
^\(\d+\) S22 = S21$
11-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) S9 = S8$
8+
^\(\d+\) S10 = S9$
9+
^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
10+
^\(\d+\) S12 = S11$
11+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
--

‎regression/cprover/basic/basic3.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ basic3.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
7-
\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
8-
\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
9-
\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
10-
\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
6+
\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)
7+
\(\d+\) ∀ ς : state \. S8\(ς\) ⇒ S9\(ς\[❝y❞:=0\]\)
8+
\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=1\]\)
9+
\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝y❞:=2\]\)
10+
\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
--

‎regression/cprover/basic/basic4.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ basic4.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
8-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
9-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
8+
^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=2\]\)$
9+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1010
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
1111
--

‎regression/cprover/basic/basic5.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ basic5.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
8-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10-
^\(\d+\) S25 = S24$
11-
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
6+
^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
8+
^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9+
^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10+
^\(\d+\) S15 = S14$
11+
^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1414
--

‎regression/cprover/basic/basic6.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ basic6.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
7-
^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
8-
^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
9-
^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
10-
^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
11-
^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
6+
^\(13\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
7+
^\(14\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
8+
^\(15\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
9+
^\(16\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
10+
^\(17\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
11+
^\(18\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
--

‎regression/cprover/basic/nondet1.desc

+7-7
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ nondet1.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
7-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8-
^\(\d+\) S23 = S22$
9-
^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
10-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11-
^\(\d+\) S25 = S24$
12-
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
6+
^\(\d+\) ∀ ς : state, nondet::S12-0 : signedbv\[32\] \. S11\(ς\) ⇒ S12\(ς\[❝main::1::x❞:=nondet::S12-0\]\)$
7+
^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8+
^\(\d+\) S13 = S12$
9+
^\(\d+\) ∀ ς : state, nondet::S14-0 : signedbv\[32\] \. S13\(ς\) ⇒ S14\(ς\[❝main::1::y❞:=nondet::S14-0\]\)$
10+
^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11+
^\(\d+\) S15 = S14$
12+
^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S16\(ς\[❝return'❞:=0\]\)$
1313
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
1414
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1515
--

0 commit comments

Comments
 (0)