29 if(code.
id()!=ID_code)
40 if(statement==ID_expression)
42 else if(statement==ID_label)
44 else if(statement==ID_switch_case)
46 else if(statement==ID_gcc_switch_case_range)
48 else if(statement==ID_block)
50 else if(statement==ID_decl_block)
53 else if(statement==ID_ifthenelse)
55 else if(statement==ID_while)
57 else if(statement==ID_dowhile)
59 else if(statement==ID_for)
61 else if(statement==ID_switch)
63 else if(statement==ID_break)
65 else if(statement==ID_goto)
67 else if(statement==ID_gcc_computed_goto)
69 else if(statement==ID_continue)
71 else if(statement==ID_return)
73 else if(statement==ID_decl)
75 else if(statement==ID_assign)
77 else if(statement==ID_skip)
80 else if(statement==ID_asm)
82 else if(statement==ID_start_thread)
84 else if(statement==ID_gcc_local_label)
86 else if(statement==ID_msc_try_finally)
92 else if(statement==ID_msc_try_except)
99 else if(statement==ID_msc_leave)
104 else if(statement==ID_static_assert)
118 error() <<
"static assertion failed";
119 if(code.
op1().
id() == ID_string_constant)
125 else if(statement==ID_CPROVER_try_catch ||
126 statement==ID_CPROVER_try_finally)
132 else if(statement==ID_CPROVER_throw)
136 else if(statement==ID_assume ||
137 statement==ID_assert)
148 error() <<
"unexpected statement: " << statement <<
eom;
174 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
176 for(
auto &expr : op.operands())
180 else if(flavor==ID_msc)
192 error() <<
"assignment statement expected to have two operands"
215 if(code_op.is_not_nil())
216 new_ops.
add(std::move(code_op));
227 error() <<
"break not allowed here" <<
eom;
237 error() <<
"continue not allowed here" <<
eom;
248 error() <<
"decl expected to have 1 operand" <<
eom;
253 if(code.
op0().
id()!=ID_declaration)
256 error() <<
"decl statement expected to have declaration as operand"
266 codet new_code(ID_static_assert);
276 std::list<codet> new_code;
285 symbol_tablet::symbolst::const_iterator s_it=
291 error() <<
"failed to find decl symbol '" << identifier
292 <<
"' in symbol table" <<
eom;
296 const symbolt &symbol=s_it->second;
305 error() <<
"incomplete type not permitted here" <<
eom;
313 symbol.
type.
id()==ID_code ||
331 new_code.push_back(decl);
336 new_code.splice(new_code.begin(),
clean_code);
344 else if(new_code.size()==1)
346 code.
swap(new_code.front());
352 code_block.set_statement(ID_decl_block);
353 code.
swap(code_block);
359 if(type.
id() == ID_array)
365 else if(type.
id()==ID_struct || type.
id()==ID_union)
369 if(struct_union_type.is_incomplete())
372 for(
const auto &c : struct_union_type.components())
376 else if(type.
id()==ID_vector)
378 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
391 error() <<
"expression statement expected to have one operand"
405 error() <<
"for expected to have four operands" <<
eom;
483 code_block.
add(std::move(code));
484 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;
784 error() <<
"do while expected to have two operands" <<
eom;
801 code.
body() = code_block;
825 const irept &contract)
827 exprt assigns =
static_cast<const exprt &
>(contract.
find(ID_C_spec_assigns));
832 for(
const auto &curr_param : function_declarator.
parameters())
834 if(curr_param.id() == ID_declaration)
839 for(
const auto &decl : param_declaration.
declarators())
850 const exprt &assigns)
854 if(curr_op.id() != ID_symbol)
863 error() <<
"Formal parameter " << declarator.
get_name() <<
" without "
864 <<
"dereference appears in ASSIGNS clause. Assigning this "
865 <<
"parameter will never affect the state of the calling context."
866 <<
" Did you mean to write *" << declarator.
get_name() <<
"?"
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
ANSI-C Language Type Checking.
const declaratorst & declarators() const
bool get_is_static_assert() const
irep_idt get_base_name() const
irep_idt get_name() const
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_break(codet &code)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void typecheck_return(code_returnt &code)
virtual void typecheck_block(code_blockt &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_decl(codet &code)
virtual void make_constant(exprt &expr)
virtual void typecheck_assign(codet &expr)
virtual void typecheck_continue(codet &code)
symbol_tablet & symbol_table
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_gcc_local_label(codet &code)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_expression(codet &code)
virtual bool is_complete_type(const typet &type) const
virtual void typecheck_start_thread(codet &code)
virtual void typecheck_switch_case(code_switch_caset &code)
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_label(code_labelt &code)
std::map< irep_idt, source_locationt > labels_defined
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
A codet representing sequential composition of program statements.
static code_blockt from_list(const std::list< codet > &_list)
source_locationt end_location() const
void add(const codet &code)
code_operandst & statements()
A codet representing the declaration of a local variable.
codet representation of a do while statement.
const exprt & cond() const
const codet & body() const
codet representation of a switch-case, i.e. a case statement within a switch.
codet & code()
the statement to be executed when the case applies
const exprt & lower() const
lower bound of range
const exprt & upper() const
upper bound of range
codet representation of a goto statement.
const irep_idt & get_destination() const
codet representation of an if-then-else statement.
const codet & then_case() const
const exprt & cond() const
const codet & else_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() const
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
A codet representing a skip statement.
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & case_op() const
codet representing a switch statement.
const exprt & value() const
const codet & body() const
const parameterst & parameters() const
codet representing a while statement.
const exprt & cond() const
const codet & body() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
source_locationt & add_source_location()
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
void reserve_operands(operandst::size_type n)
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
irept & add(const irep_namet &name)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_namet &name, const irep_idt &value)
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
source_locationt source_location
mstreamt & warning() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_value() const
Expression to hold a symbol (variable)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
Expression Initialization.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_returnt & to_code_return(const codet &code)
const code_gotot & to_code_goto(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_switch_caset & to_code_switch_case(const codet &code)
const code_labelt & to_code_label(const codet &code)
const codet & to_code(const exprt &expr)
const code_dowhilet & to_code_dowhile(const codet &code)
const code_switcht & to_code_switch(const codet &code)
const code_blockt & to_code_block(const codet &code)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
code_asm_gcct & to_code_asm_gcc(codet &code)
code_asmt & to_code_asm(codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const string_constantt & to_string_constant(const exprt &expr)
A range is a pair of a begin and an end iterators.