120 error() <<
"static assertion failed";
150 error() <<
"unexpected statement: " << statement <<
eom;
178 for(
auto &expr : op.operands())
194 error() <<
"assignment statement expected to have two operands"
229 error() <<
"break not allowed here" <<
eom;
239 error() <<
"continue not allowed here" <<
eom;
250 error() <<
"decl expected to have 1 operand" <<
eom;
258 error() <<
"decl statement expected to have declaration as operand"
278 std::list<codet> new_code;
287 symbol_tablet::symbolst::const_iterator
s_it=
293 error() <<
"failed to find decl symbol '" << identifier
294 <<
"' in symbol table" <<
eom;
307 error() <<
"incomplete type not permitted here" <<
eom;
340 new_code.push_back(decl);
345 new_code.splice(new_code.begin(),
clean_code);
353 else if(new_code.size()==1)
355 code.
swap(new_code.front());
403 error() <<
"expression statement expected to have one operand"
417 error() <<
"for expected to have four operands" <<
eom;
528 error() <<
"switch_case expected to have two operands" <<
eom;
539 error() <<
"did not expect default label here" <<
eom;
548 error() <<
"did not expect `case' here" <<
eom;
565 error() <<
"did not expect `case' here" <<
eom;
595 error() <<
"computed-goto expected to have one operand" <<
eom;
604 error() <<
"computed-goto expected to have dereferencing operand"
618 error() <<
"ifthenelse expected to have three operands" <<
eom;
630 warning(
"warning: assignment in if condition");
663 error() <<
"start_thread expected to have one operand" <<
eom;
683 warning() <<
"function has return void ";
684 warning() <<
"but a return statement returning ";
700 warning() <<
"non-void function should return a value" <<
eom;
736 for(
auto &statement :
body_block.statements())
740 else if(statement.get_statement() ==
ID_decl)
742 if(statement.operands().size() == 1)
775 error() <<
"while expected to have two operands" <<
eom;
815 error() <<
"do while expected to have two operands" <<
eom;
868 <<
"function with possible side-effect called in target's condition"
879 error() <<
"void-typed expressions not allowed as assigns clause conditions"
890 error() <<
"side-effects not allowed in assigns clause conditions" <<
eom;
897 error() <<
"ternary expressions not allowed in assigns "
917 error() <<
"void-typed expressions not allowed as assigns clause targets"
926 "POINTER_OBJECT expression"
936 error() <<
"side-effects not allowed in assigns clause targets" <<
eom;
943 error() <<
"ternary expressions not allowed in assigns "
957 for(
auto &target : targets)
963 error() <<
"expected ID_conditional_target_group expression in assigns "
975 if(condition.is_true())
992 tmp.push_back(std::move(target));
1005 std::swap(targets,
tmp);
1012 for(
auto &invariant :
ANSI-CC Language Type Checking.
API to expression classes that are internal to the C frontend.
const conditional_target_group_exprt & to_conditional_target_group_expr(const exprt &expr)
Cast an exprt to a conditional_target_group_exprt.
void validate_expr(const shuffle_vector_exprt &value)
ANSI-C Language Type Checking.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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_block(code_blockt &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_while(code_whilet &code)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
virtual void typecheck_spec_assigns_condition(exprt &condition)
virtual void typecheck_decl(codet &code)
virtual void typecheck_spec_decreases(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_spec_assigns_target(exprt &target)
virtual void typecheck_gcc_local_label(codet &code)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
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 void typecheck_return(code_frontend_returnt &)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
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_spec_loop_invariant(codet &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
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)
code_operandst & statements()
source_locationt end_location() const
codet representation of a do while statement.
const codet & body() const
const exprt & cond() const
A codet representing the declaration of a local variable.
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & upper() const
upper bound of range
const exprt & lower() const
lower bound of range
codet & code()
the statement to be executed when the case applies
codet representation of a goto statement.
const irep_idt & get_destination() const
codet representation of an if-then-else statement.
const exprt & cond() const
const codet & else_case() const
const codet & then_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() 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.
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).
std::vector< exprt > operandst
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
irept & add(const irep_idt &name)
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
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.
Generic base class for unary expressions.
const typet & element_type() const
The type of the elements of the vector.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
const code_switch_caset & to_code_switch_case(const codet &code)
const code_gotot & to_code_goto(const codet &code)
code_asm_gcct & to_code_asm_gcc(codet &code)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
const code_dowhilet & to_code_dowhile(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_labelt & to_code_label(const codet &code)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
const code_blockt & to_code_block(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
code_asmt & to_code_asm(codet &code)
const code_switcht & to_code_switch(const codet &code)
const codet & to_code(const exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
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)