67 return result_get_goto_program;
73 gcc_version.
get(
"gcc");
87 if(
cmdline.isset(
"dump-loop-contracts"))
92 std::string json_output_str =
"stdout";
93 if(
cmdline.isset(
"json-output"))
95 json_output_str =
cmdline.get_value(
"json-output");
106 log.error() <<
"failed to write to '" <<
cmdline.args[1] <<
"'";
110 goto_model, invariant_map, assigns_map, json_output_str, out);
116 goto_model, invariant_map, assigns_map, json_output_str, std::cout);
121 else if(
cmdline.isset(
"json-output"))
124 "Incompatible option detected",
125 "--json-output must be used with --dump-loop-contracts");
133 std::set<std::string> to_exclude_from_nondet_static(
134 cmdline.get_values(
"nondet-static-exclude").begin(),
135 cmdline.get_values(
"nondet-static-exclude").end());
148 goto_model.goto_functions.compute_loop_numbers();
159 log.status() <<
"Writing GOTO program to '" <<
cmdline.args[1] <<
"'"
167 else if(
cmdline.args.size() < 2)
170 "Invalid number of positional arguments passed",
172 "goto-instrument needs one input and one output file, aside from other "
182 log.status() <<
"Reading GOTO program from '" <<
cmdline.args[0] <<
"'"
189 if(!result.has_value())
204 options.
set_option(
"built-in-assertions",
true);
208 options.
set_option(
"show-goto-symex-steps",
false);
209 options.
set_option(
"show-points-to-sets",
false);
210 options.
set_option(
"show-array-constraints",
false);
211 options.
set_option(
"built-in-assertions",
true);
215 options.
set_option(
"exploration-strategy",
"lifo");
216 options.
set_option(
"symex-cache-dereferences",
false);
219 options.
set_option(
"self-loops-to-assumptions",
true);
222 if(
cmdline.isset(
"arrays-uf-always"))
224 else if(
cmdline.isset(
"arrays-uf-never"))
246 "Usage: \tPurpose:\n"
248 " {bgoto-synthesizer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
249 " {bgoto-synthesizer} {y--version} \t show version and exit\n"
250 " {bgoto-synthesizer} {uin} {uout} \t synthesize and apply loop"
255 "Accepts all of cbmc's options plus the following backend "
258 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
259 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
263 " {y--xml-ui} \t use XML-formatted output\n"
264 " {y--json-ui} \t use JSON-formatted output\n"
265 " {y--verbosity} {u#} \t verbosity level\n"
CBMC Command Line Option Processing.
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
Enumerative loop contracts synthesizers.
std::map< loop_idt, std::set< exprt > > get_assigns_map() const
invariant_mapt synthesize_all() override
This synthesizer guarantees that, with the synthesized loop contracts, all checks in the annotated GO...
void get(const std::string &executable)
void help() override
display command line help
goto_synthesizer_parse_optionst(int argc, const char **argv)
void register_languages() override
int doit() override
invoke main modules
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_option(const std::string &option, const bool value)
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
ui_message_handlert ui_message_handler
#define HELP_CONFIG_BACKEND
Verify and use annotated invariants and pre/post-conditions.
#define HELP_LOOP_CONTRACTS_NO_UNWIND
#define FLAG_LOOP_CONTRACTS_NO_UNWIND
void dump_loop_contracts(goto_modelt &goto_model, const std::map< loop_idt, exprt > &invariant_map, const std::map< loop_idt, std::set< exprt > > &assigns_map, const std::string &json_output_str, std::ostream &out)
#define HELP_DUMP_LOOP_CONTRACTS
Enumerative Loop Contracts Synthesizer.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void configure_gcc(const gcc_versiont &gcc_version)
#define GOTO_SYNTHESIZER_OPTIONS
void update_max_malloc_size(goto_modelt &goto_model, message_handlert &message_handler)
Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.
Initialize a Goto Program.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
Loop contract configurations.
#define widen_if_needed(s)
void annotate_assigns(const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.