31 if(exp.
id() != ID_symbol)
46 if(ins->is_function_call())
48 const auto &
function = ins->call_function();
50 if(
function.
id() != ID_symbol)
53 log.
error() <<
"Function pointer used in function invoked by "
67 log.
warning() <<
"Could not find function '" << fun_name
71 if(called_fun->second.body_available())
78 log.
warning() <<
"No body for function: " << fun_name
101 if(ins->is_function_call())
103 const auto &
function = ins->call_function();
105 if(
function.
id() == ID_symbol)
121 requires_visitor(requires);
131 ensures_visitor(ensures);
146 log.
debug() <<
"Creating declarations: \n" << decl_string <<
"\n";
148 std::istringstream iss(decl_string);
154 ansi_c_language.
parse(iss,
"");
158 ansi_c_language.
typecheck(tmp_symbol_table,
"<built-in-library>");
170 for(
const auto &symbol_pair : tmp_symbol_table.
symbols)
210 const std::string &fn_name,
217 as_const(*ins).call_arguments().size() > 0,
218 "Function must have arguments");
234 std::stringstream ssreq, ssensure, ssmemmap;
247 std::ostringstream oss;
250 <<
"[" + cprover_prefix +
"constant_infinity_uint]; \n"
253 <<
"(void **elem, " + cprover_prefix +
"size_t size) { \n"
254 <<
" *elem = malloc(size); \n"
256 <<
"[" + cprover_prefix +
"POINTER_OBJECT(*elem)]) return 0; \n"
258 <<
"POINTER_OBJECT(*elem)] = 1; \n"
263 <<
"(void *elem, " + cprover_prefix +
"size_t size) { \n"
265 <<
"[" + cprover_prefix +
"POINTER_OBJECT(elem)] && "
266 << cprover_prefix +
"r_ok(elem, size)); \n"
268 <<
"POINTER_OBJECT(elem)] = 1; \n"
302 std::stringstream ssreq, ssensure, ssmemmap;
303 ssreq <<
fun_id <<
"_call_requires_is_fresh";
307 ssensure <<
fun_id <<
"_call_ensures_is_fresh";
311 ssmemmap <<
fun_id <<
"_memory_map";
317 std::ostringstream oss;
320 <<
"[" + cprover_prefix +
"constant_infinity_uint]; \n"
323 <<
"(void *elem, " + cprover_prefix +
"size_t size) { \n"
324 <<
" _Bool r_ok = " + cprover_prefix +
"r_ok(elem, size); \n"
326 <<
"[" + cprover_prefix +
"POINTER_OBJECT(elem)]"
327 <<
" != 0 || !r_ok) return 0; \n"
329 << cprover_prefix +
"POINTER_OBJECT(elem)] = 1; \n"
334 <<
"(void **elem, " + cprover_prefix +
"size_t size) { \n"
335 <<
" *elem = malloc(size); \n"
336 <<
" return (*elem != 0); \n"
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Operator to return the address of an object.
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path) override
Array constructor from single element.
goto_functionst & get_goto_functions()
symbol_tablet & get_symbol_table()
struct configt::ansi_ct ansi_c
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett > function_set
std::set< goto_programt::targett > & is_fresh_calls()
void operator()(const goto_programt &prog)
const goto_functionst & goto_functions
std::set< irep_idt > & function_calls()
std::set< irep_idt > function_set
A collection of goto functions.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const irep_idt & id() const
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
std::string requires_fn_name
void update_requires(goto_programt &requires)
void add_declarations(const std::string &decl_string)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
is_fresh_enforcet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
virtual void create_declarations()
is_fresh_replacet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_requires_fn_call(goto_programt::targett &target)
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
message_handlert & get_message_handler()
virtual void set_message_handler(message_handlert &_message_handler)
void operator()(const exprt &exp) override
bool found_return_value()
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
typet type
Type of symbol.
const typet & subtype() const
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
std::string unique_symbol(const symbol_tablet &tbl, const std::string &original)
Predicates to specify memory footprint in function contracts.
#define UNREACHABLE
This should be used to mark dead code.
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor