Go to the documentation of this file.
26 if(code.
id()!=ID_code)
37 if(statement==ID_expression)
39 else if(statement==ID_label)
41 else if(statement==ID_switch_case)
43 else if(statement==ID_gcc_switch_case_range)
45 else if(statement==ID_block)
47 else if(statement==ID_decl_block)
50 else if(statement==ID_ifthenelse)
52 else if(statement==ID_while)
54 else if(statement==ID_dowhile)
56 else if(statement==ID_for)
58 else if(statement==ID_switch)
60 else if(statement==ID_break)
62 else if(statement==ID_goto)
64 else if(statement==ID_gcc_computed_goto)
66 else if(statement==ID_continue)
68 else if(statement==ID_return)
70 else if(statement==ID_decl)
72 else if(statement==ID_assign)
74 else if(statement==ID_skip)
77 else if(statement==ID_asm)
79 else if(statement==ID_start_thread)
81 else if(statement==ID_gcc_local_label)
83 else if(statement==ID_msc_try_finally)
89 else if(statement==ID_msc_try_except)
96 else if(statement==ID_msc_leave)
101 else if(statement==ID_static_assert)
107 else if(statement==ID_CPROVER_try_catch ||
108 statement==ID_CPROVER_try_finally)
114 else if(statement==ID_CPROVER_throw)
118 else if(statement==ID_assume ||
119 statement==ID_assert)
130 error() <<
"unexpected statement: " << statement <<
eom;
154 for(std::size_t i=1; i<code.
operands().size(); i++)
161 else if(flavor==ID_msc)
173 error() <<
"assignment statement expected to have two operands"
196 if(code_op.is_not_nil())
197 new_ops.
add(std::move(code_op));
208 error() <<
"break not allowed here" <<
eom;
218 error() <<
"continue not allowed here" <<
eom;
229 error() <<
"decl expected to have 1 operand" <<
eom;
234 if(code.
op0().
id()!=ID_declaration)
237 error() <<
"decl statement expected to have declaration as operand"
247 assert(declaration.
operands().size()==2);
248 codet new_code(ID_static_assert);
258 std::list<codet> new_code;
262 for(ansi_c_declarationt::declaratorst::const_iterator
267 irep_idt identifier=d_it->get_name();
270 symbol_tablet::symbolst::const_iterator s_it=
276 error() <<
"failed to find decl symbol `" << identifier
277 <<
"' in symbol table" <<
eom;
281 const symbolt &symbol=s_it->second;
290 error() <<
"incomplete type not permitted here" <<
eom;
298 symbol.
type.
id()==ID_code ||
316 new_code.push_back(decl);
321 new_code.splice(new_code.begin(),
clean_code);
329 else if(new_code.size()==1)
331 code.
swap(new_code.front());
337 code_block.set_statement(ID_decl_block);
338 code.
swap(code_block);
344 if(type.
id()==ID_incomplete_struct ||
345 type.
id()==ID_incomplete_union)
347 else if(type.
id()==ID_array)
353 else if(type.
id()==ID_struct || type.
id()==ID_union)
359 else if(type.
id()==ID_vector)
361 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
374 error() <<
"expression statement expected to have one operand"
388 error() <<
"for expected to have four operands" <<
eom;
466 code_block.
add(std::move(code));
467 code.
swap(code_block);
487 error() <<
"switch_case expected to have two operands" <<
eom;
498 error() <<
"did not expect default label here" <<
eom;
507 error() <<
"did not expect `case' here" <<
eom;
523 error() <<
"gcc_switch_case_range expected to have three operands"
533 error() <<
"did not expect `case' here" <<
eom;
562 error() <<
"computed-goto expected to have one operand" <<
eom;
568 if(dest.
id()!=ID_dereference)
571 error() <<
"computed-goto expected to have dereferencing operand"
587 error() <<
"ifthenelse expected to have three operands" <<
eom;
596 if(cond.
id()==ID_sideeffect &&
597 cond.
get(ID_statement)==ID_assign)
599 warning(
"warning: assignment in if condition");
632 error() <<
"start_thread expected to have one operand" <<
eom;
649 warning() <<
"non-void function should return a value" <<
eom;
666 warning() <<
"function has return void ";
667 warning() <<
"but a return statement returning ";
680 error() <<
"return expected to have 0 or 1 operands" <<
eom;
690 error() <<
"switch expects two operands" <<
eom;
721 error() <<
"while expected to have two operands" <<
eom;
738 code.
body() = code_block;
754 error() <<
"do while expected to have two operands" <<
eom;
771 code.
body() = code_block;
789 static_cast<exprt&
>(code.
add(spec));
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const exprt & case_op() const
A codet representing sequential composition of program statements.
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_asm(codet &code)
const typet & subtype() const
codet representation of a switch-case, i.e. a case statement within a switch.
static code_blockt from_list(const std::list< codet > &_list)
const declaratorst & declarators() const
#define Forall_operands(it, expr)
codet representing a while statement.
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_gcc_switch_case_range(codet &code)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
The type of an expression, extends irept.
const codet & then_case() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_break(codet &code)
virtual std::string to_string(const exprt &expr)
typet type
Type of symbol.
irept & add(const irep_namet &name)
virtual void typecheck_return(codet &code)
const irept & find(const irep_namet &name) const
A codet representing the declaration of a local variable.
Base class for all expressions.
const code_whilet & to_code_while(const codet &code)
const exprt & cond() const
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
struct configt::ansi_ct ansi_c
bool get_is_static_assert() const
codet representation of an if-then-else statement.
std::list< codet > clean_code
virtual void make_constant(exprt &expr)
const codet & to_code(const exprt &expr)
const code_switch_caset & to_code_switch_case(const codet &code)
code_operandst & statements()
typet & type()
Return the type of the expression.
virtual void typecheck_continue(codet &code)
codet representation of a do while statement.
virtual void implicit_typecast_bool(exprt &expr)
source_locationt source_location
const code_gotot & to_code_goto(const codet &code)
virtual void typecheck_label(code_labelt &code)
codet representation of a goto statement.
const code_ifthenelset & to_code_ifthenelse(const codet &code)
codet representation of a label for branch targets.
virtual bool is_complete_type(const typet &type) const
const code_labelt & to_code_label(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
virtual void typecheck_expression(codet &code)
symbol_tablet & symbol_table
const code_dowhilet & to_code_dowhile(const codet &code)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_code(codet &code)
const exprt & cond() const
const codet & body() const
const irep_idt & id() const
void add(const codet &code)
virtual void typecheck_dowhile(code_dowhilet &code)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_expr(exprt &expr)
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_label() const
code_asmt & to_code_asm(codet &code)
virtual void typecheck_for(codet &code)
const exprt & value() const
exprt value
Initial value of symbol.
virtual void typecheck_decl(codet &code)
A codet representing a skip statement.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
std::map< irep_idt, source_locationt > labels_defined
codet representing a switch statement.
void set(const irep_namet &name, const irep_idt &value)
const codet & body() const
const codet & else_case() const
virtual void typecheck_assign(codet &expr)
const code_switcht & to_code_switch(const codet &code)
const irep_idt & get_destination() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
virtual void typecheck_start_thread(codet &code)
const exprt & cond() const
virtual void typecheck_ifthenelse(code_ifthenelset &code)
const code_blockt & to_code_block(const codet &code)
virtual void start_typecheck_code()
virtual void typecheck_switch_case(code_switch_caset &code)
virtual void typecheck_gcc_computed_goto(codet &code)
source_locationt & add_source_location()
const irep_idt & get_flavor() const
const codet & body() const
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
The Boolean constant true.
const irep_idt & get_statement() const
mstreamt & warning() const
void reserve_operands(operandst::size_type n)
const source_locationt & source_location() const
virtual void typecheck_gcc_local_label(codet &code)
source_locationt end_location() const
virtual void typecheck_block(code_blockt &code)
virtual void implicit_typecast(exprt &expr, const typet &type)
Data structure for representing an arbitrary statement in a program.