Squashed 'cbmc/' changes from 739c7f5..4820601

4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss
278f309 Merge pull request diffblue#1526 from reuk/reuk/fixup-unified-diff
69ba9e7 Merge pull request diffblue#1546 from smowton/smowton/feature/expose_tarjan
05dc65c Use lower-case characters to start error messages
8d0b23b Change asserts to invariants
a7afc6c Return from get_diff by value
6833af6 Fix formatting
4555d9f Remove unused parameter
e32c6c5 Make instructions_equal static
f815cc0 Move instructions_equal definition
11c9acc Add getter for data member
8c35211 Make data member private
f54db47 Rename differences map data member
b67d6e8 Merge pull request diffblue#1543 from chrisr-diffblue/cleanup/add-java-array-element-type-helper
c9241cd Make generic Tarjan's algorithm publically available
ebabdb9 Merge pull request diffblue#1542 from smowton/smowton/cleanup/sharing-node-assertion
a523d6f Add a helper function for accessing the element type of a Java array type
d8e8a68 Use INVARIANT rather than assert for sharing-node assertions
64d5dd2 Merge pull request diffblue#1538 from smowton/smowton/cleanup/remove-returns-asserts-to-invariants
fca7c04 Merge pull request diffblue#1537 from smowton/smowton/cleanup/sharing-node-test-to-catch
e35372a Merge pull request diffblue#1539 from romainbrenguier/bugfix/char-array-in-java-strings#TG-58#newpr
4d011b5 Merge pull request diffblue#1541 from owen-jones-diffblue/replace-unsigned-with-number-type
b2a4e39 Merge pull request diffblue#1540 from owen-jones-diffblue/rename-detach
2f6ceed Replace unsigned with appropriate type
938ab2b Replace 'detatch' with 'detach'
c219663 Convert sharing-node test to run under Catch
dec5ddf Remove-returns: asserts -> invariants
3b1f485 Merge pull request diffblue#1535 from andreast271/ignore-eclipse-vs-dirs
6cea5aa Ignore files and directories created by Eclipse and Visual Studio
aa94fe8 Style: add nolint marker on lines formated by clang
ee4a887 Merge pull request diffblue#1458 from LAJW/perl-platform
4da5a94 Add templating functionality to the perl script
21b2641 Move make_function_application to java_utils
5196e40 Merge pull request diffblue#884 from nmanthey/ipasir-no-ci
3ee3b25 Refactor: remove m_ prefix from member fields
539ff9f Refactoring: simplify and remove unused expression
5a0d6b4 Rename first_index in array_expr
d03b8cc Remove regression test that is not checking anything
90c8495 Improve tests for StringBuilder.append([C)
232617c Add code for String constructor from array
a2d7811 Use dynamic object instead of tmp_object in init
daef30f Splitting is_string and init_string parts of init
ad65847 Style: rename i in chr_int to avoid clash
e59349f Remove redundant check in from_int_with_radix
038b476 Allow index for argument of associate array to pointer
73d51fc Remove insert_long which duplicates insert_int
bb22700 Cleanup unused fields of constraint generator
2355e8e Fix set of created strings in generator and use it
26e895d Distinguish strings and char arrays in get
4b8a421 Make get_array return array of unknown expr
ca8213f Simplify not_contains constraints before negation
92897f7 Style fixes in string_constraint_generator.h
145364c String refinement: Improve debug information
3e5b3f1 Minor code improvements in string refinement
3d5465e Minor code improvements in generator_insert
86e1444 Refactoring: use begin()+3 instead of 3 times next
fef1c5f Correction in debug model
28590fe Correction in constraints for concat
6861b9d Documentation fixes in stirng constraint generator
c410159 Regression: StringBuilder append with int argument
e6700ff Minor improvements in  bytecode typecheck
61f0e1b Making check_axioms for string_constraints and not_contains_constraints more uniform
f2122c6 Correct signature of convert_exprt_to_string_exprt_unit_test
9edbb90 [string-refinement] Change get_array to return optional
86e4782 [string-refinement] Allow index set saturation if not_contains_constraints are present
c9c612d [string-refinement] Do not update index set of constant arrays
b88fe35 [string-refinement] Check for char type
1a22916 [string-refinement] Display debug info for index-set
982a5fc Style and documentation fixes in preprocessing
a83daa7 Minor indentation, naming and const-fixes
15fd1b4 Fix typos in strings and comments of string solver
26ae9a9 Unit test improve convert exprt to string exprt
b76b116 Minor improvements in string preprocessing
05a6b09 [constraint-generator] Removing declarations of unimplemented functions
302f92e Make string primitives return return_code_type
b80d063 Doxygen corrections
369dd62 Unit test: adapte instantiate_nc for new signature
dcae158 [string-refinement] Removing unused functions
b6b2669 Style changes in string_constraint_generator_testing
edf7057 Complete string solver rework
9ea2eda Unit tests for union_find_replacet
4adf5d0 New class for union find replace
1d112d5 Java object factory for nondet strings
0ae71b0 [string-preprocessing] New functions for calling string primitives in initialization
e89f5e4 [string-preprocess] Refactor java_types_matches_tag
2505982 Extra preconditions in string solver
6378400 Style improvements in the string solver
36d6e6d [util/irep_ids] Additional identifiers
fa45b34 Regression test mprovement for if expressions
76cd14d Unit test for gen_nondet_string_init
c71c64b Regression: include model for string to char array
c3d527c compiling: add IPASIR notes for Linux
900a0fc tests: do not match iterations line
751208d tests: drop number of iterations
12a6917 build: add ipasir solver support
14419d2 solvers: add ipasir driver
8aa89be build: introduce LIBSOLVER environment variable
df45bdb Merge pull request diffblue#1524 from reuk/reuk/fix-linter
4b39446 Merge pull request diffblue#1518 from diffblue/taint-for-C
25e18c0 Merge pull request diffblue#1529 from smowton/smowton/fix/float128
3cf67f7 Merge pull request diffblue#1531 from reuk/reuk/expr-cast-fixup
2169a39 Add _Float128 spelling for 128-bit float type
a3cf849 Merge pull request diffblue#1530 from martin-cs/feature/document-return-codes
188f263 Enable casting from derived types to other derived types
3dd7f6c first regression tests
29bc3b8 custom_bitvector_domain: allow objects that are members
ab7270e check taint on sinks _before_ the call
6daa8bd Merge pull request diffblue#1528 from tautschnig/shl-overflow
2df2abb Change a few erronious return codes so that they are more internally consistent.
cf96cef Minor changes to erronious exit behaviour.
c8dfd48 Replace constants exit codes with meaningfully named macros.
961d33a Replace literal constants in returns / exits with their symbolic names.
e74b442 Named, possibly even descriptive macros for the exit codes that are used.
1e3712c Shifts of non-integers and left shifts of negative integers are undefined
6bb3872 Check for overflow on left shift of signed ints
f9af374 Merge pull request diffblue#1512 from thk123/bugfix/TG-1058/crash-inner-class-generic-class
bd2e9c2 Merge pull request diffblue#1522 from reuk/reuk/clang-format-plain-diff
f892f4a Added tests for bracket matcher to include different types of brackets
3beab8b Fixed error in find_closing_delimiter
0b3058f Tightened up exception for unknown handling
9f87a80 Assertion on unmatched ; for parsing reference types
5922826 Adding doubly nested generic tests
4a62b07 Simplifying method names for unit test
ee39620 Extended tests to verify the generic information is being parsed correctly.
465a473 Parse multiple nested generic type informations
b8d43ab Pulled out method for parsing a list of multiple types
2a5c280 Correctly parse multiple input parameters for functions
35d974f Add method for finding the matching ; corresponding to a reference L
e1621a3 Hide methods relating to getting multiple type variables for specific param
e952708 Adding tests for parsing methods of generic classes with inner classes
958c006 Adding utilities for code_type structures
72a041b Don't crash when found an invalid reference type
ed545cb Refactored out the code for erasing generic types
effc1b2 Parse the whole class when generics are present
d23a0cc Added function for getting the full class name of a type
34c185e Unit test reproducing the bug described in TG-1058
5b92002 Adding utilities for checking types in unit tests
a00edd3 Disable dowhile brace check by default
d38b5d8 Disable colour in travis diff display

git-subtree-dir: cbmc
git-subtree-split: 4820601

Author: NathanJPhillips

.gitignore

@@ -11,6 +11,13 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 /*.creator.user
 /*.files
 /*.includes
+# Eclipse
+src/.cproject
+src/.project
+src/.settings/*
+# Visual Studio
+Debug/*
+Release/*
 
 # compilation files
 *.lo

.travis.yml

@@ -20,9 +20,10 @@ jobs:
         # Now we can do the formatting pass
         clang-format --version
         git-clang-format-3.8 "${TRAVIS_BRANCH}"
-        git diff --color > formatted.diff
+        git diff > formatted.diff
         if [[ -s formatted.diff ]] ; then
-          echo 'Formatting error! Apply the following diff and resubmit:'
+          echo 'Formatting error! The following diff shows the required changes'
+          echo 'Use the raw log to get a version of the diff that preserves spacing'
           cat formatted.diff
           exit 1
         fi

COMPILING.md

@@ -67,6 +67,13 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
 STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
 
+#ifndef __clang__
+// clang doesn't have these
+#if defined(__x86_64__) || defined(__i386__)
+STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
+#endif
+#endif
+
 /* Incompatible types */
 
 STATIC_ASSERT(!__builtin_types_compatible_p(char, _Bool));

regression/ansi-c/gcc_types_compatible_p1/main.c

@@ -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 
 --
 ^warning: ignoring

regression/cbmc-concurrency/pthread_join1/test.desc

@@ -10,6 +10,5 @@ main.c
 ^\[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%\)$
-^\*\* Used 10 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc1/test.desc

@@ -10,6 +10,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc11/test.desc

@@ -13,6 +13,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc12/test.desc

@@ -6,6 +6,5 @@ main.c
 ^\[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%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc14/test.desc

@@ -7,6 +7,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc3/test.desc

@@ -9,6 +9,5 @@ main.c
 ^\[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%\)$
-^\*\* Used 9 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc4/test.desc

@@ -6,6 +6,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc6/test.desc

@@ -8,6 +8,5 @@ main.c
 ^\[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%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc7/test.desc

@@ -8,6 +8,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc8/test.desc

@@ -9,6 +9,5 @@ main.c
 ^\[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

regression/cbmc-cover/mcdc9/test.desc

@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 26 function.*: FAILURE$
-\*\* 1 of [0-9]* failed \(2 iterations\)$
+\*\* 1 of [0-9]* failed 
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/exceptions1/test.desc

@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 15 function.*: FAILURE$
-^\*\* 1 of [0-9]* failed \(2 iterations\)$
+^\*\* 1 of [0-9]* failed 
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/exceptions2/test.desc

@@ -5,6 +5,6 @@ main.c
 ^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\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring

regression/cbmc-with-incr/Multi_Dimensional_Array6/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 
 --
 ^warning: ignoring

regression/cbmc-with-incr/Pointer_byte_extract2/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 
 --
 ^warning: ignoring

regression/cbmc-with-incr/Pointer_byte_extract5/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 
 --
 ^warning: ignoring

regression/cbmc-with-incr/Pointer_byte_extract8/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 
 --
 ^warning: ignoring

regression/cbmc-with-incr/pipe1/test.desc

@@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
 pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
-\*\* 4 of 36 failed \(3 iterations\)
+\*\* 4 of 36 failed 
 --
 ^warning: ignoring

regression/cbmc/Malloc23/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 
 --
 ^warning: ignoring

regression/cbmc/Multi_Dimensional_Array6/test.desc

@@ -0,0 +1,11 @@
+int main()
+{
+  unsigned char x;
+  unsigned r=x << ((sizeof(unsigned)-1)*8);
+  r=x << ((sizeof(unsigned)-1)*8-1);
+  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+
+  int s=-1 << ((sizeof(int)-1)*8);
+  s=-256 << ((sizeof(int)-1)*8);
+  return 0;
+}

regression/cbmc/Overflow_Leftshift1/main.c

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

regression/cbmc/Overflow_Leftshift1/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 
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract2/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 
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract5/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 
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract8/test.desc

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

regression/cbmc/Quantifiers-assertion/test.desc

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

regression/cbmc/Quantifiers-assignment/test.desc

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

regression/cbmc/Quantifiers-if/test.desc

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

regression/cbmc/Quantifiers-initialisation2/test.desc

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

regression/cbmc/Quantifiers-not/test.desc

@@ -4,5 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[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 
 ^VERIFICATION FAILED$

regression/cbmc/Quantifiers-type/test.desc

@@ -0,0 +1,11 @@
+int main()
+{
+  unsigned char x;
+  unsigned r=x << ((sizeof(unsigned)-1)*8);
+  r=x << ((sizeof(unsigned)-1)*8-1);
+  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+
+  int s=-1 << ((sizeof(int)-1)*8);
+  s=-256 << ((sizeof(int)-1)*8);
+  return 0;
+}

regression/cbmc/Undefined_Shift1/main.c

@@ -0,0 +1,9 @@
+CORE
+main.c
+--undefined-shift-check
+^SIGNAL=0$
+^\[.*\] shift operand is negative in .*: FAILURE$
+^\*\* 1 of 2 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Undefined_Shift1/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.3\] assertion p\[1\]=='b': FAILURE
-\*\* 1 of \d+ failed \(2 iterations\)
+\*\* 1 of \d+ failed 
 --
 ^warning: ignoring

regression/cbmc/fgets1/test.desc

@@ -7,6 +7,6 @@ main.c
 \[main.assertion.1\] assertion \*p==42: SUCCESS
 \[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
 \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
-\*\* 12 of 26 failed \(2 iterations\)
+\*\* 12 of 26 failed
 --
 ^warning: ignoring

regression/cbmc/memory_allocation1/test.desc

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

regression/cbmc/memset1/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 
 --
 ^warning: ignoring

regression/cbmc/pipe1/test.desc

@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 7 of 7 covered \(100.0%\)$
-^\*\* Used 4 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 5 of 5 covered \(100\.0%\)$
-^\*\* Used 3 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=4$

regression/cbmc/pointer-function-parameters/test.desc

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+void my_f(void *) { }
+void my_h(void *) { }
+void *my_g(void) { return malloc(1); }
+
+void my_function()
+{
+  void *o;
+
+  my_f(o); // T1 source
+  my_h(o); // T1,T2 sink
+
+  o=my_g(); // T2 source
+  my_h(o); // T1,T2 sink
+}

regression/goto-analyzer-taint-ansi-c/taint-basic1/main.c

@@ -0,0 +1,6 @@
+[
+{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "my_f" },
+{ "id": "my_g", "kind": "source", "where": "return_value", "taint": "T2", "function": "my_g" },
+{ "id": "my_h1", "kind": "sink",   "where": "parameter1", "taint": "T1", "function": "my_h", "message": "There is a T1 flow" },
+{ "id": "my_h2", "kind": "sink",   "where": "parameter1", "taint": "T2", "function": "my_h", "message": "There is a T2 flow" }
+]