Merge pull request #7159 from feliperodri/breakdown-requires-ensures

CONTRACTS: Avoid single conjunction in contracts instrumentation

Author: feliperodri

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

@@ -1,6 +1,8 @@
 CORE
 main.c
 --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
+^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,6 +1,7 @@
 CORE
 main.c
 --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$

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

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
 ^VERIFICATION FAILED$
 --

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

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -3,8 +3,8 @@ main.c
 --replace-call-with-contract f1 --replace-call-with-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
-^\[f2.precondition.\d+\] line \d+ Check requires clause: FAILURE$
+^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
+^\[f2.precondition.\d+\] line \d+ Check requires clause of f2 in main: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

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

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause of f1 in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/test_aliasing_replace/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION FAILED$
 --

regression/contracts/test_array_memory_replace/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
 ^VERIFICATION SUCCESSFUL$

regression/contracts/test_array_memory_too_small_replace/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION FAILED$
 --