From eba97a0a41b03639562fea6974cb6847b717e4c5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 6 Feb 2017 11:24:00 +0000 Subject: [PATCH 1/5] Made the Perl script not using grep Includes tests for excluded lines and multi lines. Includes tests that the test runner should fail, these are set as KNOWNBUG so we can run the regressions folder. We also don't print out when grep options activated as no chance of doing by accident as very clearly different to any other syntax. The printing messes up the formatting of the output so better to not have it. Added test script to the Makefile Also ordered the tests into alphabetical orde.r --- regression/Makefile | 10 ++- regression/test-script/Makefile | 32 ++++++++ .../test-script/excluded-line/program.c | 7 ++ .../test-script/excluded-line/test.desc | 6 ++ .../failing-excluded-line/program.c | 7 ++ .../failing-excluded-line/test.desc | 9 +++ .../test-script/failing-multi-line/program.c | 7 ++ .../test-script/failing-multi-line/test.desc | 9 +++ .../test-script/failing-single-line/program.c | 7 ++ .../test-script/failing-single-line/test.desc | 8 ++ regression/test-script/multi-line/program.c | 7 ++ regression/test-script/multi-line/test.desc | 6 ++ regression/test-script/program_runner.sh | 6 ++ regression/test-script/single-line/program.c | 7 ++ regression/test-script/single-line/test.desc | 5 ++ regression/test.pl | 74 +++++++++++++------ 16 files changed, 184 insertions(+), 23 deletions(-) create mode 100644 regression/test-script/Makefile create mode 100755 regression/test-script/excluded-line/program.c create mode 100644 regression/test-script/excluded-line/test.desc create mode 100755 regression/test-script/failing-excluded-line/program.c create mode 100644 regression/test-script/failing-excluded-line/test.desc create mode 100755 regression/test-script/failing-multi-line/program.c create mode 100644 regression/test-script/failing-multi-line/test.desc create mode 100755 regression/test-script/failing-single-line/program.c create mode 100644 regression/test-script/failing-single-line/test.desc create mode 100755 regression/test-script/multi-line/program.c create mode 100644 regression/test-script/multi-line/test.desc create mode 100755 regression/test-script/program_runner.sh create mode 100755 regression/test-script/single-line/program.c create mode 100644 regression/test-script/single-line/test.desc diff --git a/regression/Makefile b/regression/Makefile index 1243ec9a468..5c59fd6e34c 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -1,5 +1,13 @@ -DIRS = ansi-c cbmc cpp goto-instrument goto-analyzer cbmc-java +DIRS = ansi-c \ + cbmc \ + cpp \ + cbmc-java \ + goto-analyzer \ + goto-instrument \ + test-script \ + # Empty last line + test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) diff --git a/regression/test-script/Makefile b/regression/test-script/Makefile new file mode 100644 index 00000000000..46057b6b710 --- /dev/null +++ b/regression/test-script/Makefile @@ -0,0 +1,32 @@ + +default: tests.log + +test: + @if ! ../test.pl -c ../program_runner.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +tests.log: + pwd + @if ! ../test.pl -c ../program_runner.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + rm -f tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + rm -f *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/excluded-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc new file mode 100644 index 00000000000..2384efe0828 --- /dev/null +++ b/regression/test-script/excluded-line/test.desc @@ -0,0 +1,6 @@ +CORE +program.c + +^Hello$ +-- +^Goodbye$ diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/failing-excluded-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc new file mode 100644 index 00000000000..36668db5a5f --- /dev/null +++ b/regression/test-script/failing-excluded-line/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +program.c + +^Hello$ +-- +^World$ +-- +This isn't really a known bug perse, instead this test should fail (since these +are tests of the test runner). diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/failing-multi-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc new file mode 100644 index 00000000000..cf4fcf3034b --- /dev/null +++ b/regression/test-script/failing-multi-line/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +program.c + +activate-multi-line-match +Hello\nAnother\nWorld +-- +-- +This isn't really a known bug perse, instead this test should fail (since these +are tests of the test runner). diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/failing-single-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc new file mode 100644 index 00000000000..604682ecbdb --- /dev/null +++ b/regression/test-script/failing-single-line/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +program.c + +^Goodbye$ +-- +-- +This isn't really a known bug perse, instead this test should fail (since these +are tests of the test runner). diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/multi-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc new file mode 100644 index 00000000000..cf9bb072880 --- /dev/null +++ b/regression/test-script/multi-line/test.desc @@ -0,0 +1,6 @@ +CORE +program.c + +activate-multi-line-match +Hello\nWorld +-- diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh new file mode 100755 index 00000000000..8e09b75f0ab --- /dev/null +++ b/regression/test-script/program_runner.sh @@ -0,0 +1,6 @@ +#!/bin/bash + +set -e + +gcc $1 -o a.out +./a.out diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c new file mode 100755 index 00000000000..882fedcc2fd --- /dev/null +++ b/regression/test-script/single-line/program.c @@ -0,0 +1,7 @@ +#include + +int main(void) { + printf("Hello\n"); + printf("World\n"); + return 0; +} diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc new file mode 100644 index 00000000000..2507fd6a412 --- /dev/null +++ b/regression/test-script/single-line/test.desc @@ -0,0 +1,5 @@ +CORE +program.c + +^Hello$ +-- diff --git a/regression/test.pl b/regression/test.pl index 066fe2a572f..01d94e1ef0e 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -4,6 +4,8 @@ use strict; use warnings; +use Cwd; + my $has_thread_pool = eval { # "http://www.cpan.org/authors/id/J/JW/JWU/Thread-Pool-Simple/Thread-Pool-Simple-0.25.tar.gz" @@ -61,13 +63,9 @@ ($$$$$) my ($name, $test, $t_level, $cmd, $ign) = @_; my ($level, $input, $options, $grep_options, @results) = load("$test"); - # If the 4th line starts with a '-' we use that line as options to pass to - # grep when matching all lines in this test - if($grep_options =~ /^-/) { - print "\nActivating perl flags: $grep_options\n"; - } - else { - # No grep options so stick this back into the results array + # If the 4th line is activate-multi-line-match we enable multi-line checks + if($grep_options ne "activate-multi-line-match") { + # No such flag, so we add it back in unshift @results, $grep_options; $grep_options = ""; } @@ -117,10 +115,43 @@ ($$$$$) $included--; } else { my $r; - $result =~ s/\\/\\\\/g; - $result =~ s/([^\\])\$/$1\\r\\\\?\$/; - system("bash", "-c", "grep $grep_options \$'$result' '$name/$output' >/dev/null"); - $r = ($included ? $? != 0 : $? == 0); + + my $dir = getcwd(); + my $abs_path = "$dir/$name/$output"; + open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!"; + + # Multi line therefore we run each check across the whole output + if($grep_options eq "activate-multi-line-match") { + local $/ = undef; + binmode $fh; + my $whole_file = <$fh>; + my $is_match = $whole_file =~ /$result/; + $r = ($included ? !$is_match : $is_match); + } + else + { + my $found_line = 0; + while(my $line = <$fh>) { + if($line =~ /$result/) { + # We've found the line, therefore if it is included we set + # the result to 0 (OK) If it is excluded, we set the result + # to 1 (FAILED) + $r = !$included; + $found_line = 1; + last; + } + } + + if($found_line == 0) { + # None of the lines matched, therefore the result is set to + # 0 (OK) if and only if the line was not meant to be included + $r = $included; + } + + } + close($fh); + + if($r) { print LOG "$result [FAILED]\n"; $failed = 1; @@ -185,7 +216,7 @@ ($$$$)
- + -- @@ -193,16 +224,15 @@ ($$$$) where - is one of CORE, THOROUGH, FUTURE or KNOWNBUG -
is a file with extension .c/.i/.gb/.cpp/.ii/.xml/.class/.jar - additional options to be passed to CMD - additional flags to be passed to grep when checking required - patterns (this is optional, if the line stats with a `-' - it will be used as grep options. Otherwise, it will be - considered part of the required patterns) - one or more lines of regualar expressions that must occur in the output - one or more lines of expressions that must not occur in output - free form text + is one of CORE, THOROUGH, FUTURE or KNOWNBUG +
is a file with extension .c/.i/.gb/.cpp/.ii/.xml/.class/.jar + additional options to be passed to CMD + The fourth line can optionally be activate-multi-line-match, if this is the + case then each of the rules will be matched over multiple lines (so can contain) + the new line symbol (\\n) inside them. + one or more lines of regualar expressions that must occur in the output + one or more lines of expressions that must not occur in output + free form text EOF exit 1; From 7cdc14100ee8da1c06dbcecbbb14903cc1c253cf Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 10 Feb 2017 12:54:06 +0000 Subject: [PATCH 2/5] If not multi line, use old grep system To ensure existing tests continue to behave consistently, we continue to use the external grep if the multi-line flag is not present. --- regression/test.pl | 34 +++++++++------------------------- 1 file changed, 9 insertions(+), 25 deletions(-) diff --git a/regression/test.pl b/regression/test.pl index 01d94e1ef0e..27e4153b027 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -116,42 +116,26 @@ ($$$$$) } else { my $r; - my $dir = getcwd(); - my $abs_path = "$dir/$name/$output"; - open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!"; - # Multi line therefore we run each check across the whole output if($grep_options eq "activate-multi-line-match") { + my $dir = getcwd(); + my $abs_path = "$dir/$name/$output"; + open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!"; + local $/ = undef; binmode $fh; my $whole_file = <$fh>; my $is_match = $whole_file =~ /$result/; $r = ($included ? !$is_match : $is_match); + close($fh); } else { - my $found_line = 0; - while(my $line = <$fh>) { - if($line =~ /$result/) { - # We've found the line, therefore if it is included we set - # the result to 0 (OK) If it is excluded, we set the result - # to 1 (FAILED) - $r = !$included; - $found_line = 1; - last; - } - } - - if($found_line == 0) { - # None of the lines matched, therefore the result is set to - # 0 (OK) if and only if the line was not meant to be included - $r = $included; - } - + $result =~ s/\\/\\\\/g; + $result =~ s/([^\\])\$/$1\\r\\\\?\$/; + system("bash", "-c", "grep \$'$result' '$name/$output' >/dev/null"); + $r = ($included ? $? != 0 : $? == 0); } - close($fh); - - if($r) { print LOG "$result [FAILED]\n"; $failed = 1; From a172ce0fe13c82869415fc00a50b13278225f6d5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 10 Feb 2017 14:54:21 +0000 Subject: [PATCH 3/5] If we run test.pl with -K we check the known bugs fail Added this step to the test-script makefile as this has behaviour that should fail the test (since it is testing the test.pl) --- regression/test-script/Makefile | 14 ++++++++++++++ regression/test.pl | 6 +++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/regression/test-script/Makefile b/regression/test-script/Makefile index 46057b6b710..ba7db5e6250 100644 --- a/regression/test-script/Makefile +++ b/regression/test-script/Makefile @@ -7,6 +7,13 @@ test: exit 1; \ fi + @echo "Testing KNOWNBUG fail" + + @if ! ../test.pl -c ../program_runner.sh -K ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + tests.log: pwd @if ! ../test.pl -c ../program_runner.sh ; then \ @@ -14,6 +21,13 @@ tests.log: exit 1; \ fi + @echo "Testing KNOWNBUG fail" + + @if ! ../test.pl -c ../program_runner.sh -K ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + show: @for dir in *; do \ if [ -d "$$dir" ]; then \ diff --git a/regression/test.pl b/regression/test.pl index 27e4153b027..bd9f38c6a13 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -149,11 +149,15 @@ ($$$$$) } } else { print LOG "Execution [SKIPPED]\n"; + return 2; } print LOG "\n"; - return $failed; + # if the test is a KNOWNBUG then the test should fail + my $should_fail = $level eq 8; + + return ($should_fail != $failed); } sub dirs() { From ebe4a7fe54be1bae78d841eb39fe0027e46bba14 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 14 Feb 2017 10:56:16 +0000 Subject: [PATCH 4/5] Revert "If not multi line, use old grep system" This reverts commit 7cdc14100ee8da1c06dbcecbbb14903cc1c253cf. --- regression/test.pl | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/regression/test.pl b/regression/test.pl index bd9f38c6a13..a2ac088d0e0 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -116,26 +116,42 @@ ($$$$$) } else { my $r; + my $dir = getcwd(); + my $abs_path = "$dir/$name/$output"; + open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!"; + # Multi line therefore we run each check across the whole output if($grep_options eq "activate-multi-line-match") { - my $dir = getcwd(); - my $abs_path = "$dir/$name/$output"; - open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!"; - local $/ = undef; binmode $fh; my $whole_file = <$fh>; my $is_match = $whole_file =~ /$result/; $r = ($included ? !$is_match : $is_match); - close($fh); } else { - $result =~ s/\\/\\\\/g; - $result =~ s/([^\\])\$/$1\\r\\\\?\$/; - system("bash", "-c", "grep \$'$result' '$name/$output' >/dev/null"); - $r = ($included ? $? != 0 : $? == 0); + my $found_line = 0; + while(my $line = <$fh>) { + if($line =~ /$result/) { + # We've found the line, therefore if it is included we set + # the result to 0 (OK) If it is excluded, we set the result + # to 1 (FAILED) + $r = !$included; + $found_line = 1; + last; + } + } + + if($found_line == 0) { + # None of the lines matched, therefore the result is set to + # 0 (OK) if and only if the line was not meant to be included + $r = $included; + } + } + close($fh); + + if($r) { print LOG "$result [FAILED]\n"; $failed = 1; From 9b052c200faeb0ebb1728ec2f728f3707066cb09 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 14 Feb 2017 11:00:42 +0000 Subject: [PATCH 5/5] 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 + --- regression/ansi-c/struct6/test.desc | 2 +- regression/ansi-c/struct7/test.desc | 2 +- .../cbmc-concurrency/constant_prop1/test.desc | 2 +- .../cbmc-concurrency/pthread_join1/test.desc | 2 +- regression/cbmc-cover/branch3/test.desc | 2 +- regression/cbmc-cover/branch4/test.desc | 2 +- regression/cbmc-cover/condition1/test.desc | 2 +- regression/cbmc-cover/cover1/test.desc | 2 +- regression/cbmc-cover/decision1/test.desc | 2 +- regression/cbmc-cover/location1/test.desc | 2 +- regression/cbmc-cover/location11/test.desc | 2 +- regression/cbmc-cover/location12/test.desc | 2 +- regression/cbmc-cover/location13/test.desc | 2 +- regression/cbmc-cover/location14/test.desc | 2 +- regression/cbmc-cover/location15/test.desc | 2 +- regression/cbmc-cover/location16/test.desc | 2 +- regression/cbmc-cover/mcdc1/test.desc | 2 +- regression/cbmc-cover/mcdc10/test.desc | 10 +++++----- regression/cbmc-cover/mcdc11/test.desc | 12 ++++++------ regression/cbmc-cover/mcdc12/test.desc | 18 +++++++++--------- regression/cbmc-cover/mcdc13/test.desc | 8 ++++---- regression/cbmc-cover/mcdc14/test.desc | 2 +- regression/cbmc-cover/mcdc2/test.desc | 2 +- regression/cbmc-cover/mcdc3/test.desc | 8 ++++---- regression/cbmc-cover/mcdc4/test.desc | 2 +- regression/cbmc-cover/mcdc5/test.desc | 2 +- regression/cbmc-cover/mcdc6/test.desc | 6 +++--- regression/cbmc-cover/mcdc7/test.desc | 2 +- regression/cbmc-cover/mcdc8/test.desc | 10 +++++----- regression/cbmc-cover/mcdc9/test.desc | 12 ++++++------ regression/cbmc-java/LocalVarTable2/test.desc | 2 +- regression/cbmc-java/NullPointer1/test.desc | 2 +- regression/cbmc-java/NullPointer2/test.desc | 2 +- regression/cbmc-java/NullPointer3/test.desc | 2 +- regression/cbmc-java/NullPointer4/test.desc | 2 +- .../cbmc-java/VarLengthArrayTrace1/test.desc | 2 +- regression/cbmc-java/enum1/test.desc | 2 +- regression/cbmc-java/jar-file1/test.desc | 4 ++-- regression/cbmc-java/jar-file2/test.desc | 4 ++-- regression/cbmc-java/jsr1/test.desc | 4 ++-- regression/cbmc-java/jsr2/test.desc | 4 ++-- .../cbmc-java/package_friendly1/test.desc | 4 ++-- .../cbmc-with-incr/BV_Arithmetic3/test.desc | 2 +- regression/cbmc-with-incr/Fixedbv4/test.desc | 2 +- .../Multi_Dimensional_Array6/test.desc | 6 +++--- .../Pointer_byte_extract2/test.desc | 2 +- .../Pointer_byte_extract5/test.desc | 2 +- .../Pointer_byte_extract8/test.desc | 2 +- regression/cbmc-with-incr/pipe1/test.desc | 2 +- regression/cbmc/BV_Arithmetic3/test.desc | 2 +- regression/cbmc/Fixedbv4/test.desc | 2 +- regression/cbmc/Malloc23/test.desc | 6 +++--- .../cbmc/Multi_Dimensional_Array6/test.desc | 2 +- regression/cbmc/Overflow_Addition1/test.desc | 2 +- .../cbmc/Pointer_byte_extract2/test.desc | 2 +- .../cbmc/Pointer_byte_extract5/test.desc | 2 +- .../cbmc/Pointer_byte_extract8/test.desc | 2 +- .../cbmc/Quantifiers-assertion/test.desc | 2 +- .../cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/Quantifiers-copy/test.desc | 2 +- regression/cbmc/Quantifiers-if/test.desc | 2 +- .../cbmc/Quantifiers-initialisation/test.desc | 2 +- .../cbmc/Quantifiers-initialisation2/test.desc | 2 +- .../Quantifiers-invalid-var-range/test.desc | 2 +- .../cbmc/Quantifiers-not-exists/test.desc | 12 ++++++------ regression/cbmc/Quantifiers-not/test.desc | 2 +- .../Quantifiers-two-dimension-array/test.desc | 4 ++-- regression/cbmc/Quantifiers-type/test.desc | 6 +++--- regression/cbmc/null3/test.desc | 2 +- regression/cbmc/pipe1/test.desc | 2 +- .../cegis_danger_benchmark_01_19/test.desc | 2 +- .../cegis_danger_benchmark_02_20/test.desc | 2 +- .../cegis_danger_benchmark_03_21/test.desc | 2 +- .../cegis_danger_benchmark_04_23/test.desc | 2 +- .../cegis_danger_benchmark_05_24/test.desc | 2 +- .../cegis_danger_benchmark_06_25/test.desc | 2 +- .../cegis_danger_benchmark_11_33/test.desc | 2 +- .../cegis_danger_benchmark_17_40/test.desc | 2 +- .../cegis_danger_benchmark_18_41/test.desc | 2 +- .../cegis_danger_benchmark_19_42/test.desc | 2 +- .../cegis_danger_benchmark_20_43/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../cegis/cegis_danger_unit_2x0/test.desc | 6 +++--- .../cegis/cegis_danger_unit_full1/test.desc | 6 +++--- .../cegis/cegis_danger_unit_full2/test.desc | 12 ++++++------ .../cegis_danger_unit_no_ranking/test.desc | 2 +- .../cegis_danger_unit_ranking_and_x0/test.desc | 4 ++-- .../cegis/cegis_danger_unit_x0_only/test.desc | 4 ++-- .../cegis/cegis_jsa_benchmark_00/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_01/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_02/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_03/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_04/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_05/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_06/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_07/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_08/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_09/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_10/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_11/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_12/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_13/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_14/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_15/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_16/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_17/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_18/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_18_02/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_19/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_20/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_21/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_22/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_23/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_24/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_25/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_26/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_27/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_28/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_29/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_30/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_31/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_32/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_33/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_34/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_35/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_36/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_37/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_38/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_39/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_40/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_41/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_42/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_43/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_44/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_45/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_46/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_47/test.desc | 2 +- .../cegis/cegis_jsa_benchmark_48/test.desc | 2 +- regression/cegis/cegis_jsa_filter_01/test.desc | 2 +- regression/cegis/cegis_jsa_map_01/test.desc | 2 +- .../cegis_safety_unit_greater_two/test.desc | 4 ++-- .../cegis/cegis_safety_unit_true/test.desc | 4 ++-- .../cegis/cegis_safety_unit_true2/test.desc | 4 ++-- regression/cpp-linter/throw/test.desc | 2 +- regression/cpp/Address_of_Method2/test.desc | 2 +- regression/cpp/Address_of_Method3/test.desc | 2 +- regression/cpp/Constant2/test.desc | 2 +- regression/cpp/Constant3/test.desc | 2 +- regression/cpp/Pointer_Conversion1/test.desc | 2 +- regression/cpp/Resolver12/test.desc | 2 +- regression/cpp/Resolver4/test.desc | 2 +- regression/cpp/union3/test.desc | 2 +- regression/cpp/union4/test.desc | 2 +- regression/cpp/union5/test.desc | 2 +- .../goto-instrument/data-flow1/test.desc | 2 +- regression/goto-instrument/inline_01/test.desc | 6 +++--- regression/goto-instrument/inline_02/test.desc | 6 +++--- regression/goto-instrument/inline_03/test.desc | 6 +++--- regression/goto-instrument/inline_04/test.desc | 8 ++++---- regression/goto-instrument/inline_11/test.desc | 2 +- regression/strings/test3/test.desc | 8 ++++---- regression/strings/test_char_set/test.desc | 4 ++-- regression/strings/test_concat/test.desc | 2 +- regression/strings/test_contains/test.desc | 6 +++--- regression/strings/test_equal/test.desc | 4 ++-- regression/strings/test_int/test.desc | 6 +++--- regression/strings/test_pass1/test.desc | 6 +++--- regression/strings/test_pass_pc3/test.desc | 4 ++-- regression/strings/test_substring/test.desc | 8 ++++---- regression/strings/test_suffix/test.desc | 4 ++-- regression/taint/aliasing1/test.desc | 4 ++-- regression/taint/basic1/test.desc | 4 ++-- regression/taint/basic2/test.desc | 4 ++-- regression/taint/interface1/test.desc | 2 +- regression/taint/map1/test.desc | 2 +- 213 files changed, 306 insertions(+), 306 deletions(-) diff --git a/regression/ansi-c/struct6/test.desc b/regression/ansi-c/struct6/test.desc index d97230c659f..659eb69fc00 100644 --- a/regression/ansi-c/struct6/test.desc +++ b/regression/ansi-c/struct6/test.desc @@ -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$ diff --git a/regression/ansi-c/struct7/test.desc b/regression/ansi-c/struct7/test.desc index 9c24052d9c5..6c926d0df3a 100644 --- a/regression/ansi-c/struct7/test.desc +++ b/regression/ansi-c/struct7/test.desc @@ -1,7 +1,7 @@ CORE main.c -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^main.c:4:1: error: duplicate member .*$ ^CONVERSION ERROR$ diff --git a/regression/cbmc-concurrency/constant_prop1/test.desc b/regression/cbmc-concurrency/constant_prop1/test.desc index 2ae90c417a8..201dc9bdb6e 100644 --- a/regression/cbmc-concurrency/constant_prop1/test.desc +++ b/regression/cbmc-concurrency/constant_prop1/test.desc @@ -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 diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc index 0d60be7dfd0..41b36c525bf 100644 --- a/regression/cbmc-concurrency/pthread_join1/test.desc +++ b/regression/cbmc-concurrency/pthread_join1/test.desc @@ -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 diff --git a/regression/cbmc-cover/branch3/test.desc b/regression/cbmc-cover/branch3/test.desc index ae7869dca0b..5d9bce60ebe 100644 --- a/regression/cbmc-cover/branch3/test.desc +++ b/regression/cbmc-cover/branch3/test.desc @@ -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 diff --git a/regression/cbmc-cover/branch4/test.desc b/regression/cbmc-cover/branch4/test.desc index a37182e5491..86f003eeb8e 100644 --- a/regression/cbmc-cover/branch4/test.desc +++ b/regression/cbmc-cover/branch4/test.desc @@ -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 diff --git a/regression/cbmc-cover/condition1/test.desc b/regression/cbmc-cover/condition1/test.desc index f73b84397ee..a5945572059 100644 --- a/regression/cbmc-cover/condition1/test.desc +++ b/regression/cbmc-cover/condition1/test.desc @@ -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 diff --git a/regression/cbmc-cover/cover1/test.desc b/regression/cbmc-cover/cover1/test.desc index de6009c659d..b3fcd90f22b 100644 --- a/regression/cbmc-cover/cover1/test.desc +++ b/regression/cbmc-cover/cover1/test.desc @@ -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 diff --git a/regression/cbmc-cover/decision1/test.desc b/regression/cbmc-cover/decision1/test.desc index 2be13d5d5f2..29dd4e08212 100644 --- a/regression/cbmc-cover/decision1/test.desc +++ b/regression/cbmc-cover/decision1/test.desc @@ -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 diff --git a/regression/cbmc-cover/location1/test.desc b/regression/cbmc-cover/location1/test.desc index b575efbeda3..1016f7a1aea 100644 --- a/regression/cbmc-cover/location1/test.desc +++ b/regression/cbmc-cover/location1/test.desc @@ -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 diff --git a/regression/cbmc-cover/location11/test.desc b/regression/cbmc-cover/location11/test.desc index 398e9b8b36f..78e69e1e975 100644 --- a/regression/cbmc-cover/location11/test.desc +++ b/regression/cbmc-cover/location11/test.desc @@ -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 diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc index 8b46af0784d..1bae5a4eb12 100644 --- a/regression/cbmc-cover/location12/test.desc +++ b/regression/cbmc-cover/location12/test.desc @@ -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 diff --git a/regression/cbmc-cover/location13/test.desc b/regression/cbmc-cover/location13/test.desc index 543be77b095..387920fa1d0 100644 --- a/regression/cbmc-cover/location13/test.desc +++ b/regression/cbmc-cover/location13/test.desc @@ -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 diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc index f3cb25573da..52be93aeea7 100644 --- a/regression/cbmc-cover/location14/test.desc +++ b/regression/cbmc-cover/location14/test.desc @@ -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 diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index 3fb10c3066b..4efe26c9d40 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -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 diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc index bb81dddf43c..acb02daaf1a 100644 --- a/regression/cbmc-cover/location16/test.desc +++ b/regression/cbmc-cover/location16/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index 060d9040829..d1779e15ce6 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc index daf502e74af..eb5afa10812 100644 --- a/regression/cbmc-cover/mcdc10/test.desc +++ b/regression/cbmc-cover/mcdc10/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc index 616b3249b0d..2358a5feb12 100644 --- a/regression/cbmc-cover/mcdc11/test.desc +++ b/regression/cbmc-cover/mcdc11/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc index 44e823e13c4..341ceb9da53 100644 --- a/regression/cbmc-cover/mcdc12/test.desc +++ b/regression/cbmc-cover/mcdc12/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc index c7983f47aa9..85b417fa1d7 100644 --- a/regression/cbmc-cover/mcdc13/test.desc +++ b/regression/cbmc-cover/mcdc13/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc index 6778dfcc2f8..de3fd57033c 100644 --- a/regression/cbmc-cover/mcdc14/test.desc +++ b/regression/cbmc-cover/mcdc14/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc index 6c69a4144b5..7eea5938b73 100644 --- a/regression/cbmc-cover/mcdc2/test.desc +++ b/regression/cbmc-cover/mcdc2/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc index d2b3fdf6627..0a531a3b9ba 100644 --- a/regression/cbmc-cover/mcdc3/test.desc +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc index 9d55f2ebf19..9ed8f0e7fce 100644 --- a/regression/cbmc-cover/mcdc4/test.desc +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc index c65bbc9cd1d..7e012738b96 100644 --- a/regression/cbmc-cover/mcdc5/test.desc +++ b/regression/cbmc-cover/mcdc5/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc index 2072ee3b94b..7f5289c868d 100644 --- a/regression/cbmc-cover/mcdc6/test.desc +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc index 78af58eaf8d..7df603190cd 100644 --- a/regression/cbmc-cover/mcdc7/test.desc +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index bf8dabbfa0f..f1711f5c8d1 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -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 diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc index d8ec7ea5f82..3dbd096e9be 100644 --- a/regression/cbmc-cover/mcdc9/test.desc +++ b/regression/cbmc-cover/mcdc9/test.desc @@ -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 diff --git a/regression/cbmc-java/LocalVarTable2/test.desc b/regression/cbmc-java/LocalVarTable2/test.desc index 1e982eeac10..9e12f63756c 100644 --- a/regression/cbmc-java/LocalVarTable2/test.desc +++ b/regression/cbmc-java/LocalVarTable2/test.desc @@ -4,4 +4,4 @@ LocalVarTable2.class ^EXIT=0$ ^SIGNAL=0$ -- -return_value.*(void \*)i +return_value.*\(void \*\)i diff --git a/regression/cbmc-java/NullPointer1/test.desc b/regression/cbmc-java/NullPointer1/test.desc index 0394ce544f3..d479356875a 100644 --- a/regression/cbmc-java/NullPointer1/test.desc +++ b/regression/cbmc-java/NullPointer1/test.desc @@ -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 diff --git a/regression/cbmc-java/NullPointer2/test.desc b/regression/cbmc-java/NullPointer2/test.desc index 3be1eaa44fc..366d28f8b02 100644 --- a/regression/cbmc-java/NullPointer2/test.desc +++ b/regression/cbmc-java/NullPointer2/test.desc @@ -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 diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc index f4956e75540..cc33c21738b 100644 --- a/regression/cbmc-java/NullPointer3/test.desc +++ b/regression/cbmc-java/NullPointer3/test.desc @@ -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 diff --git a/regression/cbmc-java/NullPointer4/test.desc b/regression/cbmc-java/NullPointer4/test.desc index 653f7cf47bd..2e1b728c1fc 100644 --- a/regression/cbmc-java/NullPointer4/test.desc +++ b/regression/cbmc-java/NullPointer4/test.desc @@ -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 diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc index 74403444d22..14ee7eb85a8 100644 --- a/regression/cbmc-java/VarLengthArrayTrace1/test.desc +++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc @@ -7,4 +7,4 @@ dynamic_3_array\[1l\]=10 -- ^warning: ignoring assignment removed -irep("(\\"nil\\")") +irep\("\(\\"nil\\"\)"\) diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc index 8a395386017..d9ca7a162db 100644 --- a/regression/cbmc-java/enum1/test.desc +++ b/regression/cbmc-java/enum1/test.desc @@ -3,6 +3,6 @@ enum1.class --java-unwind-enum-static --unwind 3 ^EXIT=10$ ^SIGNAL=0$ -^Unwinding loop java::enum1.:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.:()V bytecode_index 78 thread 0$ +^Unwinding loop java::enum1.:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.:\(\)V bytecode_index 78 thread 0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/jar-file1/test.desc b/regression/cbmc-java/jar-file1/test.desc index b50d83b8645..2e8294c7276 100644 --- a/regression/cbmc-java/jar-file1/test.desc +++ b/regression/cbmc-java/jar-file1/test.desc @@ -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 diff --git a/regression/cbmc-java/jar-file2/test.desc b/regression/cbmc-java/jar-file2/test.desc index fb9e05dad2c..2cad29df307 100644 --- a/regression/cbmc-java/jar-file2/test.desc +++ b/regression/cbmc-java/jar-file2/test.desc @@ -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 diff --git a/regression/cbmc-java/jsr1/test.desc b/regression/cbmc-java/jsr1/test.desc index abcbe1427a1..faec2ddbb03 100644 --- a/regression/cbmc-java/jsr1/test.desc +++ b/regression/cbmc-java/jsr1/test.desc @@ -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\\"\) diff --git a/regression/cbmc-java/jsr2/test.desc b/regression/cbmc-java/jsr2/test.desc index 0fd8981318e..844d0c49668 100644 --- a/regression/cbmc-java/jsr2/test.desc +++ b/regression/cbmc-java/jsr2/test.desc @@ -9,5 +9,5 @@ Labels: pc9 Labels: pc12 Labels: pc13 -- -\\"statement\\" (\\"jsr\\") -\\"statement\\" (\\"ret\\") +\\"statement\\" \(\\"jsr\\"\) +\\"statement\\" \(\\"ret\\"\) diff --git a/regression/cbmc-java/package_friendly1/test.desc b/regression/cbmc-java/package_friendly1/test.desc index 108ea5defb1..527f5b9bfe0 100644 --- a/regression/cbmc-java/package_friendly1/test.desc +++ b/regression/cbmc-java/package_friendly1/test.desc @@ -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$ -- diff --git a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc index 4e0ad61997b..d2a7e3e7574 100644 --- a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc +++ b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/Fixedbv4/test.desc b/regression/cbmc-with-incr/Fixedbv4/test.desc index 967f48cfce8..a43bbd7df65 100644 --- a/regression/cbmc-with-incr/Fixedbv4/test.desc +++ b/regression/cbmc-with-incr/Fixedbv4/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc index 8b9ef5dc26b..d8033224594 100644 --- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc index d0e938b109c..cf4a284351e 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc index d40554751e7..b2bf0ea5879 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc index 0215dfc4361..a2ae3807cab 100644 --- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc +++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc @@ -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 diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc index 4f3dc3ca6c6..95e607f531d 100644 --- a/regression/cbmc-with-incr/pipe1/test.desc +++ b/regression/cbmc-with-incr/pipe1/test.desc @@ -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 diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc index 4e0ad61997b..d2a7e3e7574 100644 --- a/regression/cbmc/BV_Arithmetic3/test.desc +++ b/regression/cbmc/BV_Arithmetic3/test.desc @@ -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 diff --git a/regression/cbmc/Fixedbv4/test.desc b/regression/cbmc/Fixedbv4/test.desc index 967f48cfce8..a43bbd7df65 100644 --- a/regression/cbmc/Fixedbv4/test.desc +++ b/regression/cbmc/Fixedbv4/test.desc @@ -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 diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 6271e2d1865..9e34fa7f422 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -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 diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index 97ebee19e43..101a4c0e3bf 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -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 diff --git a/regression/cbmc/Overflow_Addition1/test.desc b/regression/cbmc/Overflow_Addition1/test.desc index 07fa8a17ceb..850b22d1a46 100644 --- a/regression/cbmc/Overflow_Addition1/test.desc +++ b/regression/cbmc/Overflow_Addition1/test.desc @@ -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 diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc index 32cb3052579..888430312a7 100644 --- a/regression/cbmc/Pointer_byte_extract2/test.desc +++ b/regression/cbmc/Pointer_byte_extract2/test.desc @@ -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 diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index ffd4b6e5750..8c70c85ee47 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -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 diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index a02bd08c46e..801d41ee41b 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -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 diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 89b2bd695c6..5b4797b9b00 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 97aa2540147..cfc835ce948 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc index 70d08657075..5682d588b9c 100644 --- a/regression/cbmc/Quantifiers-copy/test.desc +++ b/regression/cbmc/Quantifiers-copy/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 85382ac5ad0..e121e2e1955 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc index 4ebb8bc2d51..b10b600c308 100644 --- a/regression/cbmc/Quantifiers-initialisation/test.desc +++ b/regression/cbmc/Quantifiers-initialisation/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index ecf508fe2f7..ad5913e4d92 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc index e150f4a9e20..e38af4ddbdb 100644 --- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc +++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc @@ -3,5 +3,5 @@ main.c ^\*\* Results:$ -^\*\* 0 of 1 failed (1 iteration)$ +^\*\* 0 of 1 failed \(1 iteration\)$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index 3d9c805336a..51feeae3b08 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 8e763e9aa72..b1b6a0d1d60 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 32ab527b42f..2874b9dc0eb 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index ee061c91c3b..3bc8a8d2a5f 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -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$ diff --git a/regression/cbmc/null3/test.desc b/regression/cbmc/null3/test.desc index 7d1a2a85c81..60ac44fc4e0 100644 --- a/regression/cbmc/null3/test.desc +++ b/regression/cbmc/null3/test.desc @@ -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 diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc index a18dce04f12..26a7b98287a 100644 --- a/regression/cbmc/pipe1/test.desc +++ b/regression/cbmc/pipe1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_01_19/test.desc b/regression/cegis/cegis_danger_benchmark_01_19/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_01_19/test.desc +++ b/regression/cegis/cegis_danger_benchmark_01_19/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_02_20/test.desc b/regression/cegis/cegis_danger_benchmark_02_20/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_02_20/test.desc +++ b/regression/cegis/cegis_danger_benchmark_02_20/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_03_21/test.desc b/regression/cegis/cegis_danger_benchmark_03_21/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_03_21/test.desc +++ b/regression/cegis/cegis_danger_benchmark_03_21/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_04_23/test.desc b/regression/cegis/cegis_danger_benchmark_04_23/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_04_23/test.desc +++ b/regression/cegis/cegis_danger_benchmark_04_23/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_05_24/test.desc b/regression/cegis/cegis_danger_benchmark_05_24/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_05_24/test.desc +++ b/regression/cegis/cegis_danger_benchmark_05_24/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_06_25/test.desc b/regression/cegis/cegis_danger_benchmark_06_25/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_06_25/test.desc +++ b/regression/cegis/cegis_danger_benchmark_06_25/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_11_33/test.desc b/regression/cegis/cegis_danger_benchmark_11_33/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_11_33/test.desc +++ b/regression/cegis/cegis_danger_benchmark_11_33/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_17_40/test.desc b/regression/cegis/cegis_danger_benchmark_17_40/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_17_40/test.desc +++ b/regression/cegis/cegis_danger_benchmark_17_40/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_18_41/test.desc b/regression/cegis/cegis_danger_benchmark_18_41/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_18_41/test.desc +++ b/regression/cegis/cegis_danger_benchmark_18_41/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_19_42/test.desc b/regression/cegis/cegis_danger_benchmark_19_42/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_19_42/test.desc +++ b/regression/cegis/cegis_danger_benchmark_19_42/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_20_43/test.desc b/regression/cegis/cegis_danger_benchmark_20_43/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_20_43/test.desc +++ b/regression/cegis/cegis_danger_benchmark_20_43/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc index c1747971a06..f57dcb6d0a1 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc index 59aa0bcc847..b81a22e5b16 100644 --- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc +++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc @@ -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 diff --git a/regression/cegis/cegis_danger_unit_2x0/test.desc b/regression/cegis/cegis_danger_unit_2x0/test.desc index 3d7cfc3d517..14f8e34538d 100644 --- a/regression/cegis/cegis_danger_unit_2x0/test.desc +++ b/regression/cegis/cegis_danger_unit_2x0/test.desc @@ -3,8 +3,8 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)]x *- *DANGER_CONSTANT_2u;$ -^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$ -^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)]x *- *DANGER_CONSTANT_2u;$ +^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$ +^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_danger_unit_full1/test.desc b/regression/cegis/cegis_danger_unit_full1/test.desc index 3d7cfc3d517..14f8e34538d 100644 --- a/regression/cegis/cegis_danger_unit_full1/test.desc +++ b/regression/cegis/cegis_danger_unit_full1/test.desc @@ -3,8 +3,8 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)]x *- *DANGER_CONSTANT_2u;$ -^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$ -^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)]x *- *DANGER_CONSTANT_2u;$ +^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$ +^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_danger_unit_full2/test.desc b/regression/cegis/cegis_danger_unit_full2/test.desc index 54b35341472..043b25c8d05 100644 --- a/regression/cegis/cegis_danger_unit_full2/test.desc +++ b/regression/cegis/cegis_danger_unit_full2/test.desc @@ -3,11 +3,11 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_tmp_0 *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *DANGER_CONSTANT_2u *&& *DANGER_CONSTANT_2u *<= *[(]unsigned *int[)]x[)];$ -^.*__CPROVER_danger_D0_x *= *DANGER_CONSTANT_4294967295u *[+] *__CPROVER_danger_tmp_0;$ -^.*__CPROVER_danger_tmp_0 *= *[(]unsigned *int[)][(][(]signed *int[)]DANGER_CONSTANT_4294967295u *>> *[(]unsigned *int[)]x[)];$ -^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$ -^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$ -^.*__CPROVER_danger_S0_x_1 *= *[(]unsigned *int[)][(]__CPROVER_danger_S0_x_0 *< *DANGER_CONSTANT_0u *&& *DANGER_CONSTANT_0u *< *DANGER_CONSTANT_4294967294u[)];$ +^.*__CPROVER_danger_tmp_0 *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_2u *&& *DANGER_CONSTANT_2u *<= *[\(]unsigned *int[\)]x[\)];$ +^.*__CPROVER_danger_D0_x *= *DANGER_CONSTANT_4294967295u *[\+] *__CPROVER_danger_tmp_0;$ +^.*__CPROVER_danger_tmp_0 *= *[\(]unsigned *int[\)][\(][\(]signed *int[\)]DANGER_CONSTANT_4294967295u *>> *[\(]unsigned *int[\)]x[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$ +^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$ +^.*__CPROVER_danger_S0_x_1 *= *[\(]unsigned *int[\)][\(]__CPROVER_danger_S0_x_0 *< *DANGER_CONSTANT_0u *&& *DANGER_CONSTANT_0u *< *DANGER_CONSTANT_4294967294u[\)];$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_danger_unit_no_ranking/test.desc b/regression/cegis/cegis_danger_unit_no_ranking/test.desc index 10479cc9d39..ad6c659ec3c 100644 --- a/regression/cegis/cegis_danger_unit_no_ranking/test.desc +++ b/regression/cegis/cegis_danger_unit_no_ranking/test.desc @@ -3,7 +3,7 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic --danger-no-ranking ^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 diff --git a/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc b/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc index 1ede2b9dd9d..cae82d5046b 100644 --- a/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc +++ b/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc @@ -3,7 +3,7 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]signed *int[)]DANGER_CONSTANT_4u *>> *[(]unsigned *int[)]x[)];$ -^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *>> *[(]unsigned *int[)]x; +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]signed *int[\)]DANGER_CONSTANT_4u *>> *[\(]unsigned *int[\)]x[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *>> *[\(]unsigned *int[\)]x; -- ^warning: ignoring diff --git a/regression/cegis/cegis_danger_unit_x0_only/test.desc b/regression/cegis/cegis_danger_unit_x0_only/test.desc index 02b836b17c6..1a387823ad1 100644 --- a/regression/cegis/cegis_danger_unit_x0_only/test.desc +++ b/regression/cegis/cegis_danger_unit_x0_only/test.desc @@ -3,7 +3,7 @@ main.c --gcc --danger --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$ -^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_jsa_benchmark_00/test.desc b/regression/cegis/cegis_jsa_benchmark_00/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_00/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_00/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_01/test.desc b/regression/cegis/cegis_jsa_benchmark_01/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_01/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_01/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_02/test.desc b/regression/cegis/cegis_jsa_benchmark_02/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_02/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_02/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_03/test.desc b/regression/cegis/cegis_jsa_benchmark_03/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_03/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_03/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_04/test.desc b/regression/cegis/cegis_jsa_benchmark_04/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_04/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_04/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_05/test.desc b/regression/cegis/cegis_jsa_benchmark_05/test.desc index 52a05c4c1ba..d3350b330e6 100644 --- a/regression/cegis/cegis_jsa_benchmark_05/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_05/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa --jsa-aggregate=max -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_06/test.desc b/regression/cegis/cegis_jsa_benchmark_06/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_06/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_06/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_07/test.desc b/regression/cegis/cegis_jsa_benchmark_07/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_07/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_07/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_08/test.desc b/regression/cegis/cegis_jsa_benchmark_08/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_08/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_08/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_09/test.desc b/regression/cegis/cegis_jsa_benchmark_09/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_09/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_09/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_10/test.desc b/regression/cegis/cegis_jsa_benchmark_10/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_10/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_10/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_11/test.desc b/regression/cegis/cegis_jsa_benchmark_11/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_11/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_11/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_12/test.desc b/regression/cegis/cegis_jsa_benchmark_12/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_12/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_12/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_13/test.desc b/regression/cegis/cegis_jsa_benchmark_13/test.desc index c58556f9d0b..88f037ea975 100644 --- a/regression/cegis/cegis_jsa_benchmark_13/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_13/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa --jsa-aggregate=min -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_14/test.desc b/regression/cegis/cegis_jsa_benchmark_14/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_14/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_14/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_15/test.desc b/regression/cegis/cegis_jsa_benchmark_15/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_15/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_15/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_16/test.desc b/regression/cegis/cegis_jsa_benchmark_16/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_16/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_16/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_17/test.desc b/regression/cegis/cegis_jsa_benchmark_17/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_17/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_17/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_18/test.desc b/regression/cegis/cegis_jsa_benchmark_18/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_18/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_18/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_18_02/test.desc b/regression/cegis/cegis_jsa_benchmark_18_02/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_18_02/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_18_02/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_19/test.desc b/regression/cegis/cegis_jsa_benchmark_19/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_19/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_19/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_20/test.desc b/regression/cegis/cegis_jsa_benchmark_20/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_20/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_20/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_21/test.desc b/regression/cegis/cegis_jsa_benchmark_21/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_21/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_21/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_22/test.desc b/regression/cegis/cegis_jsa_benchmark_22/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_22/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_22/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_23/test.desc b/regression/cegis/cegis_jsa_benchmark_23/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_23/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_23/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_24/test.desc b/regression/cegis/cegis_jsa_benchmark_24/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_24/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_24/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_25/test.desc b/regression/cegis/cegis_jsa_benchmark_25/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_25/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_25/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_26/test.desc b/regression/cegis/cegis_jsa_benchmark_26/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_26/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_26/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_27/test.desc b/regression/cegis/cegis_jsa_benchmark_27/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_27/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_27/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_28/test.desc b/regression/cegis/cegis_jsa_benchmark_28/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_28/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_28/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_29/test.desc b/regression/cegis/cegis_jsa_benchmark_29/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_29/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_29/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_30/test.desc b/regression/cegis/cegis_jsa_benchmark_30/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_30/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_30/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_31/test.desc b/regression/cegis/cegis_jsa_benchmark_31/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_31/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_31/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_32/test.desc b/regression/cegis/cegis_jsa_benchmark_32/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_32/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_32/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_33/test.desc b/regression/cegis/cegis_jsa_benchmark_33/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_33/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_33/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_34/test.desc b/regression/cegis/cegis_jsa_benchmark_34/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_34/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_34/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_35/test.desc b/regression/cegis/cegis_jsa_benchmark_35/test.desc index 10e9fbb1886..7af97cec36a 100644 --- a/regression/cegis/cegis_jsa_benchmark_35/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_35/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-jsa-generate ^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 diff --git a/regression/cegis/cegis_jsa_benchmark_36/test.desc b/regression/cegis/cegis_jsa_benchmark_36/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_36/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_36/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_37/test.desc b/regression/cegis/cegis_jsa_benchmark_37/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_37/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_37/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_38/test.desc b/regression/cegis/cegis_jsa_benchmark_38/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_38/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_38/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_39/test.desc b/regression/cegis/cegis_jsa_benchmark_39/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_39/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_39/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_40/test.desc b/regression/cegis/cegis_jsa_benchmark_40/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_40/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_40/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_41/test.desc b/regression/cegis/cegis_jsa_benchmark_41/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_41/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_41/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_42/test.desc b/regression/cegis/cegis_jsa_benchmark_42/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_42/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_42/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_43/test.desc b/regression/cegis/cegis_jsa_benchmark_43/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_43/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_43/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_44/test.desc b/regression/cegis/cegis_jsa_benchmark_44/test.desc index 10e9fbb1886..7af97cec36a 100644 --- a/regression/cegis/cegis_jsa_benchmark_44/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_44/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-jsa-generate ^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 diff --git a/regression/cegis/cegis_jsa_benchmark_45/test.desc b/regression/cegis/cegis_jsa_benchmark_45/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_45/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_45/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_46/test.desc b/regression/cegis/cegis_jsa_benchmark_46/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_46/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_46/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_benchmark_47/test.desc b/regression/cegis/cegis_jsa_benchmark_47/test.desc index 02334169c67..c3924d3001c 100644 --- a/regression/cegis/cegis_jsa_benchmark_47/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_47/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-aggregate ^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 diff --git a/regression/cegis/cegis_jsa_benchmark_48/test.desc b/regression/cegis/cegis_jsa_benchmark_48/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_benchmark_48/test.desc +++ b/regression/cegis/cegis_jsa_benchmark_48/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_filter_01/test.desc b/regression/cegis/cegis_jsa_filter_01/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_filter_01/test.desc +++ b/regression/cegis/cegis_jsa_filter_01/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_jsa_map_01/test.desc b/regression/cegis/cegis_jsa_map_01/test.desc index fc0fa8eb921..07d2c6c73d6 100644 --- a/regression/cegis/cegis_jsa_map_01/test.desc +++ b/regression/cegis/cegis_jsa_map_01/test.desc @@ -3,7 +3,7 @@ main.c --gcc --jsa -D __CPROVER --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 diff --git a/regression/cegis/cegis_safety_unit_greater_two/test.desc b/regression/cegis/cegis_safety_unit_greater_two/test.desc index 047ce9e161e..ba5ab1f42ec 100644 --- a/regression/cegis/cegis_safety_unit_greater_two/test.desc +++ b/regression/cegis/cegis_safety_unit_greater_two/test.desc @@ -3,7 +3,7 @@ main.c --gcc --safety --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$ -^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_safety_unit_true/test.desc b/regression/cegis/cegis_safety_unit_true/test.desc index f3f8fe146b0..60aab0a2cea 100644 --- a/regression/cegis/cegis_safety_unit_true/test.desc +++ b/regression/cegis/cegis_safety_unit_true/test.desc @@ -3,7 +3,7 @@ main.c --gcc --safety ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$ -^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$ -- ^warning: ignoring diff --git a/regression/cegis/cegis_safety_unit_true2/test.desc b/regression/cegis/cegis_safety_unit_true2/test.desc index 047ce9e161e..ba5ab1f42ec 100644 --- a/regression/cegis/cegis_safety_unit_true2/test.desc +++ b/regression/cegis/cegis_safety_unit_true2/test.desc @@ -3,7 +3,7 @@ main.c --gcc --safety --cegis-statistics --cegis-genetic ^EXIT=0$ ^SIGNAL=0$ -^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$ -^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$ +^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$ +^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$ -- ^warning: ignoring diff --git a/regression/cpp-linter/throw/test.desc b/regression/cpp-linter/throw/test.desc index ebd3926785e..3162178e4e1 100644 --- a/regression/cpp-linter/throw/test.desc +++ b/regression/cpp-linter/throw/test.desc @@ -2,7 +2,7 @@ CORE main.cpp main\.cpp:25: Do not include brackets when throwing an error \[readability/throw\] \[4\] -main\.cpp:26: Extra space before ( in function call \[whitespace/parens\] \[4\] +main\.cpp:26: Extra space before \( in function call \[whitespace/parens\] \[4\] main\.cpp:26: Do not include brackets when throwing an error \[readability/throw\] \[4\] main\.cpp:28: First character of throw error message should be lower case \[readability/throw\] \[4\] main\.cpp:29: Do not include brackets when throwing an error \[readability/throw\] \[4\] diff --git a/regression/cpp/Address_of_Method2/test.desc b/regression/cpp/Address_of_Method2/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/Address_of_Method2/test.desc +++ b/regression/cpp/Address_of_Method2/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Address_of_Method3/test.desc b/regression/cpp/Address_of_Method3/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/Address_of_Method3/test.desc +++ b/regression/cpp/Address_of_Method3/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Constant2/test.desc b/regression/cpp/Constant2/test.desc index 1aaf62c1e14..166ae78593b 100644 --- a/regression/cpp/Constant2/test.desc +++ b/regression/cpp/Constant2/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Constant3/test.desc b/regression/cpp/Constant3/test.desc index 1aaf62c1e14..166ae78593b 100644 --- a/regression/cpp/Constant3/test.desc +++ b/regression/cpp/Constant3/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Pointer_Conversion1/test.desc b/regression/cpp/Pointer_Conversion1/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/Pointer_Conversion1/test.desc +++ b/regression/cpp/Pointer_Conversion1/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Resolver12/test.desc b/regression/cpp/Resolver12/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/Resolver12/test.desc +++ b/regression/cpp/Resolver12/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/Resolver4/test.desc b/regression/cpp/Resolver4/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/Resolver4/test.desc +++ b/regression/cpp/Resolver4/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/union3/test.desc b/regression/cpp/union3/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/union3/test.desc +++ b/regression/cpp/union3/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/union4/test.desc b/regression/cpp/union4/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/union4/test.desc +++ b/regression/cpp/union4/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/cpp/union5/test.desc b/regression/cpp/union5/test.desc index 1f21d7d0c49..bd3820cce3a 100644 --- a/regression/cpp/union5/test.desc +++ b/regression/cpp/union5/test.desc @@ -1,7 +1,7 @@ CORE main.cpp -^EXIT=\(64\|1\)$ +^EXIT=(64|1)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -- diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-instrument/data-flow1/test.desc index a11f4754f21..eb4fc8394e4 100644 --- a/regression/goto-instrument/data-flow1/test.desc +++ b/regression/goto-instrument/data-flow1/test.desc @@ -3,6 +3,6 @@ main.c --show-dependence-graph ^EXIT=0$ ^SIGNAL=0$ -Data dependencies: *[0-9]\+,[0-9]\+,[0-9]\+ +Data dependencies: *[0-9]+,[0-9]+,[0-9]+ -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_01/test.desc b/regression/goto-instrument/inline_01/test.desc index 36bbb89719e..85d55daa118 100644 --- a/regression/goto-instrument/inline_01/test.desc +++ b/regression/goto-instrument/inline_01/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -f[(].*[)];$ -g[(].*[)];$ -h[(].*[)];$ +f[\(].*[\)];$ +g[\(].*[\)];$ +h[\(].*[\)];$ ^warning: ignoring diff --git a/regression/goto-instrument/inline_02/test.desc b/regression/goto-instrument/inline_02/test.desc index ee604db74c9..20e93e09f77 100644 --- a/regression/goto-instrument/inline_02/test.desc +++ b/regression/goto-instrument/inline_02/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -f[(].*[)];$ -g[(].*[)];$ -h[(].*[)];$ +f[\(].*[\)];$ +g[\(].*[\)];$ +h[\(].*[\)];$ -- ^warning: ignoring diff --git a/regression/goto-instrument/inline_03/test.desc b/regression/goto-instrument/inline_03/test.desc index 4681dd60cea..3b6645c8a4c 100644 --- a/regression/goto-instrument/inline_03/test.desc +++ b/regression/goto-instrument/inline_03/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -f[(].*[)];$ -g[(].*[)];$ +f[\(].*[\)];$ +g[\(].*[\)];$ -- -h[(].*[)];$ +h[\(].*[\)];$ ^warning: ignoring diff --git a/regression/goto-instrument/inline_04/test.desc b/regression/goto-instrument/inline_04/test.desc index b4f0cef0dfa..8f2f03cf5f3 100644 --- a/regression/goto-instrument/inline_04/test.desc +++ b/regression/goto-instrument/inline_04/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -g[(].*[)];$ -h[(].*[)];$ +g[\(].*[\)];$ +h[\(].*[\)];$ -- -f[(].*[)];$ -other_func[(].*[)];$ +f[\(].*[\)];$ +other_func[\(].*[\)];$ ^warning: ignoring diff --git a/regression/goto-instrument/inline_11/test.desc b/regression/goto-instrument/inline_11/test.desc index 562879b7646..ca980d9baa6 100644 --- a/regression/goto-instrument/inline_11/test.desc +++ b/regression/goto-instrument/inline_11/test.desc @@ -5,5 +5,5 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -main[(].*[)]; +main[\(].*[\)]; ^warning: ignoring diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc index 54e56188c1b..24ed719acc2 100644 --- a/regression/strings/test3/test.desc +++ b/regression/strings/test3/test.desc @@ -3,8 +3,8 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$ -^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == .p.: SUCCESS$ -^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$ +^\[main.assertion.1\] assertion __CPROVER_string_length\(s\) == i \+ 5: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\(\"po\"\),s\): SUCCESS$ +^\[main.assertion.3\] assertion __CPROVER_char_at\(s, i\) == .p.: SUCCESS$ +^\[main.assertion.4\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\(\"p!o\"\), s\): FAILURE$ -- diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc index 589767e4b82..99f3cfd81de 100644 --- a/regression/strings/test_char_set/test.desc +++ b/regression/strings/test_char_set/test.desc @@ -3,6 +3,6 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("abc")): FAILURE$ +^\[main.assertion.1\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("apc"\)): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("abc"\)): FAILURE$ -- diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc index c3f1ca2a65a..8df68c18bc3 100644 --- a/regression/strings/test_concat/test.desc +++ b/regression/strings/test_concat/test.desc @@ -4,5 +4,5 @@ test.c ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] assertion c == .p.: SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == .p.: FAILURE$ +^\[main.assertion.2\] assertion __CPROVER_char_at\(u,2\) == .p.: FAILURE$ -- diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc index fcf9694b31d..f2414880794 100644 --- a/regression/strings/test_contains/test.desc +++ b/regression/strings/test_contains/test.desc @@ -3,7 +3,7 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"12\")): SUCCESS$ -^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"b\")): FAILURE$ +^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"3\"\)): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"12\"\)): SUCCESS$ +^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"b\"\)): FAILURE$ -- diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc index d3cfd4f3747..5fbe05f8fdd 100644 --- a/regression/strings/test_equal/test.desc +++ b/regression/strings/test_equal/test.desc @@ -3,6 +3,6 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("mippo")): FAILURE$ +^\[main.assertion.1\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("pippo"\)): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("mippo"\)): FAILURE$ -- diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc index a13b3dad852..8d78e11e71b 100644 --- a/regression/strings/test_int/test.desc +++ b/regression/strings/test_int/test.desc @@ -3,8 +3,8 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_char_at(s,0) == .1.: SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$ +^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_char_at\(s,1\) == .2.: SUCCESS$ ^\[main.assertion.3\] assertion j == 234: SUCCESS$ -^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(s,2) == .4.: FAILURE$ +^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at\(s,2\) == .4.: FAILURE$ -- diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc index 4e7cd79fde4..9bb75eda5b6 100644 --- a/regression/strings/test_pass1/test.desc +++ b/regression/strings/test_pass1/test.desc @@ -3,6 +3,6 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS -^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): FAILURE$ -^\*\* 1 of 2 failed (2 iterations)$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS +^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$ +^\*\* 1 of 2 failed \(2 iterations\)$ diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc index 0e64d9b84d1..3edb9f68f7a 100644 --- a/regression/strings/test_pass_pc3/test.desc +++ b/regression/strings/test_pass_pc3/test.desc @@ -3,6 +3,6 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_length(s3) == 0: FAILURE$ -^\[main.assertion.2\] assertion __CPROVER_string_length(s3) < 2: SUCCESS$ +^\[main.assertion.1\] assertion __CPROVER_string_length\(s3\) == 0: FAILURE$ +^\[main.assertion.2\] assertion __CPROVER_string_length\(s3\) < 2: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc index 6e2609d9cd3..a32376aca23 100644 --- a/regression/strings/test_substring/test.desc +++ b/regression/strings/test_substring/test.desc @@ -3,8 +3,8 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$ -^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$ -^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("cd")): FAILURE$ +^\[main.assertion.1\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cc"\)): FAILURE$ +^\[main.assertion.3\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("bc"\)): SUCCESS$ +^\[main.assertion.4\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): FAILURE$ -- diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc index a6667cfbfcf..9f425595434 100644 --- a/regression/strings/test_suffix/test.desc +++ b/regression/strings/test_suffix/test.desc @@ -3,6 +3,6 @@ test.c --string-refine ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.1\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$ -^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$ +^\[main.assertion.1\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("po"\),s\): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("pp"\),s\): FAILURE$ -- diff --git a/regression/taint/aliasing1/test.desc b/regression/taint/aliasing1/test.desc index f2f765d40b6..a0ac6401d67 100644 --- a/regression/taint/aliasing1/test.desc +++ b/regression/taint/aliasing1/test.desc @@ -3,7 +3,7 @@ aliasing1.class --taint taint.json ^EXIT=0$ ^SIGNAL=0$ -^file aliasing1.java line 10: There is a flow (taint rule my_sink)$ +^file aliasing1.java line 10: There is a flow \(taint rule my_sink\)$ -- -^file aliasing1.java line 8: There is a flow (taint rule my_sink)$ +^file aliasing1.java line 8: There is a flow \(taint rule my_sink\)$ ^warning: ignoring diff --git a/regression/taint/basic1/test.desc b/regression/taint/basic1/test.desc index d96a4d0c427..c4384ac9655 100644 --- a/regression/taint/basic1/test.desc +++ b/regression/taint/basic1/test.desc @@ -3,7 +3,7 @@ basic1.class --taint taint.json ^EXIT=0$ ^SIGNAL=0$ -^file basic1.java line 8: There is a T1 flow (taint rule my_h1)$ -^file basic1.java line 11: There is a T2 flow (taint rule my_h2)$ +^file basic1.java line 8: There is a T1 flow \(taint rule my_h1\)$ +^file basic1.java line 11: There is a T2 flow \(taint rule my_h2\)$ -- ^warning: ignoring diff --git a/regression/taint/basic2/test.desc b/regression/taint/basic2/test.desc index 25d5141cfa5..428281280c8 100644 --- a/regression/taint/basic2/test.desc +++ b/regression/taint/basic2/test.desc @@ -3,7 +3,7 @@ basic2.class --taint taint.json ^EXIT=0$ ^SIGNAL=0$ -^file basic2.java line 8: There is a T1 flow (taint rule my_h1)$ -^file basic2.java line 11: There is a T2 flow (taint rule my_h2)$ +^file basic2.java line 8: There is a T1 flow \(taint rule my_h1\)$ +^file basic2.java line 11: There is a T2 flow \(taint rule my_h2\)$ -- ^warning: ignoring diff --git a/regression/taint/interface1/test.desc b/regression/taint/interface1/test.desc index d24d8b6bfc5..6ac81f15786 100644 --- a/regression/taint/interface1/test.desc +++ b/regression/taint/interface1/test.desc @@ -3,6 +3,6 @@ interface1.class --taint taint.json ^EXIT=0$ ^SIGNAL=0$ -^file interface1.java line 18: There is a flow! (taint rule sink_rule)$ +^file interface1.java line 18: There is a flow! \(taint rule sink_rule\)$ -- ^warning: ignoring diff --git a/regression/taint/map1/test.desc b/regression/taint/map1/test.desc index 25bf4fb7e58..5526aa21b3a 100644 --- a/regression/taint/map1/test.desc +++ b/regression/taint/map1/test.desc @@ -3,6 +3,6 @@ map1.class --taint taint.json ^EXIT=0$ ^SIGNAL=0$ -^file map1.java line 12: There is a flow (taint rule my_sink)$ +^file map1.java line 12: There is a flow \(taint rule my_sink\)$ -- ^warning: ignoring