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(
unsigned i=1; i<code.
operands().size(); i++)
161 else if(flavor==ID_msc)
173 error() <<
"assignment statement expected to have two operands" 204 codet *code_ptr=&code_op;
208 assert(code_ptr->
operands().size()==1);
209 code_ptr=&
to_code(code_ptr->op0());
228 error() <<
"break not allowed here" <<
eom;
238 error() <<
"continue not allowed here" <<
eom;
249 error() <<
"decl expected to have 1 operand" <<
eom;
254 if(code.
op0().
id()!=ID_declaration)
257 error() <<
"decl statement expected to have declaration as operand" 267 assert(declaration.
operands().size()==2);
268 codet new_code(ID_static_assert);
278 std::list<codet> new_code;
282 for(ansi_c_declarationt::declaratorst::const_iterator
287 irep_idt identifier=d_it->get_name();
290 symbol_tablet::symbolst::iterator s_it=
296 error() <<
"failed to find decl symbol `" << identifier
297 <<
"' in symbol table" <<
eom;
310 error() <<
"incomplete type not permitted here" <<
eom;
318 symbol.
type.
id()==ID_code ||
337 new_code.push_back(code);
342 new_code.splice(new_code.begin(),
clean_code);
350 else if(new_code.size()==1)
352 code.
swap(new_code.front());
359 code.
swap(code_block);
365 if(type.
id()==ID_incomplete_struct ||
366 type.
id()==ID_incomplete_union)
368 else if(type.
id()==ID_array)
374 else if(type.
id()==ID_struct || type.
id()==ID_union)
378 for(struct_union_typet::componentst::const_iterator
379 it=components.begin();
380 it!=components.end();
385 else if(type.
id()==ID_vector)
387 else if(type.
id()==ID_symbol)
398 error() <<
"expression statement expected to have one operand" 412 error() <<
"for expected to have four operands" <<
eom;
455 if(
to_code(code.
op3()).get_statement()==ID_decl_block)
474 if(
to_code(code.
op3()).get_statement()==ID_block)
491 code.
swap(code_block);
511 error() <<
"switch_case expected to have two operands" <<
eom;
522 error() <<
"did not expect default label here" <<
eom;
531 error() <<
"did not expect `case' here" <<
eom;
546 error() <<
"gcc_switch_case_range expected to have three operands" 556 error() <<
"did not expect `case' here" <<
eom;
583 error() <<
"computed-goto expected to have one operand" <<
eom;
589 if(dest.
id()!=ID_dereference)
592 error() <<
"computed-goto expected to have dereferencing operand" 608 error() <<
"ifthenelse expected to have three operands" <<
eom;
617 if(cond.
id()==ID_sideeffect &&
618 cond.
get(ID_statement)==ID_assign)
620 warning(
"warning: assignment in if condition");
657 error() <<
"start_thread expected to have one operand" <<
eom;
691 warning() <<
"function has return void ";
692 warning() <<
"but a return statement returning ";
705 error() <<
"return expected to have 0 or 1 operands" <<
eom;
715 error() <<
"switch expects two operands" <<
eom;
746 error() <<
"while expected to have two operands" <<
eom;
781 error() <<
"do while expected to have two operands" <<
eom;
818 static_cast<exprt&
>(code.
add(spec));
const irep_idt & get_statement() const
bool get_is_static_assert() const
The type of an expression.
const codet & then_case() const
std::map< irep_idt, source_locationt > labels_used
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
Linking: Zero Initialization.
virtual void typecheck_start_thread(codet &code)
A `switch' instruction.
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_declaration(ansi_c_declarationt &)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const exprt & cond() const
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_gcc_switch_case_range(codet &code)
const exprt & cond() const
const codet & body() const
void copy_to_operands(const exprt &expr)
source_locationt end_location() const
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
exprt value
Initial value of symbol.
const componentst & components() const
virtual void typecheck_switch_case(code_switch_caset &code)
A `goto' instruction.
const irep_idt & get_flavor() const
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 exprt & case_op() const
symbol_tablet & symbol_table
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const irep_idt & id() const
const declaratorst & declarators() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
virtual void typecheck_break(codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
The boolean constant true.
ANSI-C Language Type Checking.
A declaration of a local variable.
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_assign(codet &expr)
source_locationt source_location
const code_dowhilet & to_code_dowhile(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_gotot & to_code_goto(const codet &code)
virtual void typecheck_continue(codet &code)
const irep_idt & get(const irep_namet &name) const
A label for branch targets.
const exprt & size() const
virtual void typecheck_expr(exprt &expr)
void err_location(const source_locationt &loc)
A `while' instruction.
const code_switch_caset & to_code_switch_case(const codet &code)
std::list< codet > clean_code
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_asm(codet &code)
virtual void typecheck_block(codet &code)
const codet & body() const
const code_switcht & to_code_switch(const codet &code)
virtual void start_typecheck_code()
virtual void typecheck_for(codet &code)
virtual void typecheck_label(code_labelt &code)
const exprt & value() const
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
message_handlert & get_message_handler()
virtual void typecheck_gcc_local_label(codet &code)
void set_statement(const irep_idt &statement)
Base class for all expressions.
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_decl(codet &code)
A `do while' instruction.
const source_locationt & source_location() const
ANSI-CC Language Type Checking.
irept & add(const irep_namet &name)
std::map< irep_idt, source_locationt > labels_defined
#define Forall_operands(it, expr)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
virtual void implicit_typecast_arithmetic(exprt &expr)
const code_blockt & to_code_block(const codet &code)
const irep_idt & get_destination() const
A statement in a programming language.
const code_labelt & to_code_label(const codet &code)
const typet & subtype() const
const exprt & cond() const
const codet & else_case() const
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void make_typecast(const typet &_type)
const codet & body() const
const irept & find(const irep_namet &name) const
code_asmt & to_code_asm(codet &code)
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_return(codet &code)
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_expression(codet &code)