Squashed 'cbmc/' changes from 7c1de91..6fd77f4

6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders
5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs
a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return
bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class
c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix
8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly
9af7ef1 Add tests for new class_hierarchy_grapht functions
79cad15 Fix existing class hierarchy test syntax
dbac316 Add documentation to class_hierarchyt
3ecac30 Move non-graph function below graph functions
4badd8f Add useful functions to class_hierarchy_grapht
610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests
2431ac0 Doxygen formatting for dependence_graph test includes
19a1ceb factor out common call graph unit test functions into header
deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs
e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref
d00d833 Fix: several grapht functions were uncompilable if ever called
b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search
7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable
da76500 JBMC: Fixed asymmetry between synchronized blocks and methods.
5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class
d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf
91e8b89 Fix for nondet replacement on a direct return (pre-remove returns)
904132d unit tests for depth limited search on call graph
2c76d0d call graph helper interface to depth limited search
64fdb9b depht limited search for grapht
e708bfb Adds --java-load-class to tests that require it
6665c69 Remove unreachable instructions
6e4d5a7 printf does not and should not have a left-hand side
2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm
6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2
3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction
cf797da Merge pull request diffblue#2473 from tautschnig/vs-update
c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex
e504e80 Remove unused parameter in string abstraction
4d88b98 Remove unused parameter in counterexample beautification
888f168 Remove unused parameter from update_scores
461754d Remove unused parameters in goto-instrument/wmm
93300aa Use string2unsigned when reading/expecting an unsigned
1a7033a String refinement: Take a reference to avoid copy

git-subtree-dir: cbmc
git-subtree-split: 6fd77f4

Author: JohnDumbell

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class

@@ -14,6 +14,25 @@ public void me0()
     }
   }
 
+  // expected verification success
+  public static void aStatic() throws java.io.IOException
+  {
+    Object _lock = new Object();
+    try
+    {
+      synchronized (_lock)
+      {
+        if(true)
+          throw new java.io.IOException();
+      }
+    }
+    catch (java.io.IOException e)
+    {
+      return;
+    }
+    assert false; // unreachable
+  }
+
   // expected verification success
   // --
   // base-case, no synchronization

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

@@ -0,0 +1,10 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified.
+