31 const std::string &file_name,
33 : ns(goto_model.symbol_table),
34 goto_model(goto_model),
35 symbol_table(goto_model.symbol_table),
36 goto_functions(goto_model.goto_functions),
37 message_handler(message_handler)
61 " matches more than one function");
76 " matches no function");
81 std::string function_name,
124 std::ostringstream
pr;
125 pr <<
"void _fn() { while(1==1)";
126 if(!loop_contracts.
assigns.empty())
136 pr <<
" {}}" << std::endl;
138 log.
debug() <<
"Constructing fake function:\n" <<
pr.str() << log.
eom;
141 std::istringstream
is(
pr.str());
157 log.
debug() <<
"Extracted loop invariants: " <<
inv_expr.pretty() <<
"\n"
162 if(!loop_contracts.
assigns.empty())
188 log.
debug() <<
"Start to replace symbols" << log.
eom;
215 log.
debug() <<
"Start to typecheck invariants." << log.
eom;
219 "old is not allowed in loop invariants.");
228 log.
debug() <<
"Start to typecheck assigns." << log.
eom;
240 log.
debug() <<
"Start to typecheck decreases." << log.
eom;
245 std::vector<exprt>();
255 log.
debug() <<
"Mangling finished." << log.
eom;
276 if(!function.is_object())
284 if(!items.is_array())
289 function_config.
regex_str = function_name;
296 std::string loop_id =
"";
346 if(symbol ==
nullptr)
349 "\" does not exist in the symbol table");
366 "loop entry must have one identifier");
372 "loop entry must have one invariant string");
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
pointer_typet pointer_type(const typet &subtype)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
ansi_c_parse_treet parse_tree
virtual void clear() override
virtual bool parse() override
std::vector< parametert > parameterst
symbol_tablet & symbol_table
message_handlert & message_handler
void configure_functions(const jsont &)
void add_builtin_pointer_function_symbol(std::string function_name, const std::size_t num_of_args)
Add builtin function symbol with function_name into symbol table.
contracts_wranglert(goto_modelt &goto_model, const std::string &file_name, message_handlert &message_handler)
void mangle(const loop_contracts_clauset &loop_contracts, const irep_idt &function_id)
Mangle loop_contracts in the function with function_id
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Class that provides messages with a built-in verbosity 'level'.
message_handlert & get_message_handler()
void set_file(const irep_idt &file)
void set_line_no(unsigned _line_no)
Expression to hold a symbol (variable)
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The Boolean constant true.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Parse and annotate contracts.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
unchecked_replace_symbolt replace_symbol
Loop id used to identify loops.
void annotate_decreases(const std::map< loop_idt, std::vector< exprt > > &decreases_map, goto_modelt &goto_model)
Annotate the decreases in decreases_map to their corresponding loops.
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.
std::map< loop_idt, exprt > invariant_mapt