Merge branch 'master' of github.com:diffblue/cbmc

Author: Daniel Kroening

.travis.yml

@@ -13,8 +13,10 @@ matrix:
           packages:
             - libwww-perl
             - g++-5
+            - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER=g++-5
     - os: linux
       compiler: clang
@@ -26,8 +28,10 @@ matrix:
           packages:
             - libwww-perl
             - clang-3.7
+            - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+      # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env: COMPILER=clang++-3.7
     - os: osx
       compiler: gcc
@@ -42,5 +46,5 @@ script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
     make -C src minisat2-download &&
     make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 &&
-    make -C regression test &&
-    make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 aa-symex.dir cegis.dir clobber.dir memory-models.dir musketeer.dir
+    env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test &&
+    make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 aa-symex.dir cegis.dir clobber.dir memory-models.dir musketeer.dir

regression/ansi-c/function_return1/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --verbosity 2
-^file main.c line 3 function fun: function has return void but a return statement returning signed int$
+^main.c:3:1: warning: function has return void but a return statement returning signed int$
 ^SIGNAL=0$
 
 --

regression/ansi-c/struct6/test.desc

@@ -3,6 +3,6 @@ main.c
 
 ^EXIT=\(64\|1\)$
 ^SIGNAL=0$
-^file main.c line 2: incomplete type not permitted here$
+^main.c:2:1: error: incomplete type not permitted here$
 ^CONVERSION ERROR$
 --

regression/ansi-c/struct7/test.desc

@@ -3,6 +3,6 @@ main.c
 
 ^EXIT=\(64\|1\)$
 ^SIGNAL=0$
-^file main.c line 4: duplicate member x$
+^main.c:4:1: error: duplicate member .*$
 ^CONVERSION ERROR$
 --

regression/cbmc-java/enum1/enum1.class

@@ -0,0 +1,16 @@
+public enum enum1
+{
+  VAL1, VAL2, VAL3, VAL4, VAL5;
+  static
+  {
+    for(enum1 e : enum1.values())
+    {
+      System.out.println(e);
+    }
+  }
+  public static void main(String[] args)
+  {
+    enum1 e=VAL5;
+    assert(e==VAL5);
+  }
+}

regression/cbmc-java/enum1/enum1.java

@@ -0,0 +1,8 @@
+CORE
+enum1.class
+--java-unwind-enum-static --unwind 3
+^EXIT=10$
+^SIGNAL=0$
+^Unwinding loop java::enum1.<clinit>:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.<clinit>:()V bytecode_index 78 thread 0$
+--
+^warning: ignoring

regression/cbmc-java/enum1/test.desc

@@ -918,7 +918,7 @@ void c_typecheck_baset::typecheck_compound_body(
       if(!members.insert(it->get_name()).second)
       {
         error().source_location=it->source_location();
-        error() << "duplicate member " << it->get_name() << eom;
+        error() << "duplicate member '" << it->get_name() << '\'' << eom;
         throw 0;
       }
     }

src/ansi-c/c_typecheck_type.cpp

@@ -2,7 +2,7 @@ SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \
       cbmc_languages.cpp counterexample_beautification.cpp \
       bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \
       xml_interface.cpp bmc_cover.cpp all_properties.cpp \
-      fault_localization.cpp
+      fault_localization.cpp symex_coverage.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/cbmc/Makefile

@@ -528,6 +528,15 @@ safety_checkert::resultt bmct::run(
                    << " remaining after simplification" << eom;
     }
 
+    // coverage report
+    std::string cov_out=options.get_option("symex-coverage-report");
+    if(!cov_out.empty() &&
+       symex.output_coverage_report(goto_functions, cov_out))
+    {
+      error() << "Failed to write symex coverage report" << eom;
+      return safety_checkert::ERROR;
+    }
+
     if(options.get_bool_option("show-vcc"))
     {
       show_vcc();

src/cbmc/bmc.cpp

@@ -43,6 +43,8 @@ class bmct:public safety_checkert
     ui(ui_message_handlert::PLAIN)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
+    symex.record_coverage=
+      !options.get_option("symex-coverage-report").empty();
   }
 
   virtual resultt run(const goto_functionst &goto_functions);

src/cbmc/bmc.h

@@ -434,6 +434,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("stop-on-fail", true);
     options.set_option("trace", true);
   }
+
+  if(cmdline.isset("symex-coverage-report"))
+    options.set_option(
+      "symex-coverage-report",
+      cmdline.get_value("symex-coverage-report"));
 }
 
 /*******************************************************************\
@@ -550,6 +555,8 @@ int cbmc_parse_optionst::doit()
   if(set_properties(goto_functions))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
+  // unwinds <clinit> loops to number of enum elements
+  // side effect: add this as explicit unwind to unwind set
   if(options.get_bool_option("java-unwind-enum-static"))
     remove_static_init_loops(symbol_table, goto_functions, options);
 
@@ -1084,6 +1091,7 @@ void cbmc_parse_optionst::help()
     "\n"
     "Analysis options:\n"
     " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n"
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)

src/cbmc/cbmc_parse_options.cpp

@@ -46,7 +46,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):" \
+  "(cover):(symex-coverage-report):" \
   "(mm):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \

src/cbmc/cbmc_parse_options.h

@@ -29,7 +29,9 @@ symex_bmct::symex_bmct(
   symbol_tablet &_new_symbol_table,
   symex_targett &_target):
   goto_symext(_ns, _new_symbol_table, _target),
-  max_unwind_is_set(false)
+  record_coverage(false),
+  max_unwind_is_set(false),
+  symex_coverage(_ns)
 {
 }
 
@@ -61,6 +63,10 @@ void symex_bmct::symex_step(
     last_source_location=source_location;
   }
 
+  if(record_coverage &&
+     !state.guard.is_false())
+    symex_coverage.covered(state.source.pc);
+
   goto_symext::symex_step(goto_functions, state);
 }
 

src/cbmc/symex_bmc.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-symex/goto_symex.h>
 
+#include "symex_coverage.h"
+
 class symex_bmct:
   public goto_symext,
   public messaget
@@ -49,6 +51,15 @@ class symex_bmct:
     loop_limits[id]=limit;
   }
 
+  bool output_coverage_report(
+    const goto_functionst &goto_functions,
+    const std::string &path) const
+  {
+    return symex_coverage.generate_report(goto_functions, path);
+  }
+
+  bool record_coverage;
+
 protected:
   // We have
   // 1) a global limit (max_unwind)
@@ -85,6 +96,8 @@ class symex_bmct:
   virtual void no_body(const irep_idt &identifier);
 
   std::unordered_set<irep_idt, irep_id_hash> body_warnings;
+
+  symex_coveraget symex_coverage;
 };
 
 #endif // CPROVER_CBMC_SYMEX_BMC_H