Merge commit '356aed461b387a8ae815a9901a16d26f32f102be' into develop

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" }
+]