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