Go to the documentation of this file.
29 main_arguments.resize(parameters.size());
31 for(std::size_t param_number=0;
32 param_number<parameters.size();
45 object_factory_parameters);
48 return main_arguments;
56 bool has_return_value=
62 codet output(ID_output);
76 init_code.
add(std::move(output));
82 for(
const auto &p : parameters)
84 if(p.get_identifier().empty())
87 irep_idt identifier=p.get_identifier();
91 if(symbol.
type.
id()==ID_pointer)
93 codet output(ID_output);
104 init_code.
add(std::move(output));
127 std::list<irep_idt> matches;
132 symbol_tablet::symbolst::const_iterator s_it=
133 symbol_table.
symbols.find(it->second);
135 if(s_it==symbol_table.
symbols.end())
138 if(s_it->second.type.id()==ID_code)
139 matches.push_back(it->second);
150 if(matches.size()>=2)
158 main_symbol=matches.front();
164 symbol_tablet::symbolst::const_iterator s_it=
165 symbol_table.
symbols.find(main_symbol);
167 if(s_it==symbol_table.
symbols.end())
170 const symbolt &symbol=s_it->second;
184 symbol, symbol_table, message_handler, object_factory_parameters);
211 symbol_tablet::symbolst::const_iterator init_it=
214 if(init_it==symbol_table.
symbols.end())
225 init_code.
add(std::move(call_init));
237 return_symbol.
mode=ID_C;
239 return_symbol.
name=
"return'";
243 symbol_table.
add(return_symbol);
250 if(symbol.
name==ID_main)
252 if(parameters.empty())
256 else if(parameters.size()==2 || parameters.size()==3)
270 init_code.
add(std::move(assumption));
284 init_code.
add(std::move(assumption));
289 codet input(ID_input);
294 init_code.
add(std::move(input));
297 if(parameters.size()==3)
304 if(envp_size_symbol.
type.
id()==ID_signedbv)
308 else if(envp_size_symbol.
type.
id()==ID_unsignedbv)
318 envp_size_symbol.
symbol_expr(), ID_le, max_minus_one);
321 init_code.
add(std::move(assumption));
354 index_expr.set(
"bounds_check",
false);
359 if(parameters.size()==3)
371 index_expr.set(
"bounds_check",
false);
376 init_code.
add(std::move(assumption2));
382 if(parameters.size()==3)
387 exprt &op0=operands[0];
388 exprt &op1=operands[1];
393 const exprt &arg1=parameters[1];
403 index_expr.
set(
"bounds_check",
false);
409 if(parameters.size()==3)
412 exprt &op2=operands[2];
414 const exprt &arg2=parameters[2];
434 parameters, init_code, symbol_table, object_factory_parameters);
437 init_code.
add(std::move(call_main));
451 if(!symbol_table.
insert(std::move(new_symbol)).second)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
#define PRECONDITION(CONDITION)
const typet & subtype() const
const symbol_base_mapt & symbol_base_map
std::vector< parametert > parameterst
typet type
Type of symbol.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Internally generated symbol table entry.
struct configt::ansi_ct ansi_c
bitvector_typet index_type()
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
#define UNREACHABLE
This should be used to mark dead code.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
const irep_idt & get_base_name() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
void static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location)
The null pointer constant.
const std::string & id2string(const irep_idt &d)
codet representation of a label for branch targets.
An assumption, which must hold in subsequent code.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INITIALIZE_FUNCTION
virtual void set_message_handler(message_handlert &_message_handler)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
std::vector< exprt > operandst
void add(const codet &code)
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.
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
mp_integer largest() const
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
exprt value
Initial value of symbol.
A codet representing a skip statement.
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)
Creates a symbol and generates code so that it can vary over all possible values for its type.
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
A base class for relations, i.e., binary predicates.
#define forall_symbol_base_map(it, expr, base_name)
mp_integer largest() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
source_locationt & add_source_location()
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A codet representing an assignment in the program.
const source_locationt & source_location() const
irep_idt name
The unique identifier.
Data structure for representing an arbitrary statement in a program.