Squashed 'cbmc/' changes from da61186..31ef182

31ef182 Merge pull request diffblue#2208 from diffblue/cleanout-goto-programs
0e84d3e Merge pull request diffblue#2195 from smowton/smowton/feature/smarter-reachability-slicer
c801126 Merge pull request diffblue#2209 from diffblue/travis-no-osx-g++
3487bf7 Reachability slicer: mark reachable code more precisely
85e8451 Merge pull request diffblue#2066 from tautschnig/bv-endianness
5e5eafb Merge pull request diffblue#2191 from smowton/smowton/feature/java-fatal-assertions
8a68ab8 remove g++ build on OS X; this is identical to the clang++ build
48e5b25 Amend faulty long-string test
3f718ba Java: make null-pointer and similar checks fatal
821eb1d remove basic_blocks and goto_program_irep
d87c2db Merge pull request diffblue#2203 from diffblue/typed-lookup
d77dea3 strongly type the lookup() methods in namespacet
2382f27 Merge pull request diffblue#2193 from martin-cs/feature/correct-instruction-documentation
c314272 Merge pull request diffblue#2181 from diffblue/format-expr-constants
514a0a5 Merge pull request diffblue#2167 from diffblue/parse_unwindset_options
0102452 move escape(s) to string_utils
f1b6174 use unwindsett in goto-instrument
dcc907a introduce unwindsett for unwinding limits
10aeae8 format_expr now does index, c_bool constants, string constants
92b92d6 Correct the documentation of ASSERT : it does not alter control flow.
a11add8 Expand the documentation of the goto-program instructions.
a06503b Merge pull request diffblue#2197 from tautschnig/fix-help
05e4bc3 Remove stray whitespace previously demanded by clang-format
3261f4d Fix help output of --generate-function-body-options
7c67b23 Merge pull request diffblue#2110 from tautschnig/type-mismatch-exception
18fb262 Merge pull request diffblue#2025 from tautschnig/stack-depth-fix
9191b6a Merge pull request diffblue#2199 from tautschnig/simplifier-typing
f99e631 Merge pull request diffblue#2198 from tautschnig/fix-test-desc
1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty
a7690ba Merge pull request diffblue#2185 from smowton/smowton/fix/tolerate-ts18661-types
fc02e8f Restore returns before writing the simplified binary
49333eb Make restore_returns handle simplified programs
46f7987 Fix perl regular expressioons in regression test descriptions
9fe432b Merge pull request diffblue#1899 from danpoe/sharing-map-catch-unit-tests
9cc6aae Merge pull request diffblue#2081 from hannes-steffenhagen-diffblue/floating_point_simplificiation
da19abe Tolerate TS 18661 (_Float32 et al) types
a055454 Try all rounding modes when domain is unknown
5f7bc15 Add float support to constant propagator domain
3dc2244 Move adjust_float_expressions to goto-programs
06d8bea Merge pull request diffblue#2187 from diffblue/move-convert-nondet
6d8c3fa Merge pull request diffblue#2189 from thk123/bugfix/json-parser-restart
2ad157f Merge pull request diffblue#2186 from smowton/smowton/fix/call-graph-uninit-field
cd54ad7 Corrected state persistence in the json parser
4447be0 Fix uninitialised collect_callsites field in call_grapht
ead0aa3 Merge pull request diffblue#2188 from smowton/smowton/fix/init-string-types-without-refine-strings
57988fc Fix String type initialisation when --refine-strings is not active
6a76aff Move convert_nondet to java_bytecode
ac6eb21 Merge pull request diffblue#1858 from danpoe/dependence-graph-fix
10b8b09 Merge pull request diffblue#2011 from thomasspriggs/final_classes
a154593 Merge pull request diffblue#2087 from danpoe/feature/small-map
7002909 More dependence graph tests
66263ea Make dependence graph merge() return true when abstract state changes
3aa6dca Control dependency computation fix
a408423 Simplified state merging in the dependence graph
0315816 Merge pull request diffblue#2180 from thomasspriggs/json_id2string
8941567 Merge pull request diffblue#2124 from smowton/smowton/feature/fallback-function-provider
cd04e70 JBMC: use simple method stubbing pass
a6b2cda Add Java simple method stubbing pass
ec1127c Lazy goto model: hook for driver program to replace or stub functions
b6a4382 Remove `id2string` from inside calls to the `json_stringt` constructor.
b673ebb Add storage of final modifier status of java classes in `java_class_typet`.
a2ad909 Small map
808dade Provide suitable diagnostics for equality-without-matching-types
89cf6fe Throw appropriate exceptions when converting constraints
2ae66c2 Produce a proper error message when catching a std::runtime_error at top level
e7b3ade Workaround for Visual Studio loss of CV qualifier bug
1f661f5 Move sharing map and sharing node unit tests to util
47463a3 Use std::size_t instead of unsigned in the sharing map
3e22217 Sharing map documentation
e54f740 Fix sharing map compiler warnings
bcc489c Move sharing map unit tests to catch
34114b8 Use a specialised endianness map for flattening

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

.travis.yml

@@ -90,17 +90,6 @@ jobs:
         - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
-    # OS X using g++
-    - stage: Test different OS/CXX/Flags
-      os: osx
-      sudo: false
-      compiler: gcc
-      cache: ccache
-      before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
-        - export PATH=$PATH:/usr/local/opt/ccache/libexec
-      env: COMPILER="ccache g++"
-
     # OS X using clang++
     - stage: Test different OS/CXX/Flags
       os: osx

regression/cbmc-java/NondetCharSequence/NondetCharSequence.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetCharSequence
+{
+  static void main()
+  {
+    CharSequence x = CProver.nondetWithNull();
+    assert x == null || x instanceof CharSequence;
+  }
+}

regression/cbmc-java/NondetCharSequence/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetCharSequence.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetString/NondetString.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetString
+{
+  static void main()
+  {
+    String x = CProver.nondetWithNull();
+    assert x == null || x instanceof String;
+  }
+}

regression/cbmc-java/NondetString/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetString.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuffer
+{
+  static void main()
+  {
+    StringBuffer x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuffer;
+  }
+}

regression/cbmc-java/NondetStringBuffer/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetStringBuffer.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuilder
+{
+  static void main()
+  {
+    StringBuilder x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuilder;
+  }
+}

regression/cbmc-java/NondetStringBuilder/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetStringBuilder.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

@@ -3,7 +3,7 @@ NullPointer3.class
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^.*Throw null: FAILURE$
+^.*Null pointer check: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/repeated_guards/Test.java

@@ -0,0 +1,45 @@
+public class Test {
+
+  // In each of these cases a guard is repeated -- either an explicit assertion,
+  // or a guard implied by Java's semantics, e.g. that an array index is in bounds.
+  // It should be possible to violate the condition the first time, but not the second,
+  // as the program would have aborted (without --java-throw-runtime-exceptions) or a
+  // runtime exception thrown (with --java-throw-runtime-exceptions).
+
+  public static void testAssertion(boolean condition) {
+    assert(condition);
+    assert(condition);
+  }
+
+  public static void testArrayBounds(int[] array, int index) {
+    if(array == null)
+      return;
+    int got = array[index];
+    got = array[index];
+  }
+
+  public static void testClassCast(boolean unknown) {
+    A maybe_b = unknown ? new A() : new B();
+    B definitely_b = (B)maybe_b;
+    definitely_b = (B)maybe_b;
+  }
+
+  public static void testNullDeref(A maybeNull) {
+    int got = maybeNull.field;
+    got = maybeNull.field;
+  }
+
+  public static void testDivByZero(int unknown) {
+    int div = 1 / unknown;
+    div = 1 / unknown;
+  }
+
+  public static void testArrayCreation(int maybeNegative) {
+    int[] arr = new int[maybeNegative];
+    arr = new int[maybeNegative];
+  }
+
+}
+
+class A { public int field; }
+class B extends A {}

regression/cbmc-java/repeated_guards/test_arraybounds.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.testArrayBounds
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-index-out-of-bounds-low\.1.*: FAILURE$
+array-index-out-of-bounds-low\.2.*: SUCCESS$
+array-index-out-of-bounds-high\.1.*: FAILURE$
+array-index-out-of-bounds-high\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_arraycreation.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testArrayCreation
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-create-negative-size\.1.*: FAILURE$
+array-create-negative-size\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_assertion.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 10.*: FAILURE$
+assertion at file Test\.java line 11.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_classcast.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testClassCast
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+bad-dynamic-cast\.1.*: FAILURE$
+bad-dynamic-cast\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_divbyzero.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testDivByZero
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+integer-divide-by-zero\.1.*: FAILURE$
+integer-divide-by-zero\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_nullderef.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testNullDeref
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+testNullDeref:\(LA;\)V\.null-pointer-exception\.1.*: FAILURE$
+testNullDeref:\(LA;\)V\.null-pointer-exception\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc/reachability-slice-interproc/test.c

@@ -0,0 +1,76 @@
+#include <assert.h>
+
+// After a reachability slice based on the assertion in `target`, we should
+// retain both its possible callers (...may_call_target_1, ...may_call_target_2)
+// and their callees, but should be more precise concerning before_target and
+// after_target, which even though they are also called by
+// `unreachable_calls_before_target` and `unreachable_calls_after_target`, those
+// functions are not reachable.
+
+void before_target()
+{
+  const char *local = "before_target_kept";
+}
+
+void after_target()
+{
+  const char *local = "after_target_kept";
+}
+
+void target()
+{
+  const char *local = "target_kept";
+
+  before_target();
+  assert(0);
+  after_target();
+}
+
+void unreachable_calls_before_target()
+{
+  const char *local = "unreachable_calls_before_target_kept";
+  before_target();
+}
+
+void unreachable_calls_after_target()
+{
+  const char *local = "unreachable_calls_after_target_kept";
+  after_target();
+}
+
+void reachable_before_target_caller_1()
+{
+  const char *local = "reachable_before_target_caller_1_kept";
+}
+
+void reachable_after_target_caller_1()
+{
+  const char *local = "reachable_after_target_caller_1_kept";
+}
+
+void reachable_may_call_target_1()
+{
+  const char *local = "reachable_may_call_target_1_kept";
+  reachable_before_target_caller_1();
+  target();
+  reachable_after_target_caller_1();
+}
+
+void reachable_before_target_caller_2()
+{
+  const char *local = "reachable_before_target_caller_2_kept";
+}
+
+void reachable_after_target_caller_2()
+{
+  const char *local = "reachable_after_target_caller_2_kept";
+}
+
+void reachable_may_call_target_2()
+{
+  const char *local = "reachable_may_call_target_2_kept";
+  reachable_before_target_caller_2();
+  target();
+  reachable_after_target_caller_2();
+}
+

regression/cbmc/reachability-slice-interproc/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--reachability-slice-fb --show-goto-functions
+target_kept
+reachable_before_target_caller_1_kept
+reachable_after_target_caller_1_kept
+reachable_may_call_target_1_kept
+reachable_before_target_caller_2_kept
+reachable_after_target_caller_2_kept
+reachable_may_call_target_2_kept
+--
+unreachable_calls_before_target_kept
+unreachable_calls_after_target_kept

regression/cbmc/ts18661_typedefs/main.c

@@ -0,0 +1,9 @@
+typedef float _Float32;
+typedef double _Float32x;
+typedef double _Float64;
+typedef long double _Float64x;
+typedef long double _Float128;
+typedef long double _Float128x;
+
+int main(int argc, char** argv) {
+}

regression/cbmc/ts18661_typedefs/test.desc

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

regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc

@@ -10,10 +10,10 @@ replacing function pointer by 3 possible targets
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets

regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc

@@ -9,10 +9,10 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets