diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index e9b5d0dfc5d..602b906c2af 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -547,6 +547,10 @@ The SMT solver should support the QF_AUFBV logic. .TP \fB\-\-outfile\fR filename output formula to given file +.br +If all properties are simplified to true before solving, the formula +written to \fIfilename\fR will contain only the solver header and no +assertions, and a status message is emitted to that effect. .TP \fB\-\-dump\-smt\-formula\fR filename output smt incremental formula to the given file diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 0bbf11b0de9..0d389d178e5 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -451,6 +451,10 @@ incremental solving (experimental) .TP \fB\-\-outfile\fR filename output formula to given file +.br +If all properties are simplified to true before solving, the formula +written to \fIfilename\fR will contain only the solver header and no +assertions, and a status message is emitted to that effect. .TP \fB\-\-dump\-smt\-formula\fR filename output smt incremental formula to the given file diff --git a/regression/cbmc/empty-formula-warning-no-properties/main.c b/regression/cbmc/empty-formula-warning-no-properties/main.c new file mode 100644 index 00000000000..f8b643afbf2 --- /dev/null +++ b/regression/cbmc/empty-formula-warning-no-properties/main.c @@ -0,0 +1,4 @@ +int main() +{ + return 0; +} diff --git a/regression/cbmc/empty-formula-warning-no-properties/test.desc b/regression/cbmc/empty-formula-warning-no-properties/test.desc new file mode 100644 index 00000000000..8e04408caa0 --- /dev/null +++ b/regression/cbmc/empty-formula-warning-no-properties/test.desc @@ -0,0 +1,7 @@ +CORE no-new-smt +main.c +--smt2 --outfile formula.smt2 +^EXIT=0$ +^SIGNAL=0$ +-- +will not contain any assertions diff --git a/regression/cbmc/empty-formula-warning-with-vccs/main.c b/regression/cbmc/empty-formula-warning-with-vccs/main.c new file mode 100644 index 00000000000..3e0b961ed50 --- /dev/null +++ b/regression/cbmc/empty-formula-warning-with-vccs/main.c @@ -0,0 +1,7 @@ +#include +int main() +{ + int x; + assert(x == 5); + return 0; +} diff --git a/regression/cbmc/empty-formula-warning-with-vccs/test.desc b/regression/cbmc/empty-formula-warning-with-vccs/test.desc new file mode 100644 index 00000000000..8e04408caa0 --- /dev/null +++ b/regression/cbmc/empty-formula-warning-with-vccs/test.desc @@ -0,0 +1,7 @@ +CORE no-new-smt +main.c +--smt2 --outfile formula.smt2 +^EXIT=0$ +^SIGNAL=0$ +-- +will not contain any assertions diff --git a/regression/cbmc/empty-formula-warning/main.c b/regression/cbmc/empty-formula-warning/main.c new file mode 100644 index 00000000000..0d7dde8eddb --- /dev/null +++ b/regression/cbmc/empty-formula-warning/main.c @@ -0,0 +1,7 @@ +#include +int main() +{ + int x = 5; + assert(x == 5); + return 0; +} diff --git a/regression/cbmc/empty-formula-warning/test.desc b/regression/cbmc/empty-formula-warning/test.desc new file mode 100644 index 00000000000..fc4844b407d --- /dev/null +++ b/regression/cbmc/empty-formula-warning/test.desc @@ -0,0 +1,7 @@ +CORE no-new-smt paths-lifo-expected-failure +main.c +--smt2 --outfile formula.smt2 +^EXIT=0$ +^SIGNAL=0$ +will not contain any assertions +-- diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6548067d791..4f7dc8adf40 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -675,12 +675,31 @@ int cbmc_parse_optionst::doit() stop_on_fail_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); + // Note: we do not emit the "empty formula" usability warning here. + // Under --paths the equation is rebuilt per path and the outfile is + // overwritten on each non-empty path, so a per-path notion of "the + // formula is empty" does not correspond to anything the user can + // observe in the final file. } else { stop_on_fail_verifiert verifier( options, ui_message_handler, goto_model); (void)verifier(); + + // If symex generated VCCs but simplification reduced them all to true, + // the formula written via --outfile contains only the solver header + // and no assertions. Tell the user why the file is nearly empty. + const std::string outfile = options.get_option("outfile"); + if( + !outfile.empty() && verifier.get_checker().get_total_vccs() > 0 && + verifier.get_checker().get_remaining_vccs() == 0) + { + log.status() << "All properties were simplified to true before " + "solving. The formula written to " + << outfile << " will not contain any assertions." + << messaget::eom; + } } return CPROVER_EXIT_SUCCESS; diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h index b8e8b3ab116..3aeeed6aea3 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -29,6 +29,22 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert resultt operator()(propertiest &) override; + /// Returns the total number of VCCs generated by symex, before + /// simplification. + std::size_t get_total_vccs() const + { + return symex.get_total_vccs(); + } + + /// Returns the number of VCCs remaining after simplification (i.e. those + /// still to be discharged by a solver). When this is zero but + /// \ref get_total_vccs returns a positive value, all properties were + /// simplified to true and there is nothing for the solver to do. + std::size_t get_remaining_vccs() const + { + return symex.get_remaining_vccs(); + } + protected: abstract_goto_modelt &goto_model; symbol_tablet symex_symbol_table; diff --git a/src/goto-checker/stop_on_fail_verifier.h b/src/goto-checker/stop_on_fail_verifier.h index f6a26a60132..450c7021c8c 100644 --- a/src/goto-checker/stop_on_fail_verifier.h +++ b/src/goto-checker/stop_on_fail_verifier.h @@ -74,6 +74,14 @@ class stop_on_fail_verifiert : public goto_verifiert incremental_goto_checker.report(); } + /// Returns the underlying incremental goto checker. Useful for callers that + /// need to query checker-specific state after verification, e.g. VCC counts + /// when deciding whether to emit a usability warning. + const incremental_goto_checkerT &get_checker() const + { + return incremental_goto_checker; + } + protected: abstract_goto_modelt &goto_model; incremental_goto_checkerT incremental_goto_checker;