diff --git a/regression/Makefile b/regression/Makefile index ff713b428e4..d47df3994cc 100644 --- a/regression/Makefile +++ b/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 \ diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 555f7b0e61f..df26ad98dbe 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 289e8a47efc..ca5f55d51a2 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index be4945b25ef..7685cf4284a 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index 630e54eb224..63ff98c10ad 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 2e862045758..b22b6666f14 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/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$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index b0b25cc9903..a3939c6a78a 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/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$ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f7aab087027..be77888ad47 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1482,6 +1482,7 @@ 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" @@ -1489,6 +1490,8 @@ void goto_instrument_parse_optionst::help() " --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" diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index d55afbe91a1..b329a41ddbc 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/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; } diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 508fb4fda6d..fe227986a71 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/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( diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp index 8261bb087ea..b030cbaa312 100644 --- a/src/goto-programs/replace_java_nondet.cpp +++ b/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); } - diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 36b98dc0ccd..bf41076d84c 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + bool java_is_array_type(const typet &type) { if(type.id()!=ID_struct) diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 59405c9f9c6..ed26fe1caf6 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -6,15 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include -#include - -#include "java_bytecode_parse_tree.h" #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H -#include +#include +#include +#include bool java_is_array_type(const typet &type); diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 2ce6dee37aa..d094dbd8523 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; -class namespacet; - class pointer_logict { public: diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 2a5b4ffa786..01dacc19048 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/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()));