Squashed 'cbmc/' changes from ad62682..31c47c2

31c47c2 Merge pull request diffblue#2113 from diffblue/java_new_array_data
fb3025d Merge pull request diffblue#2107 from thk123/feature/TG-3271/interpreter-tracking-mock-exceptions
32bf48e Merge pull request diffblue#2105 from tautschnig/determinise-test
7254a2a show java_new_array_data side effects
0f1482c Merge pull request diffblue#2094 from smowton/smowton/fix/tmp-object-factory-prefix
3cfec66 Merge pull request diffblue#2106 from diffblue/ptrmember_on_array
bf4c39c Merge pull request diffblue#1966 from JohnDumbell/JohnDumbell/Update-Assertion-Validation
74a37c6 Merge pull request diffblue#1988 from tautschnig/cadical
74dc576 Merge pull request diffblue#2003 from tautschnig/bitfield-offset
8916906 Merge pull request diffblue#2008 from tautschnig/section-bug
0bd83ab Extension to interpreter class
a0ca0ba fix array->f typechecking
e1f4120 Make virtual function resolution independent of string table entry ordering
714ccff Merge pull request diffblue#2072 from danpoe/feature/small-shared-two-way-ptr
16b6c20 Merge pull request diffblue#2046 from thk123/gs_tg2922
04cb909 Merge pull request diffblue#2102 from thk123/formatting/sort-includes-clang-format
7070ba1 Sort includes using clang-format
9874a6b Reformatting touched output function
f2a4054 Remove redundant default constructor
54fb9ab Use format rather than from_expr for output
781bf7c Introduce exceptions for all conversion steps.
21997b2 Add documentation to convert_bitvector
015b284 Test demonstrating logging with clause for dealing with Windows
9d41b0c Disable nested exception printing for Windows
b866015 Provide the original goto statement in the error
a97bc28 Introduce throwing a guard conversion exception
12f25c2 Introduce throwing bv_conversion expection
9bd5222 Convert flatten_byte_extract to use structured exceptions
3207291 Introduce nested exception printing
35c4be7 Small shared two way pointer
7d247da Merge pull request diffblue#2099 from mgudemann/bugfix/build/glucose_syrup
1776a9e Merge pull request diffblue#1950 from romainbrenguier/refactor/prop_conv_straightforward
4147243 Change set_variable_name API to consume irep_idt
2d8be06 Rename `it` to pair in boolbvt::print_assignment
4365c28 Simplify boolbvt::set_to
b18109f Make make_(free_)bv_expr return exprt
5724a35 Simplify loop in prop_conv::get
4987f3a Remove useless comments
13e87a9 Simplify dec_solve
a0500f6 Use standard algorithm for finding an element
ba13c94 Use auto for iterator types
9179571 Remove useless includes
a905a07 Replace throws by invariant or preconditions
7db44fc Remove virtual keyword where not needed
990f33e Initialize at declaration instead of construction
c1a93b3 Renaming `it` to symbol
8eb20f6 Use ranged for
dc799e0 Assert replaced by unreachable
c34e073 Add support for CaDiCaL
1bd9efd Merge pull request diffblue#2097 from peterschrammel/java-cleanup-replace
a079f46 Clang-format moved file
2eb3714 Move replace_java_nondet to java_bytecode
9a8c292 Remove unnecessary include
c8cf100 Remove Java refs from ANSI-C docs
0090952 Merge pull request diffblue#2096 from diffblue/cleanout-java
aa3caa3 Fix CMake build for Glucose Syrup
1156930 Merge pull request diffblue#1244 from tautschnig/goto-gcc-at-fix
706e391 Merge pull request diffblue#2093 from owen-jones-diffblue/owen-jones-diffblue/remove_unnecessary_irep_id_hash
290feb4 Merge pull request diffblue#2095 from diffblue/get_json_stream_precondition
ac2df21 Merge pull request diffblue#2027 from tautschnig/linking-multiple-conflicts
dd0d602 Merge pull request diffblue#2030 from tautschnig/goto-cc-linux-kernel
42e58d4 Merge pull request diffblue#2085 from tautschnig/from_expr-cleanup
692f92d remove dependency on java_bytecode
8c6165d precondition for get_json_stream()
e28a662 Remove unused typedef
5626fb7 Merge pull request diffblue#2092 from smowton/smowton/cleanup/diffblue-spelling
4840154 Replace stack by deque and use range-based for loop
987edbe Use range-based for loops
92ac82c Remove redundant irep_id_hash for unordered maps
dc2b436 Remove redundant irep_id_hash for sets
5aa2c2d Attribute main function arguments to __CPROVER_start
b7ef5af Merge pull request diffblue#2053 from owen-jones-diffblue/owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions
252474f String tests: DiffBlue -> Diffblue
de1915a Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-no-candidate-callees
d73f6bc Make directed callgraph include nodes with no edges
2a45e61 Only the top-level section should be considered for renaming
9c66a66 fixup! Support __attribute__((section("x"))
e133964 C front-end: Section/ASM renaming also needs to be applied to aliases
0cfc72f Test --call-graph and --reachable-call-graph
1c34d22 Test lazy-loading when there are no candidates
289a439 Deal with virtual function calls with no candidate targets
9347615 Remove incorrect comment
18b1962 Fix order of parameters in function header
82058da Store virtual function calls instead of virtual call-sites
3653550 Use unordered set of irep_ids in ci_lazy_methods
c31d43f Remove code duplication
945f885 Rename two variables and make one more local
b7d70e7 Replace do-while loop with equally valid while loop
58b990d Use from_{expr,type} matching the language of the expression/type
177c8c1 goto-cc: support thin ar archives, refactoring
e80008e goto-cc: support GCC's print-sysroot* options
38e6fa5 Accept the --build-id option in goto-ld
f3bbb12 Linking: report multiple conflicts
495f109 Fixing member offset computation in presence of bitfields
5109eab Add @<file> arguments to the original command line
97d556e Update desc file to add pass variables.
eea76ec Add a regression test.
c14e907 Increase AssertionError arguments allowed from 2 to 3

git-subtree-dir: cbmc
git-subtree-split: 31c47c2

Author: Owen Jones

.clang-format

@@ -84,7 +84,7 @@ NamespaceIndentation: None
 PenaltyBreakString: 10000
 PointerAlignment: Right
 ReflowComments: 'false'
-SortIncludes: 'false'
+SortIncludes: 'true'
 SpaceAfterCStyleCast: 'false'
 SpaceBeforeAssignmentOperators: 'true'
 SpaceBeforeParens: Never

regression/ansi-c/Struct_ptrmember1/main.c

@@ -0,0 +1,10 @@
+struct some_struct
+{
+  int some_field;
+} array[10];
+
+int main()
+{
+  array[0].some_field=1;
+  array->some_field=1;
+}

regression/ansi-c/Struct_ptrmember1/test.desc

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

regression/ansi-c/gcc_attributes11/main.c

@@ -0,0 +1,18 @@
+#ifdef __GNUC__
+// example extracted from SV-COMP's ldv-linux-3.4-simple/
+// 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640
+static int __attribute__((__section__(".init.text")))
+__attribute__((no_instrument_function)) dp83640_init(void)
+{
+  return 0;
+}
+int init_module(void) __attribute__((alias("dp83640_init")));
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  dp83640_init();
+#endif
+  return 0;
+}

regression/ansi-c/gcc_attributes11/test.desc

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

regression/ansi-c/gcc_attributes9/main.c

@@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar();
 volatile int __attribute__((__section__(".init.data1"))) txt_heap_base1;
 volatile int __attribute__((__section__(".init.data3"))) txt_heap_base, __attribute__((__section__(".init.data4"))) txt_heap_size;
 
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+__alloc_bootmem_huge_page(void *h);
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+alloc_bootmem_huge_page(void *h);
+int alloc_bootmem_huge_page(void *h)
+  __attribute__((weak, alias("__alloc_bootmem_huge_page")));
+int __alloc_bootmem_huge_page(void *h)
+{
+  return 1;
+}
 #endif
 
 int main()
 {
 #ifdef __GNUC__
+  int r = alloc_bootmem_huge_page(0);
+
   static int __attribute__((section(".data.unlikely"))) __warned;
   __warned=1;
   return __warned;

regression/ansi-c/linking_conflicts1/main.c

@@ -0,0 +1,14 @@
+int bar()
+{
+  return 0;
+}
+
+int bar2()
+{
+  return 0;
+}
+
+int main()
+{
+  unsigned x = foo();
+}

regression/ansi-c/linking_conflicts1/other.c

@@ -0,0 +1,12 @@
+void bar()
+{
+}
+
+void bar2()
+{
+}
+
+unsigned foo()
+{
+  return 0;
+}

regression/ansi-c/linking_conflicts1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+other.c
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+error: conflicting function declarations `bar'
+error: conflicting function declarations `bar2'
+--
+^warning: ignoring

regression/cbmc-java/assertion_error_constructors/AssertionIssue.class

@@ -0,0 +1,13 @@
+public class AssertionIssue {
+
+    public static void throwAssertion() {
+        throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
+    }
+
+    public static class ThrowableAssertion extends Throwable {
+        @Override
+        public String getMessage() {
+            return "How did we get here?";
+        }
+    }
+}

regression/cbmc-java/assertion_error_constructors/AssertionIssue.java

@@ -0,0 +1,8 @@
+CORE
+AssertionIssue.class
+--function AssertionIssue.throwAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/assertion_error_constructors/test.desc

@@ -0,0 +1,7 @@
+public class TestClass {
+  public static void f(int y) {
+    float[][] a1 = new float[y][3];
+    int j = 0;
+    a1[j][0] = 34.5f;
+  }
+}

regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class

@@ -0,0 +1,10 @@
+CORE
+TestClass.class
+--function TestClass.f --cover location --unwind 2
+Source GOTO statement: .*
+(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
+^EXIT=6$
+--
+--
+The exception thrown in this test is the symptom of a bug; the purpose of this
+test is the validate the output of that exception

regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java

@@ -0,0 +1,12 @@
+public class Test {
+
+  interface factory_intf {
+    public intf getintf();
+  }
+
+  interface intf {
+    public void f();
+  }
+
+  public static void main(factory_intf i) { i.getintf().f(); }
+}

regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--lazy-methods --show-goto-functions --verbosity 10 --function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$
+Test\$intf\.f:\(\)V\(\);$
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class

@@ -3,6 +3,6 @@ test.class
 --show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
-IF.*"java::C".*THEN GOTO
-IF.*"java::D".*THEN GOTO
+IF.*"java::B".*THEN GOTO
+IF.*"java::E".*THEN GOTO
 IF.*"java::A".*THEN GOTO

regression/cbmc-java/lazyloading_no_candidates/Test$intf.class

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#pragma pack(1)
+struct A
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c : 2;
+  unsigned char d;
+};
+
+struct B
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c;
+  unsigned char d : 2;
+};
+
+struct C
+{
+  unsigned char a;
+  unsigned char b : 4;
+  unsigned char c : 4;
+  unsigned char d;
+};
+#pragma pack()
+
+int main(void)
+{
+  assert(sizeof(struct A) == 3);
+  struct A *p = malloc(3);
+  assert((unsigned char *)p + 2 == &(p->d));
+  p->c = 3;
+  if(p->c != 3)
+  {
+    free(p);
+  }
+  free(p);
+
+  assert(sizeof(struct B) == 4);
+  struct B *pb = malloc(4);
+  assert((unsigned char *)pb + 2 == &(pb->c));
+  free(pb);
+
+  assert(sizeof(struct C) == 3);
+  struct C *pc = malloc(3);
+  assert((unsigned char *)pc + 2 == &(pc->d));
+  free(pc);
+
+  return 0;
+}

regression/cbmc-java/lazyloading_no_candidates/Test.class

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

regression/cbmc-java/lazyloading_no_candidates/Test.java

@@ -0,0 +1 @@
+other.c

regression/cbmc-java/lazyloading_no_candidates/test.desc

@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  return foo();
+}

regression/cbmc-java/virtual7/test.desc

@@ -0,0 +1,4 @@
+int foo()
+{
+  return 1;
+}

regression/cbmc/Bitfields3/main.c

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

regression/cbmc/Bitfields3/test.desc

@@ -0,0 +1,81 @@
+
+int x;
+
+void func0()
+{
+  func0();
+}
+
+void func1()
+{
+  x = 1;
+}
+
+void func2()
+{
+  x = 2;
+  func3();
+}
+
+void func3()
+{
+  x = 3;
+}
+
+void func4(int b)
+{
+  x = 4;
+  if(b)
+  {
+    func5(0);
+  }
+}
+
+void func5(int b)
+{
+  x = 5;
+  func4(b);
+}
+
+void func6()
+{
+  x = 6;
+}
+
+void func7(int b)
+{
+  x = 7;
+  if(b)
+  {
+    func8(0);
+  }
+}
+
+void func8(int b)
+{
+  x = 8;
+  func7(b);
+}
+
+void func9()
+{
+  x = 9;
+  funca();
+}
+
+void funca()
+{
+  x = 10;
+  func9();
+}
+
+
+
+int main()
+{
+  func1();
+  func2();
+  func4(1);
+
+  return 0;
+}

regression/goto-gcc/at_files/args

@@ -0,0 +1,20 @@
+CORE
+main.c
+--call-graph
+^EXIT=0$
+^SIGNAL=0$
+^main -> func2$
+^main -> func1$
+^main -> func4$
+^funca -> func9$
+^func9 -> funca$
+^func8 -> func7$
+^func7 -> func8$
+^__CPROVER__start -> __CPROVER_initialize$
+^__CPROVER__start -> main$
+^func2 -> func3$
+^func0 -> func0$
+^func4 -> func5$
+^func5 -> func4$
+--
+^warning: ignoring