Merge pull request #583 from diffblue/master

Update security-scanner-support to current master

Author: peterschrammel

.travis.yml

@@ -28,6 +28,7 @@ matrix:
           packages:
             - libwww-perl
             - clang-3.7
+            - libstdc++-5-dev
             - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc

regression/cbmc-java/lazyloading1/A.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading1/B.class

@@ -0,0 +1,21 @@
+// The most basic lazy loading test: A::f is directly called, B::g should be unreachable
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A.f();
+  }
+}
+
+class A
+{
+  public static void f() {}
+}
+
+class B
+{
+  public static void g() {}
+}

regression/cbmc-java/lazyloading1/test.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading1/test.desc

@@ -0,0 +1,23 @@
+// This test checks that because A is instantiated in main and B is not,
+// A::f is reachable and B::g is not
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A a = new A();
+    a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}

regression/cbmc-java/lazyloading1/test.java

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V

regression/cbmc-java/lazyloading2/A.class

@@ -0,0 +1,30 @@
+// This test checks that because `main` has a parameter of type C, which has a field of type A,
+// A::f is considered reachable, but B::g is not.
+
+public class test
+{
+  public static void main(C c)
+  {
+    c.a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}
+
+class C
+{
+  A a;
+}
+
+class D
+{
+  B b;
+}

regression/cbmc-java/lazyloading2/B.class

@@ -4,23 +4,25 @@
 
 open LOG,"<tests.log" or die "Failed to open tests.log\n";
 
-my $ignore = 1;
+my $printed_this_test = 1;
 my $current_test = "";
 
 while (<LOG>) {
   chomp;
   if (/^Test '(.+)'/) {
     $current_test = $1;
-    $ignore = 0;
-  } elsif (1 == $ignore) {
-    next;
+    $printed_this_test = 0;
   } elsif (/\[FAILED\]\s*$/) {
-    $ignore = 1;
-    print "Failed test: $current_test\n";
-    my $outf = `sed -n '2p' $current_test/test.desc`;
-    $outf =~ s/\..*$/.out/;
-    system("cat $current_test/$outf");
-    print "\n\n";
+    if(0 == $printed_this_test) {
+      $printed_this_test = 1;
+      print "\n\n";
+      print "Failed test: $current_test\n";
+      my $outf = `sed -n '2p' $current_test/test.desc`;
+      $outf =~ s/\..*$/.out/;
+      system("cat $current_test/$outf");
+      print "\n\nFailed test.desc lines:\n";
+    }
+    print "$_\n";
   }
 }
 

regression/cbmc-java/lazyloading2/test.class

@@ -1,7 +1,7 @@
 DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
-       assembler analyses java_bytecode aa-path-symex path-symex musketeer \
-       json cegis goto-analyzer jsil symex goto-diff aa-symex clobber \
+       assembler analyses java_bytecode path-symex musketeer \
+       json cegis goto-analyzer jsil symex goto-diff clobber \
        memory-models
 
 all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir goto-diff.dir

regression/cbmc-java/lazyloading2/test.desc

@@ -56,6 +56,7 @@ class optionst;
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \
+  "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:

regression/cbmc-java/lazyloading2/test.java

@@ -544,8 +544,8 @@ bool compilet::parse(const std::string &file_name)
 
   language_filet language_file;
 
-  std::pair<language_filest::filemapt::iterator, bool>
-  res=language_files.filemap.insert(
+  std::pair<language_filest::file_mapt::iterator, bool>
+  res=language_files.file_map.insert(
     std::pair<std::string, language_filet>(file_name, language_file));
 
   language_filet &lf=res.first->second;
@@ -736,7 +736,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // so we remove it from the list afterwards
-  language_files.filemap.erase(file_name);
+  language_files.file_map.erase(file_name);
   return false;
 }
 

regression/cbmc-java/lazyloading3/A.class

@@ -75,8 +75,8 @@ bool get_goto_modelt::operator()(const std::vector<std::string> &files)
           return true;
         }
 
-        std::pair<language_filest::filemapt::iterator, bool>
-          result=language_files.filemap.insert(
+        std::pair<language_filest::file_mapt::iterator, bool>
+          result=language_files.file_map.insert(
             std::pair<std::string, language_filet>(filename, language_filet()));
 
         language_filet &lf=result.first->second;

regression/cbmc-java/lazyloading3/B.class

@@ -339,7 +339,8 @@ void remove_virtual_functionst::get_functions(
     component_name,
     functions);
 
-  functions.push_back(root_function);
+  if(root_function.symbol_expr!=symbol_exprt())
+    functions.push_back(root_function);
 }
 
 /*******************************************************************\