33 main_arguments.resize(parameters.size());
35 for(std::size_t param_number=0;
36 param_number<parameters.size();
49 object_factory_parameters,
53 return main_arguments;
61 bool has_return_value =
76 for(
const auto &p : parameters)
78 if(p.get_identifier().empty())
81 irep_idt identifier=p.get_identifier();
85 if(symbol.
type.
id()==ID_pointer)
87 codet output(ID_output);
98 init_code.
add(std::move(output));
121 std::list<irep_idt> matches;
123 for(
const auto &symbol_name_entry :
127 symbol_tablet::symbolst::const_iterator s_it =
128 symbol_table.
symbols.find(symbol_name_entry.second);
130 if(s_it==symbol_table.
symbols.end())
133 if(s_it->second.type.id()==ID_code)
134 matches.push_back(symbol_name_entry.second);
140 message.
error() <<
"main symbol '" <<
config.
main.value() <<
"' not found"
145 if(matches.size()>=2)
153 main_symbol=matches.front();
159 symbol_tablet::symbolst::const_iterator s_it=
160 symbol_table.
symbols.find(main_symbol);
162 if(s_it==symbol_table.
symbols.end())
165 const symbolt &symbol=s_it->second;
179 symbol, symbol_table, message_handler, object_factory_parameters);
206 symbol_tablet::symbolst::const_iterator init_it=
209 if(init_it==symbol_table.
symbols.end())
220 init_code.
add(std::move(call_init));
232 return_symbol.
mode=ID_C;
234 return_symbol.
name=
"return'";
238 symbol_table.
add(return_symbol);
245 if(symbol.
name==ID_main)
247 if(parameters.empty())
251 else if(parameters.size()==2 || parameters.size()==3)
259 argc_symbol.
name =
"argc'";
263 argc_symbol.
mode = ID_C;
265 auto r = symbol_table.
insert(argc_symbol);
266 if(!
r.second &&
r.first != argc_symbol)
269 message.
error() <<
"argc already exists but is not usable"
288 argv_symbol.
name =
"argv'";
289 argv_symbol.
type = argv_type;
292 argv_symbol.
mode = ID_C;
294 auto r = symbol_table.
insert(argv_symbol);
295 if(!
r.second &&
r.first != argv_symbol)
298 message.
error() <<
"argv already exists but is not usable"
315 argc_symbol.
symbol_expr(), ID_ge, std::move(zero));
326 argc_symbol.
symbol_expr(), ID_le, std::move(bound_expr));
334 if(parameters.size()==3)
338 envp_size_symbol.
base_name =
"envp_size'";
339 envp_size_symbol.
name =
"envp_size'";
342 envp_size_symbol.
mode = ID_C;
344 if(!symbol_table.
insert(std::move(envp_size_symbol)).second)
358 envp_symbol.
name =
"envp'";
362 envp_symbol.
mode = ID_C;
364 if(!symbol_table.
insert(std::move(envp_symbol)).second)
379 envp_size_symbol.
symbol_expr(), ID_le, std::move(max_minus_one));
414 index_expr.
set(ID_C_bounds_check,
false);
419 if(parameters.size()==3)
431 index_expr.
set(ID_C_bounds_check,
false);
441 if(parameters.size()==3)
446 exprt &op0=operands[0];
447 exprt &op1=operands[1];
457 index_expr.
set(ID_C_bounds_check,
false);
467 if(parameters.size()==3)
485 const std::string main_signature =
type2c(symbol.
type, ns);
488 message.
error() <<
"'main' with signature '" << main_signature
490 <<
" but expecting one of:\n"
491 <<
" int main(void)\n"
492 <<
" int main(int argc, char *argv[])\n"
493 <<
" int main(int argc, char *argv[], char *envp[])\n"
494 <<
"If this is a non-standard main entry point please "
496 <<
"entry function and use --function instead"
505 parameters, init_code, symbol_table, object_factory_parameters);
508 init_code.
add(std::move(call_main));
516 for(
const auto &symbol_table_entry : symbol_table.
symbols)
518 const symbolt &symbol = symbol_table_entry.second;
520 if(symbol.
type.
id() != ID_code)
530 init_code.
add(std::move(destructor_call));
542 if(!symbol_table.
insert(std::move(new_symbol)).second)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
exprt::operandst build_function_environment(const code_typet::parameterst ¶meters, code_blockt &init_code, symbol_tablet &symbol_table, const c_object_factory_parameterst &object_factory_parameters)
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Generate a _start function for a specific function.
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
symbol_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, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
bitvector_typet index_type()
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A base class for relations, i.e., binary predicates whose two operands have the same type.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void add(const codet &code)
A codet representing an assignment in the program.
codet representation of a function call statement.
codet representation of a label for branch targets.
A codet representing the declaration that an output of a particular description has a value which cor...
A codet representing a skip statement.
const irep_idt & get_base_name() const
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
Data structure for representing an arbitrary statement in a program.
optionalt< std::string > main
struct configt::ansi_ct ansi_c
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
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mp_integer largest() const
Return the largest value that can be represented using this type.
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
static exprt conditional_cast(const exprt &expr, const typet &type)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
#define PRECONDITION(CONDITION)
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...