replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Modified tests to pass without using grep 

Now directly test individual lines with perls regex matching rather than
calling out to grep. Some changes were required:

- escape (,  ) if we want to match them
- unescape (, ) if we want to use them as regex bracket groups
- escape +, $ if we want to use them as actual characters
- unescape + to use as a regex +
This commit is contained in:
thk123 2017-02-14 11:00:42 +00:00
parent ebe4a7fe54
commit 9b052c200f
213 changed files with 306 additions and 306 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
regression/ansi-c/struct6/test.desc
View File

@ -1,7 +1,7 @@
CORE
main.c
^EXIT=\(64\|1\)$
^EXIT=(64|1)$
^SIGNAL=0$
^main.c:2:1: error: incomplete type not permitted here$
^CONVERSION ERROR$

2
regression/ansi-c/struct7/test.desc
View File

@ -1,7 +1,7 @@
CORE
main.c
^EXIT=\(64\|1\)$
^EXIT=(64|1)$
^SIGNAL=0$
^main.c:4:1: error: duplicate member .*$
^CONVERSION ERROR$

2
regression/cbmc-concurrency/constant_prop1/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
^Generated 1 VCC(s), 0 remaining after simplification$
^Generated 1 VCC\(s\), 0 remaining after simplification$
--
^warning: ignoring

2
regression/cbmc-concurrency/pthread_join1/test.desc
View File

@ -5,6 +5,6 @@ main.c
^SIGNAL=0$
^\[main\.assertion\.1\] assertion i==1: FAILURE$
^\[main\.assertion\.2\] assertion i==2: SUCCESS$
^\*\* 1 of 2 failed (2 iterations)$
^\*\* 1 of 2 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc-cover/branch3/test.desc
View File

@ -3,6 +3,6 @@ main.c
--cover branch --unwind 6
^EXIT=0$
^SIGNAL=0$
^\*\* 23 of 23 covered (100.0%)$
^\*\* 23 of 23 covered \(100.0%\)$
--
^warning: ignoring

2
regression/cbmc-cover/branch4/test.desc
View File

@ -3,6 +3,6 @@ main.c
--cover branch
^EXIT=0$
^SIGNAL=0$
^\*\* 1 of 1 covered (100.0%)$
^\*\* 1 of 1 covered \(100.0%\)$
--
^warning: ignoring

2
regression/cbmc-cover/condition1/test.desc
View File

@ -13,6 +13,6 @@ main.c
^\[main.coverage.8] file main.c line 14 function main condition .* true: SATISFIED
^\[main.coverage.9] file main.c line 16 function main condition .* false: FAILED
^\[main.coverage.10] file main.c line 16 function main condition .* true: SATISFIED
^\*\* 9 of 10 covered (90.0%)
^\*\* 9 of 10 covered \(90.0%\)
--
^warning: ignoring

2
regression/cbmc-cover/cover1/test.desc
View File

@ -6,6 +6,6 @@ main.c
^\[main.coverage.1] file main.c line 8 function main condition .*: SATISFIED$
^\[main.coverage.2] file main.c line 9 function main condition .*: SATISFIED$
^\[main.coverage.3] file main.c line 13 function main condition .*: FAILED$
^\*\* 2 of 3 covered (66.7%)$
^\*\* 2 of 3 covered \(66.7%\)$
--
^warning: ignoring

2
regression/cbmc-cover/decision1/test.desc
View File

@ -3,6 +3,6 @@ main.c
--cover decision
^EXIT=0$
^SIGNAL=0$
^\*\* 2 of 2 covered (100.0%)$
^\*\* 2 of 2 covered \(100.0%\)$
--
^warning: ignoring

2
regression/cbmc-cover/location1/test.desc
View File

@ -8,6 +8,6 @@ main.c
^\[main.coverage.3\] file main.c line 13 function main block 3: SATISFIED$
^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
^\*\* 4 of 5 covered (80.0%)
^\*\* 4 of 5 covered \(80.0%\)
--
^warning: ignoring

2
regression/cbmc-cover/location11/test.desc
View File

@ -14,6 +14,6 @@ main.c
^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
^\*\* 6 of 11 covered (54.5%)
^\*\* 6 of 11 covered \(54.5%\)
--
^warning: ignoring

2
regression/cbmc-cover/location12/test.desc
View File

@ -10,6 +10,6 @@ main.c
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
^\*\* 5 of 7 covered (71.4%)
^\*\* 5 of 7 covered \(71.4%\)
--
^warning: ignoring

2
regression/cbmc-cover/location13/test.desc
View File

@ -13,6 +13,6 @@ main.c
^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
^\*\* 5 of 10 covered (50.0%)
^\*\* 5 of 10 covered \(50.0%\)
--
^warning: ignoring

2
regression/cbmc-cover/location14/test.desc
View File

@ -9,6 +9,6 @@ main.c
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
^\*\* 2 of 6 covered (33.3%)
^\*\* 2 of 6 covered \(33.3%\)
--
^warning: ignoring

2
regression/cbmc-cover/location15/test.desc
View File

@ -12,6 +12,6 @@ main.c
^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
^\*\* 3 of 9 covered (33.3%)
^\*\* 3 of 9 covered \(33.3%\)
--
^warning: ignoring

2
regression/cbmc-cover/location16/test.desc
View File

@ -12,6 +12,6 @@ main.c
^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
^\*\* 4 of 9 covered (44.4%)
^\*\* 4 of 9 covered \(44.4%\)
--
^warning: ignoring

2
regression/cbmc-cover/mcdc1/test.desc
View File

@ -9,7 +9,7 @@ main.c
^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 10 iterations$
--
^warning: ignoring

10
regression/cbmc-cover/mcdc10/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && !\(C != FALSE\).*: SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE.*: SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 5 iterations$
--
^warning: ignoring

12
regression/cbmc-cover/mcdc11/test.desc
View File

@ -4,12 +4,12 @@ main.c
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 6 iterations$
--
^warning: ignoring

18
regression/cbmc-cover/mcdc12/test.desc
View File

@ -4,15 +4,15 @@ main.c
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !\(F != FALSE\).*: SATISFIED$
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 10 iterations$
--
^warning: ignoring

8
regression/cbmc-cover/mcdc13/test.desc
View File

@ -4,10 +4,10 @@ main.c
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !\(C != FALSE\).* SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE.* SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE.* SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 6 iterations$
--
^warning: ignoring

2
regression/cbmc-cover/mcdc14/test.desc
View File

@ -5,7 +5,7 @@ main.c
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 2 iterations$
--
^warning: ignoring

2
regression/cbmc-cover/mcdc2/test.desc
View File

@ -7,7 +7,7 @@ main.c
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 6 iterations$
--
^warning: ignoring

8
regression/cbmc-cover/mcdc3/test.desc
View File

@ -3,10 +3,10 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!\(x > \(unsigned int\)3\) && !\(y < \(unsigned int\)5\).*: SATISFIED$
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 4 iterations$
--
^warning: ignoring

2
regression/cbmc-cover/mcdc4/test.desc
View File

@ -8,7 +8,7 @@ main.c
^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 9 iterations$
--
^warning: ignoring

2
regression/cbmc-cover/mcdc5/test.desc
View File

@ -8,7 +8,7 @@ main.c
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 9 iterations$
--
^warning: ignoring

6
regression/cbmc-cover/mcdc6/test.desc
View File

@ -3,9 +3,9 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 2 iterations$
--
^warning: ignoring

2
regression/cbmc-cover/mcdc7/test.desc
View File

@ -7,7 +7,7 @@ main.c
^\[main.coverage.2\] file main.c line 8 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 2 iterations$
--
^warning: ignoring

10
regression/cbmc-cover/mcdc8/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 6 iterations$
--
^warning: ignoring

12
regression/cbmc-cover/mcdc9/test.desc
View File

@ -3,12 +3,12 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE && A != FALSE && !\(B != FALSE\).* SATISFIED$
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\) && A != FALSE && !\(B != FALSE\).* SATISFIED$
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
^\*\* Used 8 iterations$
--
^warning: ignoring

2
regression/cbmc-java/LocalVarTable2/test.desc
View File

@ -4,4 +4,4 @@ LocalVarTable2.class
^EXIT=0$
^SIGNAL=0$
--
return_value.*(void \*)i
return_value.*\(void \*\)i

2
regression/cbmc-java/NullPointer1/test.desc
View File

@ -3,7 +3,7 @@ NullPointer1.class
--pointer-check --stop-on-fail
^EXIT=10$
^SIGNAL=0$
^ file NullPointer1.java line 16 function java::NullPointer1.main:(\[Ljava/lang/String;)V$
^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc-java/NullPointer2/test.desc
View File

@ -3,7 +3,7 @@ NullPointer2.class
--pointer-check --stop-on-fail
^EXIT=10$
^SIGNAL=0$
^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V
^ file NullPointer2.java line 9 function java::NullPointer2.main:\(\[Ljava/lang/String;\)V
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc-java/NullPointer3/test.desc
View File

@ -3,7 +3,7 @@ NullPointer3.class
--pointer-check --stop-on-fail
^EXIT=10$
^SIGNAL=0$
^ file NullPointer3.java line 5 function java::NullPointer3.main:(\[Ljava/lang/String;)V bytecode_index 1$
^ file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc-java/NullPointer4/test.desc
View File

@ -3,7 +3,7 @@ NullPointer4.class
--pointer-check --stop-on-fail
^EXIT=10$
^SIGNAL=0$
^ file NullPointer4.java line 6 function java::NullPointer4.main:(\[Ljava/lang/String;)V$
^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc-java/VarLengthArrayTrace1/test.desc
View File

@ -7,4 +7,4 @@ dynamic_3_array\[1l\]=10
--
^warning: ignoring
assignment removed
irep("(\\"nil\\")")
irep\("\(\\"nil\\"\)"\)

2
regression/cbmc-java/enum1/test.desc
View File

@ -3,6 +3,6 @@ enum1.class
--java-unwind-enum-static --unwind 3
^EXIT=10$
^SIGNAL=0$
^Unwinding loop java::enum1.<clinit>:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.<clinit>:()V bytecode_index 78 thread 0$
^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode_index 78 thread 0$
--
^warning: ignoring

4
regression/cbmc-java/jar-file1/test.desc
View File

@ -1,8 +1,8 @@
CORE
some_jar.jar
^EXIT=\(0\|6\)$
^EXIT=(0|6)$
^SIGNAL=0$
^\(VERIFICATION SUCCESSFUL\|No support for reading JAR files\)$
^(VERIFICATION SUCCESSFUL|No support for reading JAR files)$
--
^warning: ignoring

4
regression/cbmc-java/jar-file2/test.desc
View File

@ -1,8 +1,8 @@
CORE
jar-file2.jar
--main-class some_class
^EXIT=\(10\|6\)$
^EXIT=(10|6)$
^SIGNAL=0$
^\(VERIFICATION FAILED\|No support for reading JAR files\)$
^(VERIFICATION FAILED|No support for reading JAR files)$
--
^warning: ignoring

4
regression/cbmc-java/jsr1/test.desc
View File

@ -4,5 +4,5 @@ edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class
^EXIT=0$
^SIGNAL=0$
--
\\"statement\\" (\\"jsr\\")
\\"statement\\" (\\"ret\\")
\\"statement\\" \(\\"jsr\\"\)
\\"statement\\" \(\\"ret\\"\)

4
regression/cbmc-java/jsr2/test.desc
View File

@ -9,5 +9,5 @@ Labels: pc9
Labels: pc12
Labels: pc13
--
\\"statement\\" (\\"jsr\\")
\\"statement\\" (\\"ret\\")
\\"statement\\" \(\\"jsr\\"\)
\\"statement\\" \(\\"ret\\"\)

4
regression/cbmc-java/package_friendly1/test.desc
View File

@ -1,8 +1,8 @@
CORE
main.class
package_friendly1.class package_friendly2.class --show-goto-functions
^main[.]main[(][)].*$
^package_friendly2[.]operation2[(][)].*$
^main[.]main[\(][\)].*$
^package_friendly2[.]operation2[\(][\)].*$
^EXIT=0$
^SIGNAL=0$
--

2
regression/cbmc-with-incr/BV_Arithmetic3/test.desc
View File

@ -3,7 +3,7 @@ main.c
^EXIT=0$
^SIGNAL=0$
\(Starting CEGAR Loop\|^Generated 1 VCC(s), 0 remaining after simplification$\)
(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

2
regression/cbmc-with-incr/Fixedbv4/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
--
^warning: ignoring

6
regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
View File

@ -3,8 +3,8 @@ main.c
--unwind-max 3 --no-unwinding-assertions --all-properties
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.1\] assertion matriz\[(signed long int)j\]\[(signed long int)k\] <= maior: OK$
^\[main\.assertion\.2\] assertion matriz\[(signed long int)0\]\[(signed long int)0\] < maior: FAILED$
^\*\* 1 of 2 failed (2 iterations)$
^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
^\*\* 1 of 2 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.2\] .*: FAILED$
^\*\* 1 of 2 failed (2 iterations)$
^\*\* 1 of 2 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
^\*\* 1 of 9 failed (2 iterations)$
^\*\* 1 of 9 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
^\*\* 1 of 9 failed (2 iterations)$
^\*\* 1 of 9 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc-with-incr/pipe1/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
^\*\* 1 of 5 failed (2 iterations)$
^\*\* 1 of 5 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc/BV_Arithmetic3/test.desc
View File

@ -3,7 +3,7 @@ main.c
^EXIT=0$
^SIGNAL=0$
\(Starting CEGAR Loop\|^Generated 1 VCC(s), 0 remaining after simplification$\)
(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

2
regression/cbmc/Fixedbv4/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
--
^warning: ignoring

6
regression/cbmc/Malloc23/test.desc
View File

@ -5,8 +5,8 @@ main.c
^SIGNAL=0$
pointer outside dynamic object bounds in \*p: FAILURE
pointer outside dynamic object bounds in \*p: FAILURE
pointer outside dynamic object bounds in p2\[(signed long int)1\]: FAILURE
pointer outside dynamic object bounds in p2\[(signed long int)0\]: FAILURE
\*\* 4 of 36 failed (3 iterations)
pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE
pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE
\*\* 4 of 36 failed \(3 iterations\)
--
^warning: ignoring

2
regression/cbmc/Multi_Dimensional_Array6/test.desc
View File

@ -5,6 +5,6 @@ main.c
^SIGNAL=0$
^\[main\.assertion\.1\] : SUCCESS$
^\[main\.assertion\.2\] : FAILURE$
^\*\* 1 of 2 failed (2 iterations)$
^\*\* 1 of 2 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc/Overflow_Addition1/test.desc
View File

@ -2,7 +2,7 @@ CORE
main.c
--signed-overflow-check
^SIGNAL=0$
^\[.*\] arithmetic overflow on signed + in .*: FAILURE$
^\[.*\] arithmetic overflow on signed \+ in .*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc/Pointer_byte_extract2/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.2\] .*: FAILURE$
^\*\* 1 of 2 failed (2 iterations)$
^\*\* 1 of 2 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc/Pointer_byte_extract5/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
array\.List dynamic object upper bound in p->List\[2\]: FAILURE
\*\* 1 of 11 failed (2 iterations)
\*\* 1 of 11 failed \(2 iterations\)
--
^warning: ignoring

2
regression/cbmc/Pointer_byte_extract8/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
^\*\* 1 of 9 failed (2 iterations)$
^\*\* 1 of 9 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cbmc/Quantifiers-assertion/test.desc
View File

@ -9,5 +9,5 @@ main.c
^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
^\*\* 2 of 6 failed (2 iterations)$
^\*\* 2 of 6 failed \(2 iterations\)$
^\VERIFICATION FAILED$

2
regression/cbmc/Quantifiers-assignment/test.desc
View File

@ -7,5 +7,5 @@ main.c
^\[main.assertion.3\] assertion z1: SUCCESS$
^\[main.assertion.4\] assertion z2: SUCCESS$
^\*\* 1 of 4 failed (2 iterations)$
^\*\* 1 of 4 failed \(2 iterations\)$
^\VERIFICATION FAILED$

2
regression/cbmc/Quantifiers-copy/test.desc
View File

@ -8,5 +8,5 @@ main.c
^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
^\*\* 0 of 5 failed (1 iteration)$
^\*\* 0 of 5 failed \(1 iteration\)$
^VERIFICATION SUCCESSFUL$

2
regression/cbmc/Quantifiers-if/test.desc
View File

@ -8,5 +8,5 @@ main.c
^\[main.assertion.4\] failure 3: FAILURE$
^\[main.assertion.5\] success 2: SUCCESS$
^\*\* 3 of 5 failed (2 iterations)$
^\*\* 3 of 5 failed \(2 iterations\)$
^\VERIFICATION FAILED$

2
regression/cbmc/Quantifiers-initialisation/test.desc
View File

@ -8,5 +8,5 @@ main.c
^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
^\*\* 0 of 5 failed (1 iteration)$
^\*\* 0 of 5 failed \(1 iteration\)$
^VERIFICATION SUCCESSFUL$

2
regression/cbmc/Quantifiers-initialisation2/test.desc
View File

@ -8,5 +8,5 @@ main.c
^\[main.assertion.4\] forall c\[\]: SUCCESS$
^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
^\*\* 1 of 5 failed (2 iterations)$
^\*\* 1 of 5 failed \(2 iterations\)$
^VERIFICATION FAILED$

2
regression/cbmc/Quantifiers-invalid-var-range/test.desc
View File

@ -3,5 +3,5 @@ main.c
^\*\* Results:$
^\*\* 0 of 1 failed (1 iteration)$
^\*\* 0 of 1 failed \(1 iteration\)$
^VERIFICATION SUCCESSFUL$

12
regression/cbmc/Quantifiers-not-exists/test.desc
View File

@ -3,11 +3,11 @@ main.c
^\*\* Results:$
^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
^\[main.assertion.2\] assertion tmp_if_expr$3: SUCCESS$
^\[main.assertion.3\] assertion tmp_if_expr$6: SUCCESS$
^\[main.assertion.4\] assertion tmp_if_expr$9: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr$12: SUCCESS$
^\[main.assertion.6\] assertion tmp_if_expr$15: SUCCESS$
^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$
^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$
^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
^\*\* 0 of 6 failed (1 iteration)$
^\*\* 0 of 6 failed \(1 iteration\)$
^\VERIFICATION SUCCESSFUL$

2
regression/cbmc/Quantifiers-not/test.desc
View File

@ -8,5 +8,5 @@ main.c
^\[main.assertion.4\] success 3: SUCCESS$
^\[main.assertion.5\] failure 2: FAILURE$
^\*\* 2 of 5 failed (2 iterations)$
^\*\* 2 of 5 failed \(2 iterations\)$
^\VERIFICATION FAILED$

4
regression/cbmc/Quantifiers-two-dimension-array/test.desc
View File

@ -6,7 +6,7 @@ main.c
^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr$3: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
^\*\* 0 of 5 failed (1 iteration)$
^\*\* 0 of 5 failed \(1 iteration\)$
^VERIFICATION SUCCESSFUL$

6
regression/cbmc/Quantifiers-type/test.desc
View File

@ -2,8 +2,8 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion tmp_if_expr$1: FAILURE$
^\[main.assertion.2\] assertion tmp_if_expr$2: SUCCESS$
^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
^\*\* 1 of 2 failed (2 iterations)$
^\*\* 1 of 2 failed \(2 iterations\)$
^\VERIFICATION FAILED$

2
regression/cbmc/null3/test.desc
View File

@ -3,7 +3,7 @@ main.c
^EXIT=0$
^SIGNAL=0$
^Generated .* VCC(s), 0 remaining after simplification$
^Generated .* VCC\(s\), 0 remaining after simplification$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

2
regression/cbmc/pipe1/test.desc
View File

@ -4,6 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
^\*\* 1 of 5 failed (2 iterations)$
^\*\* 1 of 5 failed \(2 iterations\)$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_01_19/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_02_20/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_03_21/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_04_23/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_05_24/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_06_25/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_11_33/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_17_40/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_18_41/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_19_42/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_20_43/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --danger --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

2
regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--gcc --safety --cegis-statistics --cegis-genetic
^EXIT=0$
^SIGNAL=0$
^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
--
^warning: ignoring

Some files were not shown because too many files have changed in this diff Show More