Merge branch 'diffblue:develop' into goto-synthesizer

Author: qinheping

CMakeLists.txt

@@ -216,6 +216,7 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    cprover-api-cpp
     cprover
     cprover-lib
     crangler

CODEOWNERS

@@ -44,7 +44,7 @@
 /jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
 /src/analyses/ @martin-cs @peterschrammel @chris-ryder
 /src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
-
+/src/libcprover-cpp @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel
 
 # These files change frequently and changes are medium-risk
 

regression/CMakeLists.txt

@@ -85,6 +85,7 @@ add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 add_subdirectory(cpp-linter)
 add_subdirectory(catch-framework)
+add_subdirectory(libcprover-cpp)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/ansi-c/gcc_attribute_used1/main.c

@@ -0,0 +1,6 @@
+static int foo __attribute__((used)) = 42;
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/gcc_attribute_used1/other.c

@@ -0,0 +1,15 @@
+struct bar
+{
+  char *ptr;
+};
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data")));
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data"))) = {0};
+
+void use_foo()
+{
+  __CPROVER_assert(foo.ptr == 0, "null");
+}

regression/cbmc-library/Float_lib2/test.desc renamed to regression/ansi-c/gcc_attribute_used1/test.desc

@@ -1,8 +1,8 @@
-CORE
+CORE gcc-only
 main.c
---floatbv
+other.c
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc-concurrency/thread_chain_cbmc1/main.c

@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-concurrency/thread_chain_cbmc2/main.c

@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c renamed to regression/cbmc-incr-smt2/pointers-conversions/byte_extract.c

@@ -6,7 +6,7 @@ int main()
   uint32_t input;
   uint32_t original = input;
   uint8_t *ptr = (uint8_t *)(&input);
-  assert(*ptr == 0); // falsifiable
+  assert(*ptr != 42); // falsifiable
   *ptr = ~(*ptr);
   assert(input != original); // valid
 }

regression/cbmc-incr-smt2/pointers-conversions/byte_extract.desc

@@ -0,0 +1,19 @@
+CORE
+byte_extract.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion \*ptr != 42: FAILURE
+\[main\.assertion\.\d+\] line \d+ assertion input != original: SUCCESS
+  input=42ul? \(00000000 00000000 00000000 00101010\)
+  original=42ul? \(00000000 00000000 00000000 00101010\)
+Violated property:
+  file byte_extract.c function main line \d+ thread \d+
+  assertion \*ptr != 42
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_extract_little_endian
+--
+This test is here to document our lack of support for byte_extract_little_endian
+in the pointers support for the new SMT backend.