21 if(parameters.empty())
24 if(parameters.size()!=2 &&
28 error() <<
"main expected to have no or two or three parameters" <<
eom;
34 const exprt &op0=
static_cast<const exprt &
>(parameters[0]);
35 const exprt &op1=
static_cast<const exprt &
>(parameters[1]);
41 argc_symbol.
name=
"argc'";
46 if(argc_symbol.
type.
id()!=ID_signedbv &&
47 argc_symbol.
type.
id()!=ID_unsignedbv)
50 error() <<
"argc argument expected to be integer type, but got `" 59 if(op1.
type().
id()!=ID_pointer ||
63 error() <<
"argv argument expected to be pointer-to-pointer type, " 77 exprt size_expr(ID_plus, argc_new_symbol->
type);
79 argv_type.
add(ID_size).
swap(size_expr);
84 argv_symbol.
name=
"argv'";
85 argv_symbol.
type=argv_type;
93 if(parameters.size()==3)
97 envp_symbol.
name=
"envp'";
98 envp_symbol.
type=(
static_cast<const exprt&
>(parameters[2])).type();
101 symbolt envp_size_symbol, *envp_new_size_symbol;
103 envp_size_symbol.
name=
"envp_size'";
106 move_symbol(envp_size_symbol, envp_new_size_symbol);
108 if(envp_symbol.
type.
id()!=ID_pointer)
111 error() <<
"envp argument expected to be pointer type, but got `" 118 envp_symbol.
type.
id(ID_array);
The type of an expression.
irep_idt name
The unique identifier.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
void copy_to_operands(const exprt &expr)
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)
virtual std::string to_string(const exprt &expr)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
ANSI-C Language Type Checking.
source_locationt source_location
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
Base class for all expressions.
void add_argc_argv(const symbolt &main_symbol)
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
irept & add(const irep_namet &name)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const typet & subtype() const