Go to the documentation of this file.
28 if(code.
id()!=ID_code)
39 if(statement==ID_expression)
41 else if(statement==ID_label)
43 else if(statement==ID_switch_case)
45 else if(statement==ID_gcc_switch_case_range)
47 else if(statement==ID_block)
49 else if(statement==ID_decl_block)
52 else if(statement==ID_ifthenelse)
54 else if(statement==ID_while)
56 else if(statement==ID_dowhile)
58 else if(statement==ID_for)
60 else if(statement==ID_switch)
62 else if(statement==ID_break)
64 else if(statement==ID_goto)
66 else if(statement==ID_gcc_computed_goto)
68 else if(statement==ID_continue)
70 else if(statement==ID_return)
72 else if(statement==ID_decl)
74 else if(statement==ID_assign)
76 else if(statement==ID_skip)
79 else if(statement==ID_asm)
81 else if(statement==ID_start_thread)
83 else if(statement==ID_gcc_local_label)
85 else if(statement==ID_msc_try_finally)
91 else if(statement==ID_msc_try_except)
98 else if(statement==ID_msc_leave)
103 else if(statement==ID_static_assert)
117 error() <<
"static assertion failed";
118 if(code.
op1().
id() == ID_string_constant)
124 else if(statement==ID_CPROVER_try_catch ||
125 statement==ID_CPROVER_try_finally)
131 else if(statement==ID_CPROVER_throw)
135 else if(statement==ID_assume ||
136 statement==ID_assert)
147 error() <<
"unexpected statement: " << statement <<
eom;
173 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
175 for(
auto &expr : op.operands())
179 else if(flavor==ID_msc)
191 error() <<
"assignment statement expected to have two operands"
214 if(code_op.is_not_nil())
215 new_ops.
add(std::move(code_op));
226 error() <<
"break not allowed here" <<
eom;
236 error() <<
"continue not allowed here" <<
eom;
247 error() <<
"decl expected to have 1 operand" <<
eom;
252 if(code.
op0().
id()!=ID_declaration)
255 error() <<
"decl statement expected to have declaration as operand"
265 codet new_code(ID_static_assert);
275 std::list<codet> new_code;
284 symbol_tablet::symbolst::const_iterator s_it=
290 error() <<
"failed to find decl symbol '" << identifier
291 <<
"' in symbol table" <<
eom;
295 const symbolt &symbol=s_it->second;
304 error() <<
"incomplete type not permitted here" <<
eom;
312 symbol.
type.
id()==ID_code ||
330 new_code.push_back(decl);
335 new_code.splice(new_code.begin(),
clean_code);
343 else if(new_code.size()==1)
345 code.
swap(new_code.front());
351 code_block.set_statement(ID_decl_block);
352 code.
swap(code_block);
358 if(type.
id() == ID_array)
364 else if(type.
id()==ID_struct || type.
id()==ID_union)
368 if(struct_union_type.is_incomplete())
371 for(
const auto &c : struct_union_type.components())
375 else if(type.
id()==ID_vector)
377 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
390 error() <<
"expression statement expected to have one operand"
404 error() <<
"for expected to have four operands" <<
eom;
482 code_block.
add(std::move(code));
483 code.
swap(code_block);
504 error() <<
"switch_case expected to have two operands" <<
eom;
515 error() <<
"did not expect default label here" <<
eom;
524 error() <<
"did not expect `case' here" <<
eom;
541 error() <<
"did not expect `case' here" <<
eom;
571 error() <<
"computed-goto expected to have one operand" <<
eom;
577 if(dest.
id()!=ID_dereference)
580 error() <<
"computed-goto expected to have dereferencing operand"
594 error() <<
"ifthenelse expected to have three operands" <<
eom;
603 if(cond.
id()==ID_sideeffect &&
604 cond.
get(ID_statement)==ID_assign)
606 warning(
"warning: assignment in if condition");
639 error() <<
"start_thread expected to have one operand" <<
eom;
659 warning() <<
"function has return void ";
660 warning() <<
"but a return statement returning ";
676 warning() <<
"non-void function should return a value" <<
eom;
712 for(
auto &statement : body_block.
statements())
714 if(statement.get_statement() == ID_switch_case)
716 else if(statement.get_statement() == ID_decl)
718 if(statement.operands().size() == 1)
721 wrapping_block.
statements().back().swap(statement);
726 wrapping_block.
add(statement);
727 wrapping_block.
statements().back().operands().pop_back();
728 statement.set_statement(ID_assign);
735 wrapping_block.
add(std::move(code));
736 code.
swap(wrapping_block);
751 error() <<
"while expected to have two operands" <<
eom;
768 code.
body() = code_block;
785 error() <<
"do while expected to have two operands" <<
eom;
802 code.
body() = code_block;
818 for(
auto &invariant :
835 for(
auto &decreases_clause_component :
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)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
codet representation of a switch-case, i.e. a case statement within a switch.
ANSI-CC Language Type Checking.
static code_blockt from_list(const std::list< codet > &_list)
virtual void typecheck_spec_loop_invariant(codet &code)
const declaratorst & declarators() const
codet representing a while statement.
virtual void typecheck_while(code_whilet &code)
codet representation of an inline assembler statement.
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.
ANSI-C Language Type Checking.
const codet & then_case() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const exprt & upper() const
upper bound of range
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)
const irept & find(const irep_namet &name) const
A codet representing the declaration of a local variable.
const string_constantt & to_string_constant(const exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
Base class for all expressions.
const code_whilet & to_code_while(const codet &code)
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & cond() const
struct configt::ansi_ct ansi_c
bool get_is_static_assert() const
codet representation of an if-then-else statement.
bool is_false() const
Return whether the expression is a constant representing false.
const exprt & lower() const
lower bound of range
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 typecheck_asm(code_asmt &code)
virtual void implicit_typecast_bool(exprt &expr)
codet & code()
the statement to be executed when the case applies
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.
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
virtual void typecheck_spec_decreases(codet &code)
virtual bool is_complete_type(const typet &type) const
A range is a pair of a begin and an end iterators.
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
Ranges: pair of begin and end iterators, which can be initialized from containers,...
const code_returnt & to_code_return(const codet &code)
void add(const codet &code)
code_asm_gcct & to_code_asm_gcc(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_return(code_returnt &code)
virtual void typecheck_dowhile(code_dowhilet &code)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
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
bool has_return_value() const
exprt value
Initial value of symbol.
virtual void typecheck_decl(codet &code)
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
A codet representing a skip statement.
codet representation of a "return from a function" 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 symbolst & symbols
Read-only field, used to look up symbols given their names.
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
Semantic type conversion.
const exprt & return_value() const
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)
const irep_idt & get_value() const
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.