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)
109 else if(statement==ID_CPROVER_try_catch ||
110 statement==ID_CPROVER_try_finally)
116 else if(statement==ID_CPROVER_throw)
120 else if(statement==ID_assume ||
121 statement==ID_assert)
132 error() <<
"unexpected statement: " << statement <<
eom;
158 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
160 for(
auto &expr : op.operands())
164 else if(flavor==ID_msc)
176 error() <<
"assignment statement expected to have two operands"
199 if(code_op.is_not_nil())
200 new_ops.
add(std::move(code_op));
211 error() <<
"break not allowed here" <<
eom;
221 error() <<
"continue not allowed here" <<
eom;
232 error() <<
"decl expected to have 1 operand" <<
eom;
237 if(code.
op0().
id()!=ID_declaration)
240 error() <<
"decl statement expected to have declaration as operand"
250 assert(declaration.
operands().size()==2);
251 codet new_code(ID_static_assert);
261 std::list<codet> new_code;
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_array)
350 else if(type.
id()==ID_struct || type.
id()==ID_union)
354 if(struct_union_type.is_incomplete())
357 for(
const auto &c : struct_union_type.components())
361 else if(type.
id()==ID_vector)
363 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
376 error() <<
"expression statement expected to have one operand"
390 error() <<
"for expected to have four operands" <<
eom;
468 code_block.
add(std::move(code));
469 code.
swap(code_block);
489 error() <<
"switch_case expected to have two operands" <<
eom;
500 error() <<
"did not expect default label here" <<
eom;
509 error() <<
"did not expect `case' here" <<
eom;
526 error() <<
"did not expect `case' here" <<
eom;
556 error() <<
"computed-goto expected to have one operand" <<
eom;
562 if(dest.
id()!=ID_dereference)
565 error() <<
"computed-goto expected to have dereferencing operand"
579 error() <<
"ifthenelse expected to have three operands" <<
eom;
588 if(cond.
id()==ID_sideeffect &&
589 cond.
get(ID_statement)==ID_assign)
591 warning(
"warning: assignment in if condition");
624 error() <<
"start_thread expected to have one operand" <<
eom;
644 warning() <<
"function has return void ";
645 warning() <<
"but a return statement returning ";
661 warning() <<
"non-void function should return a value" <<
eom;
697 for(
auto &statement : body_block.
statements())
699 if(statement.get_statement() == ID_switch_case)
701 else if(statement.get_statement() == ID_decl)
703 if(statement.operands().size() == 1)
706 wrapping_block.
statements().back().swap(statement);
711 wrapping_block.
add(statement);
712 wrapping_block.
statements().back().operands().pop_back();
713 statement.set_statement(ID_assign);
720 wrapping_block.
add(std::move(code));
721 code.
swap(wrapping_block);
736 error() <<
"while expected to have two operands" <<
eom;
753 code.
body() = code_block;
769 error() <<
"do while expected to have two operands" <<
eom;
786 code.
body() = code_block;
810 const irept &contract)
812 exprt assigns =
static_cast<const exprt &
>(contract.
find(ID_C_spec_assigns));
817 for(
const auto &curr_param : function_declarator.
parameters())
819 if(curr_param.id() == ID_declaration)
824 for(
const auto &decl : param_declaration.
declarators())
835 const exprt &assigns)
839 if(curr_op.id() != ID_symbol)
848 error() <<
"Formal parameter " << declarator.
get_name() <<
" without "
849 <<
"dereference appears in ASSIGNS clause. Assigning this "
850 <<
"parameter will never affect the state of the calling context."
851 <<
" Did you mean to write *" << declarator.
get_name() <<
"?"
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
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)
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.
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
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
bool get_is_static_assert() const
codet representation of an if-then-else statement.
const exprt & lower() const
lower bound of range
std::list< codet > clean_code
irep_idt get_name() const
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)
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
codet representation of a do while statement.
Expression Initialization.
virtual void typecheck_asm(code_asmt &code)
irep_idt get_base_name() const
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)
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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)
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
virtual void typecheck_switch(codet &code)
const parameterst & parameters() const
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)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
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)
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.