Squashed 'cbmc/' changes from ca5aa95..67ec6f2

67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104
fabc99e Merge pull request diffblue#1563 from NathanJPhillips/feature/lazy-loading
2d67e42 Merge pull request diffblue#1692 from NathanJPhillips/feature/numbering-at
5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212
4f4a9c7 Add at method to template_numberingt
d9cc0c0 Merge pull request diffblue#1685 from peterschrammel/remove-existing-coverage-goals
f13c871 Update a comment in instrument_cover_goals
6c39443 Remove existing coverage goals
a2cf16d Store symbol type instead of followed type when clean casting
f96efb4 Change template parameter name to not clash with existing type
b0cd57b Encapsulate lazy_goto_modelt::goto_functions
ef02f4d Update test to handle changed symbol creation order
441d269 Reset counter used by get_fresh_aux_symbol in unit tests
f759f25 Fix new test to run remove_java_new pass
cb09d8e Fix new tests to use lazy loading
166563f Do lowering of java_new as a function-level pass
3779782 Always convert the main function from bytecode into the symbol_table
7e52e22 Always allow the main function not to have a body
c938b08 Encapsulate maps in language_filest
87c6b28 Don't erase symbol in java_bytecode_convert_methodt::convert
e3e44c8 Do type-checking as a function pass
2ba1364 Update load_all_functions
5f06e36 Recreate initialize in final
aa5440b Moved call to final to lazy_goto_modelt::finalize
a659bc0 Add lazy_goto_functions_mapt
7e1ecc9 Allow post-processing functions to run on a function-by-function basis
0c05be6 Allow convert_lazy_method on functions that don't have a lazy body
05a8da2 Make goto_convert_functions not add directly to function map
c078858 Introduce lazy_goto_modelt
a22dd1c Merge pull request diffblue#1671 from thk123/bugfix/TG-1278/correct-access-level
5b6eb00 Merge pull request diffblue#1668 from romainbrenguier/bugfix/string-index-of#TG-1846
9062853 Tidied up the generic specalised class copying the base class visibility
f934ca3 String classes should be public
7b06a00 Merge pull request diffblue#1498 from smowton/smowton/feature/call_graph_improvements
f3b4c9b Test for verification of the indexOf method
9a7fa2d Correct lower bound in String indexOf
682cd1a Use a symbol generator to avoid name clashes
28a2ada Access in empty array should be unconstrained
d41403f Merge pull request diffblue#1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808
ac7e649 Use CProverString function in jbmc tests
22dc353 Add CProverString class for jbmc-strings tests
ef610b3 Use CProverString functions in strings-smoke-tests
5c716c1 Add a CProverString class for string-smoke-tests
6b619e0 Deactivate preprocessing of charAt and substring
bcfaaa4 Merge pull request diffblue#1664 from svorenova/refactoring_tg1190
c2a8bae Refactoring in specialization of generic classes
7a98e15 Rename call graph constructors
6228ed3 Slice global inits: use improved call graph
d136bbc Expose limited call graph via goto-instrument
9c29bee Improve call graph unit tests
8ed3ccb Add documentation to call graph
8f6f429 Add call graph helpers
3b06a16 Call graph: add constructors that only include reachable functions
9b65862 grapht: add get_reachable function
aaa8513 Call graph -> grapht transformation
8115248 Call graph: optionally record callsites

git-subtree-dir: cbmc
git-subtree-split: 67ec6f2

Author: smowton

regression/jbmc-strings/StaticCharMethods05/test.desc

@@ -3,7 +3,6 @@ StaticCharMethods05.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-null-pointer-exception\.14\] Throw null: FAILURE
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
 ^\[.*assertion\.2\] .* line 22 .* FAILURE$
 ^VERIFICATION FAILED$

regression/jbmc-strings/StringIndexOf/Test.class

@@ -0,0 +1,46 @@
+public class Test {
+
+    public boolean check(String input_String, char input_char, int input_int) {
+        // Verify indexOf is conform to its specification
+        int i = input_String.indexOf(input_char, input_int);
+
+        assert i < input_String.length();
+
+        int lower_bound;
+        if (input_int < 0)
+            lower_bound = 0;
+        else
+            lower_bound = input_int;
+
+        if (i == -1) {
+            for (int j = lower_bound; j < input_String.length(); j++)
+                assert input_String.charAt(j) != input_char;
+        } else {
+            assert i >= lower_bound;
+            assert input_String.charAt(i) == input_char;
+
+            for (int j = lower_bound; j < i; j++)
+                assert input_String.charAt(j) != input_char;
+        }
+        return true;
+    }
+
+    public boolean check2() {
+        // Verification should fail, this is to check the solver does
+        // not get a contradiction
+        int i = "hello".indexOf('o', 1);
+        assert i == 4;
+        i = "hello".indexOf('h', 1);
+        assert i == -1;
+        i = "hello".indexOf('e', 4);
+        assert i == -1;
+        i = "hello".indexOf('e', 8);
+        assert i == -1;
+        i = "hello".indexOf('x', 0);
+        assert i == -1;
+        i = "hello".indexOf('h', -1000);
+        assert i == 0;
+        assert false;
+        return true;
+    }
+}

regression/jbmc-strings/StringIndexOf/Test.java

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/jbmc-strings/StringIndexOf/test.desc

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 32 .* SUCCESS
+assertion at file Test.java line 34 .* SUCCESS
+assertion at file Test.java line 36 .* SUCCESS
+assertion at file Test.java line 38 .* SUCCESS
+assertion at file Test.java line 40 .* SUCCESS
+assertion at file Test.java line 42 .* SUCCESS
+assertion at file Test.java line 43 .* FAILURE
+^VERIFICATION FAILED$
+--

regression/jbmc-strings/StringIndexOf/test2.desc

@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/jbmc-strings/StringIndexOf/test_thorough.desc

@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
                 // Contradiction with the previous condition (should fail).
                 assert "foo".lastIndexOf("") != 3;
             } else if (i == 2 && input_String2.length() > 0) {
-                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
                 if (input_String2.length() == 0)
                     assert lio == fromIndex;
             } else if (i == 3) {

regression/jbmc-strings/StringLastIndexOf/Test.class

@@ -8,19 +8,19 @@ public static char[] toCharArray(String s)
         char arr[]=new char[s.length()];
         // We limit arbitrarly the loop unfolding to 10
         for(int i=0; i<length && i<10; i++)
-            arr[i]=s.charAt(i);
+            arr[i]=org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
     public static void main(String[] args)
     {
         String s1 = "diffblue";
         String s2 = "TESTGENERATION";
-        String s3 = "	automated   ";
+        String s3 = "   automated   ";
 
         assert s1.equals("diffblue");
         assert s2.equals("TESTGENERATION");
-        assert s3.equals("   automated	 ");
+        assert s3.equals("   automated   ");
 
         System.out.printf(
           "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
         int i=0;
         for (char character : charArray)
         {
-            assert character=="diffblue".charAt(i);
+            assert character==org.cprover.CProverString.charAt("diffblue", i);
             ++i;
         }