41 const symbolt *init_symbol=
nullptr;
44 message.
error() <<
"Linking not done, missing " 49 if(init_symbol->
mode!=ID_C)
51 message.
error() <<
"argc/argv modelling is C specific" 56 goto_functionst::function_mapt::iterator init_entry=
60 init_entry->second.body_available());
65 assert(init_end->is_end_function());
66 assert(init_end!=init.instructions.begin());
74 if(parameters.size()!=2 &&
77 message.
warning() <<
"main expected to take 2 or 3 arguments," 78 <<
" argc/argv instrumentation skipped" 86 std::ostringstream oss;
91 <<
" unsigned next=0u;\n" 94 <<
" " CPROVER_PREFIX "thread_local static char arg_string[4096];\n" 95 <<
" for(unsigned i=0u; i<ARGC && i<" << max_argc <<
"; ++i)\n" 101 <<
" ARGV[i]=&(arg_string[next]);\n" 105 std::istringstream iss(oss.str());
111 ansi_c_language.parse(iss,
"");
115 ansi_c_language.typecheck(tmp_symbol_table,
"<built-in-library>");
126 symbol_table.
add(it->second);
129 value=it->second.value;
132 replace.
insert(
"ARGC", ns.
lookup(
"argc'").symbol_expr());
133 replace.
insert(
"ARGV", ns.
lookup(
"argv'").symbol_expr());
138 symbol_table.
add(it->second))
150 it->source_location.set_file(
"<built-in-library>");
153 init.insert_before_swap(init_end, tmp);
157 init.compute_loop_numbers();
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
#define forall_symbols(it, expr)
Initialize command line arguments.
irep_idt mode
Language mode.
Goto Programs with Functions.
std::vector< parametert > parameterst
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
preprocessort preprocessor
virtual void set_message_handler(message_handlert &_message_handler)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
function_mapt function_map
bool has_prefix(const std::string &s, const std::string &prefix)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Base class for all expressions.
const parameterst & parameters() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
bool model_argc_argv(symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned max_argc, message_handlert &message_handler)
instructionst::iterator targett