37 main_arguments.resize(parameters.size());
39 for(std::size_t param_number=0;
40 param_number<parameters.size();
47 main_arguments[param_number]=
57 return main_arguments;
65 bool has_return_value=
71 codet output(ID_output);
91 for(
const auto &p : parameters)
93 if(p.get_identifier().empty())
96 irep_idt identifier=p.get_identifier();
100 if(symbol.
type.
id()==ID_pointer)
102 codet output(ID_output);
123 const std::string &standard_main,
136 std::list<irep_idt> matches;
141 symbol_tablet::symbolst::const_iterator s_it=
142 symbol_table.
symbols.find(it->second);
144 if(s_it==symbol_table.
symbols.end())
147 if(s_it->second.type.id()==ID_code)
148 matches.push_back(it->second);
159 if(matches.size()>=2)
167 main_symbol=matches.front();
170 main_symbol=standard_main;
173 symbol_tablet::symbolst::const_iterator s_it=
174 symbol_table.
symbols.find(main_symbol);
176 if(s_it==symbol_table.
symbols.end())
179 const symbolt &symbol=s_it->second;
198 symbol_tablet::symbolst::iterator init_it=
201 if(init_it==symbol_table.
symbols.end())
212 call_init.
function()=init_it->second.symbol_expr();
227 return_symbol.
mode=ID_C;
229 return_symbol.
name=
"return'";
233 symbol_table.
add(return_symbol);
240 if(symbol.
name==standard_main)
242 if(parameters.empty())
246 else if(parameters.size()==2 || parameters.size()==3)
284 codet input(ID_input);
292 if(parameters.size()==3)
299 if(envp_size_symbol.
type.
id()==ID_signedbv)
303 else if(envp_size_symbol.
type.
id()==ID_unsignedbv)
346 null.
set(ID_value, ID_NULL);
354 index_expr.set(
"bounds_check",
false);
359 if(parameters.size()==3)
366 null.
set(ID_value, ID_NULL);
374 index_expr.set(
"bounds_check",
false);
388 if(parameters.size()==3)
393 exprt &op0=operands[0];
394 exprt &op1=operands[1];
399 const exprt &arg1=parameters[1];
409 index_expr.
set(
"bounds_check",
false);
415 if(parameters.size()==3)
418 exprt &op2=operands[2];
420 const exprt &arg2=parameters[2];
464 if(symbol_table.
move(new_symbol))
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
The type of an expression.
irep_idt name
The unique identifier.
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt mode
Language mode.
void copy_to_operands(const exprt &expr)
Goto Programs with Functions.
void move_to_operands(exprt &expr)
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
bool static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
symbol_base_mapt symbol_base_map
static mstreamt & eom(mstreamt &m)
exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, bool allow_null)
Creates a symbol and generates code so that it can vary over all possible values for its type...
const irep_idt & id() const
const irep_idt & get_base_name() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt::operandst build_function_environment(const code_typet::parameterst ¶meters, code_blockt &init_code, symbol_tablet &symbol_table, message_handlert &message_handler)
#define INITIALIZE_FUNCTION
static irep_idt entry_point()
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
virtual void set_message_handler(message_handlert &_message_handler)
mp_integer largest() const
bitvector_typet index_type()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Operator to return the address of an object.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
std::vector< exprt > operandst
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
mp_integer largest() const
bool ansi_c_entry_point(symbol_tablet &symbol_table, const std::string &standard_main, message_handlert &message_handler)
#define forall_symbol_base_map(it, expr, base_name)
void set_statement(const irep_idt &statement)
Base class for all expressions.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const source_locationt & source_location() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
source_locationt & add_source_location()
A statement in a programming language.
const typet & subtype() const
const typet & return_type() const
void set(const irep_namet &name, const irep_idt &value)