Skip to content

Commit dc5e09b

Browse files
feliperodrifeliperodri
committed
CONTRACTS: Updates log message for requires clause
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 6a3ef0a commit dc5e09b

File tree

14 files changed

+17
-17
lines changed

14 files changed

+17
-17
lines changed

‎regression/contracts/assigns-replace-ignored-return-value/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
4-
^\[bar.precondition.\d+\] line \d+ Check bar's requires clause in foo: SUCCESS$
5-
^\[baz.precondition.\d+\] line \d+ Check baz's requires clause in foo: SUCCESS$
4+
^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
5+
^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
66
^EXIT=0$
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$

‎regression/contracts/assigns-replace-malloc-zero/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
4-
^\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS$
4+
^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$

‎regression/contracts/history-pointer-replace-04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS$
6+
^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
77
^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
88
^VERIFICATION FAILED$
99
--

‎regression/contracts/quantifiers-exists-both-replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts/quantifiers-exists-requires-replace/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--replace-call-with-contract f1 --replace-call-with-contract f2
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
7-
^\[f2.precondition.\d+\] line \d+ Check f2's requires clause in main: FAILURE$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
7+
^\[f2.precondition.\d+\] line \d+ Check requires clause of f2 in main: FAILURE$
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎regression/contracts/quantifiers-forall-both-replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts/quantifiers-forall-requires-replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts/test_aliasing_replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: FAILURE
6+
\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE
77
\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
88
^VERIFICATION FAILED$
99
--

‎regression/contracts/test_array_memory_replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS
6+
\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS
77
\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
88
\[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
99
^VERIFICATION SUCCESSFUL$

‎regression/contracts/test_array_memory_too_small_replace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--replace-call-with-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: FAILURE
6+
\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE
77
\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
88
^VERIFICATION FAILED$
99
--

0 commit comments

Comments
 (0)