50 message.
error() <<
"Linking not done, missing " 59 if(main_symbol.
mode!=ID_C)
61 message.
error() <<
"argc/argv modelling is C specific" 68 if(parameters.size()!=2 &&
71 message.
warning() <<
"main expected to take 2 or 3 arguments," 72 <<
" argc/argv instrumentation skipped" 80 std::ostringstream oss;
85 <<
" unsigned next=0u;\n" 88 <<
" char arg_string[4096];\n" 89 <<
" __CPROVER_input(\"arg_string\", &arg_string[0]);\n" 90 <<
" for(int i=0; i<ARGC && i<" << max_argc <<
"; ++i)\n" 96 <<
" ARGV[i]=&(arg_string[next]);\n" 100 std::istringstream iss(oss.str());
106 ansi_c_language.parse(iss,
"");
110 ansi_c_language.typecheck(tmp_symbol_table,
"<built-in-library>");
117 for(
const auto &symbol_pair : tmp_symbol_table.
symbols)
126 value = symbol_pair.second.value;
129 replace.
insert(
"ARGC", ns.
lookup(
"argc'").symbol_expr());
130 replace.
insert(
"ARGV", ns.
lookup(
"argv'").symbol_expr());
151 it->source_location.set_file(
"<built-in-library>");
155 goto_functionst::function_mapt::iterator start_entry=
161 start_entry->second.body_available(),
162 "entry point expected to have a body");
170 if(main_call->is_function_call())
174 if(func.
id()==ID_symbol &&
181 start.insert_before_swap(main_call, init_instructions);
irep_idt name
The unique identifier.
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Initialize command line arguments.
irep_idt mode
Language mode.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
std::vector< parametert > parameterst
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
#define POSTCONDITION(CONDITION)
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
mstreamt & warning() const
preprocessort preprocessor
const irep_idt & id() const
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
bool has_prefix(const std::string &s, const std::string &prefix)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual void set_message_handler(message_handlert &_message_handler)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
static irep_idt entry_point()
Base class for all expressions.
const parameterst & parameters() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
#define DATA_INVARIANT(CONDITION, REASON)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)