Collection of minor fixes and cleanup

regression/Makefile

@@ -1,9 +1,9 @@
 DIRS = ansi-c \
        cbmc \
-       cpp \
+       cbmc-cover \
        cbmc-java \
        cbmc-java-inheritance \
-       cbmc-cover \
+       cpp \
        goto-analyzer \
        goto-diff \
        goto-gcc \

regression/cbmc/Quantifiers-assertion/test.desc

@@ -9,4 +9,4 @@ main.c
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
 ^\*\* 2 of 6 failed \(2 iterations\)$
-^\VERIFICATION FAILED$
+^VERIFICATION FAILED$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -7,4 +7,4 @@ main.c
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
 ^\*\* 1 of 4 failed \(2 iterations\)$
-^\VERIFICATION FAILED$
+^VERIFICATION FAILED$

regression/cbmc/Quantifiers-if/test.desc

@@ -8,4 +8,4 @@ main.c
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
 ^\*\* 3 of 5 failed \(2 iterations\)$
-^\VERIFICATION FAILED$
+^VERIFICATION FAILED$

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -9,4 +9,4 @@ main.c
 ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
 ^\*\* 0 of 6 failed \(1 iteration\)$
-^\VERIFICATION SUCCESSFUL$
+^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-not/test.desc

@@ -8,4 +8,4 @@ main.c
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
 ^\*\* 2 of 5 failed \(2 iterations\)$
-^\VERIFICATION FAILED$
+^VERIFICATION FAILED$

regression/cbmc/Quantifiers-type/test.desc

@@ -5,4 +5,4 @@ main.c
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
 ^\*\* 1 of 2 failed \(2 iterations\)$
-^\VERIFICATION FAILED$
+^VERIFICATION FAILED$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1482,13 +1482,16 @@ void goto_instrument_parse_optionst::help()
     " --show-symbol-table          show symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --print-internal-representation\n" // NOLINTNEXTLINE(*)
     "                              show verbose internal representation of the program\n"
     " --list-undefined-functions   list functions without body\n"
     " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
     " --show-natural-loops         show natural loop heads\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --list-calls-args            list all function calls with their arguments\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --print-path-lengths         print statistics about control-flow graph paths\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"

src/goto-programs/convert_nondet.cpp

@@ -67,7 +67,8 @@ static goto_programt::targett insert_nondet_init_code(
   }
 
   // Although, if the type is a ptr-to-void then we also want to bail
-  if(lhs.type().subtype().id()==ID_empty)
+  if(lhs.type().subtype().id()==ID_empty ||
+     lhs.type().subtype().id()==ID_code)
   {
     return next_instr;
   }

src/goto-programs/goto_convert_class.h

@@ -530,11 +530,6 @@ class goto_convertt:public messaget
     const exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);
-  void do_array_set(
-    const exprt &lhs,
-    const exprt &rhs,
-    const exprt::operandst &arguments,
-    goto_programt &dest);
   void do_array_equal(
     const exprt &lhs,
     const exprt &rhs,
@@ -543,7 +538,7 @@ class goto_convertt:public messaget
   void do_array_op(
     const irep_idt &id,
     const exprt &lhs,
-    const exprt &rhs,
+    const exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_printf(

src/goto-programs/replace_java_nondet.cpp

@@ -251,4 +251,3 @@ void replace_java_nondet(goto_modelt &goto_model)
 {
   replace_java_nondet(goto_model.goto_functions);
 }
-

src/java_bytecode/java_utils.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/string_utils.h>
 
+#include <set>
+
 bool java_is_array_type(const typet &type)
 {
   if(type.id()!=ID_struct)

src/java_bytecode/java_utils.h

@@ -6,15 +6,12 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/symbol_table.h>
-#include <util/message.h>
-#include <util/std_expr.h>
-
-#include "java_bytecode_parse_tree.h"
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 
-#include <util/type.h>
+#include <util/message.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 bool java_is_array_type(const typet &type);
 

src/solvers/flattening/pointer_logic.h

@@ -18,8 +18,6 @@ Author: Daniel Kroening, [email protected]
 
 class namespacet;
 
-class namespacet;
-
 class pointer_logict
 {
 public:

src/solvers/prop/bdd_expr.cpp

@@ -122,7 +122,7 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const
   }
   else if(r.high().is_false())
   {
-    if(r.high().is_true())
+    if(r.low().is_true())
       return not_exprt(n_expr);
     else
       return and_exprt(not_exprt(n_expr), as_expr(r.low()));