Merge branch 'master' of https://github.com/diffblue/cbmc into fault-localization

Author: Peter Schrammel

.gitattributes

@@ -0,0 +1,11 @@
+*.cpp text
+*.c text
+*.h text
+*.y text
+*.tex text
+*.shtml text
+*.html text
+*.css text
+*.inc text
+test.desc text
+Makefile text

.gitignore

@@ -54,6 +54,8 @@ src/xmllang/xml_y.tab.h
 # binaries
 src/cbmc/cbmc
 src/cbmc/cbmc.exe
+src/cegis/cegis
+src/cegis/cegis.exe
 src/goto-analyzer/goto-analyzer
 src/goto-analyzer/goto-analyzer.exe
 src/goto-cc/goto-cc

COMPILING

@@ -15,7 +15,8 @@ environments:
 - Cygwin
   (We recommend the i686-pc-mingw32-g++ cross compiler, version 4.7 or above.)
 
-- Microsoft's Visual Studio 2012, 2013 or 2015 (older versions won't work)
+- Microsoft's Visual Studio version 12 (2013), version 14 (2015),
+  or version 15 (older versions won't work)
 
 The rest of this document is split up into three parts: compilation on
 Linux, MacOS, Windows.  Please read the section appropriate for your
@@ -52,14 +53,10 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 COMPILATION ON SOLARIS 11
 -------------------------
 
-0) We recommend you get OpenCSW. Follow the instructions at
-
-   http://www.opencsw.org/manual/for-administrators/getting-started.html
-
 1) As root, get the necessary development tools:
 
-   pkg install system/header
-   /opt/csw/bin/pkgutil -i gzip coreutils wget CSWpm-libwww-perl git flex bison CSWgcc4g++
+   pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
+   pkg install --accept developer/gcc-49
 
 2) As a user, get the CBMC source via
 
@@ -70,13 +67,16 @@ COMPILATION ON SOLARIS 11
    cd cbmc-git
    wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
    gtar xfz minisat_2.2.1.orig.tar.gz
+   mv minisat2-2.2.1 minisat-2.2.1
    (cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
 
 4) Type
 
-   cd src; gmake CXX=/opt/csw/bin/g++
+   cd src; gmake
+
+   That should do it. To run, you will need
 
-   That should do it.
+   export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
 
    Do not attempt to compile with gcc-45 that comes with Solaris 11.
    It will mis-optimize MiniSat2.
@@ -165,7 +165,7 @@ Follow these instructions:
    BUILD_ENV = MinGW
 
 3B) To compile with Visual Studio, make sure you have at least Visual
-   Studio 2012, and adjust the second line of config.inc to say
+   Studio version 12 (2013), and adjust the second line of config.inc to say
 
    BUILD_ENV = MSVC
 

regression/ansi-c/Universal_characters1/main.c

@@ -0,0 +1,18 @@
+int identifier_\u0201_;
+int \u0201_abc;
+
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1];    
+
+char my_string[]="\u0201";
+STATIC_ASSERT(sizeof(my_string)==3);
+
+// also as character literal
+STATIC_ASSERT(L'\u0201'==0x0201);
+
+int main()
+{
+  identifier_ȁ_=10;
+  ȁ_abc=10;
+}
+

regression/ansi-c/Universal_characters1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/array_initialization2/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int a[(int)(10./1.)];
+int b[(int)2] = { 10, 20 };
+int c[(int)(10./1.)] = { 10, 20 };
+int d[(int)(10/1)] = { 10, 20 };
+
+int main (void) {
+  if (a[0]) {
+    assert(b[1] + c[2] > 20);
+  }
+
+  return 1;
+}
+
+extern int g_array[];
+int array[(int)(10./1)];
+
+int array2[(int)(10./1)];

regression/ansi-c/array_initialization2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/enum7/main.c

@@ -0,0 +1,8 @@
+int main(void)
+{
+  enum enum_tag { A = 2 };
+
+  {
+     enum enum_tag { A = 3 };
+  }
+}

regression/ansi-c/enum7/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/float_constant1/main.c

@@ -7,6 +7,9 @@ STATIC_ASSERT(0x1.0p-95f == 2.524355e-29f);
 // also with upper case X, P, F
 STATIC_ASSERT(0X1.0P-95F == 2.524355e-29f);
 
+// nothing before the dot
+STATIC_ASSERT(0X.0p+1f == 0);
+
 #ifdef __GNUC__
 _Complex c;
 #endif

regression/ansi-c/gcc_builtins1/main.c

@@ -1,14 +1,17 @@
 #ifdef __GNUC__
 
-enum { E1 = __builtin_isinf(1.0) };
-enum { E2 = __builtin_isnan(1.0) };
-enum { E3 = __builtin_isinf(__builtin_inf()) };
-enum { E4 = __builtin_signbit(-1.0) };
-enum { E5 = __builtin_classify_type(1) };
-enum { E6 = sizeof(int) };
-enum { E7 = __alignof__(int) };
-enum { E8 = (int)1.0 };
-enum { E9 = __builtin_popcount(123) };
+enum { E01 = __builtin_isinf(1.0) };
+enum { E02 = __builtin_isnan(1.0) };
+enum { E03 = __builtin_isinf(__builtin_inf()) };
+enum { E04 = __builtin_signbit(-1.0) }; // clang doesn't do this one
+enum { E05 = __builtin_classify_type(1) };
+enum { E06 = sizeof(int) };
+enum { E07 = __alignof__(int) };
+enum { E08 = (int)1.0 };
+enum { E09 = __builtin_popcount(123) };
+enum { E10 = __builtin_bswap16(0xaabb) };
+enum { E11 = __builtin_bswap32(0xaabb) };
+enum { E12 = __builtin_bswap64(0xaabb) };
 
 #endif
 

regression/cbmc-concurrency/atomic_section_sc6/test.desc

@@ -3,6 +3,6 @@ main.c
 
 ^EXIT=10$
 ^SIGNAL=0$
-^start_thread in atomic section detected$
+^file main.c line 12 function spawn: start_thread in atomic section detected$
 --
 ^warning: ignoring

regression/cbmc-concurrency/norace_array1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/norace_array2/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <pthread.h>
+#include <stdlib.h>
+
+unsigned long data[2];
+
+void *thread0(void *arg)
+{
+    data[0] = 1;
+    return NULL;
+}
+
+void *thread1(void *arg)
+{
+    data[1] = 1;
+    return NULL;
+}
+
+int main(int argc, char *argv[])
+{
+    pthread_t t0;
+    pthread_t t1;
+
+    pthread_create(&t0, NULL, thread0, NULL);
+    pthread_create(&t1, NULL, thread1, NULL);
+    pthread_join(t0, NULL);
+    pthread_join(t1, NULL);
+
+    assert(data[0] == 1);
+    assert(data[1] == 1);
+
+    return 0;
+}

regression/cbmc-concurrency/norace_array2/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-concurrency/norace_struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cbmc-cover/branch2/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 5 function main function main entry point: SATISFIED$
-^\[main.coverage.2\] file main.c line 6 function main function main block 2 branch false: SATISFIED$
-^\[main.coverage.3\] file main.c line 6 function main function main block 2 branch true: SATISFIED$
+^\[main.coverage.2\] file main.c line 6 function main function main block 3 branch false: SATISFIED$
+^\[main.coverage.3\] file main.c line 6 function main function main block 3 branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc1/main.c

@@ -17,4 +17,6 @@ int main()
   else
   {
   }
+
+  return 1;
 }

regression/cbmc-cover/mcdc1/test.desc

@@ -3,7 +3,13 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
+^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
+^\[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%)$
-^\*\* Used 6 iterations$
+^\*\* Used 10 iterations$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc2/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+
+  __CPROVER_bool A, B, C;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+
+  if(A||B||C)
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc2/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
+^\[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%)$
+^\*\* Used 6 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc3/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+  unsigned x, y;
+  
+  __CPROVER_input("x", x);
+  __CPROVER_input("y", y);
+  
+  if (!(x>3) && y<5) 
+    ;
+
+  return 1;
+}

regression/cbmc-cover/mcdc3/test.desc

@@ -0,0 +1,12 @@
+CORE
+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%)$
+^\*\* Used 4 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc4/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+
+  __CPROVER_bool A, B, C, D;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if((A && B) || (C && D)) 
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}

regression/cbmc-cover/mcdc4/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover mcdc
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
+^\[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%)$
+^\*\* Used 9 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/mcdc5/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+  __CPROVER_bool A, B, C, D;
+
+  __CPROVER_input("A", A);
+  __CPROVER_input("B", B);
+  __CPROVER_input("C", C);
+  __CPROVER_input("D", D);
+
+  if((A || B)  && (C || D)) 
+  {
+  }
+  else
+  {
+  }
+
+  return 1;
+}