31 if(code.
id()!=ID_code)
42 if(statement==ID_expression)
44 else if(statement==ID_label)
46 else if(statement==ID_switch_case)
48 else if(statement==ID_gcc_switch_case_range)
50 else if(statement==ID_block)
52 else if(statement==ID_decl_block)
55 else if(statement==ID_ifthenelse)
57 else if(statement==ID_while)
59 else if(statement==ID_dowhile)
61 else if(statement==ID_for)
63 else if(statement==ID_switch)
65 else if(statement==ID_break)
67 else if(statement==ID_goto)
69 else if(statement==ID_gcc_computed_goto)
71 else if(statement==ID_continue)
73 else if(statement==ID_return)
75 else if(statement==ID_decl)
77 else if(statement==ID_assign)
79 else if(statement==ID_skip)
82 else if(statement==ID_asm)
84 else if(statement==ID_start_thread)
86 else if(statement==ID_gcc_local_label)
88 else if(statement==ID_msc_try_finally)
94 else if(statement==ID_msc_try_except)
101 else if(statement==ID_msc_leave)
106 else if(statement==ID_static_assert)
123 error() <<
"static assertion failed";
124 if(code.
operands().size() == 2 && code.
op1().
id() == ID_string_constant)
130 else if(statement==ID_CPROVER_try_catch ||
131 statement==ID_CPROVER_try_finally)
137 else if(statement==ID_CPROVER_throw)
141 else if(statement==ID_assume ||
142 statement==ID_assert)
153 error() <<
"unexpected statement: " << statement <<
eom;
179 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
181 for(
auto &expr : op.operands())
185 else if(flavor==ID_msc)
197 error() <<
"assignment statement expected to have two operands"
220 if(code_op.is_not_nil())
221 new_ops.
add(std::move(code_op));
232 error() <<
"break not allowed here" <<
eom;
242 error() <<
"continue not allowed here" <<
eom;
253 error() <<
"decl expected to have 1 operand" <<
eom;
258 if(code.
op0().
id()!=ID_declaration)
261 error() <<
"decl statement expected to have declaration as operand"
271 codet new_code(ID_static_assert);
281 std::list<codet> new_code;
290 symbol_table_baset::symbolst::const_iterator s_it =
296 error() <<
"failed to find decl symbol '" << identifier
297 <<
"' in symbol table" <<
eom;
301 const symbolt &symbol=s_it->second;
310 error() <<
"incomplete type not permitted here" <<
eom;
343 new_code.push_back(decl);
348 new_code.splice(new_code.begin(),
clean_code);
356 else if(new_code.size()==1)
358 code.
swap(new_code.front());
364 code_block.set_statement(ID_decl_block);
365 code.
swap(code_block);
371 if(type.
id() == ID_array)
375 if(array_type.size().is_nil())
380 else if(type.
id()==ID_struct || type.
id()==ID_union)
384 if(struct_union_type.is_incomplete())
387 for(
const auto &c : struct_union_type.components())
391 else if(type.
id()==ID_vector)
410 error() <<
"expression statement expected to have one operand"
424 error() <<
"for expected to have four operands" <<
eom;
441 if(!
config.ansi_c.for_has_scope ||
502 code_block.
add(std::move(code));
503 code.
swap(code_block);
541 error() <<
"switch_case expected to have two operands" <<
eom;
552 error() <<
"did not expect default label here" <<
eom;
561 error() <<
"did not expect `case' here" <<
eom;
578 error() <<
"did not expect `case' here" <<
eom;
608 error() <<
"computed-goto expected to have one operand" <<
eom;
614 if(dest.
id()!=ID_dereference)
617 error() <<
"computed-goto expected to have dereferencing operand"
631 error() <<
"ifthenelse expected to have three operands" <<
eom;
668 error() <<
"start_thread expected to have one operand" <<
eom;
688 warning() <<
"function has return void ";
689 warning() <<
"but a return statement returning ";
705 warning() <<
"non-void function should return a value" <<
eom;
741 for(
auto &statement : body_block.
statements())
743 if(statement.get_statement() == ID_switch_case)
745 else if(statement.get_statement() == ID_decl)
747 if(statement.operands().size() == 1)
750 wrapping_block.
statements().back().swap(statement);
755 wrapping_block.
add(statement);
756 wrapping_block.
statements().back().operands().pop_back();
757 statement.set_statement(ID_assign);
764 wrapping_block.
add(std::move(code));
765 code.
swap(wrapping_block);
780 error() <<
"while expected to have two operands" <<
eom;
797 code.
body() = code_block;
826 error() <<
"do while expected to have two operands" <<
eom;
843 code.
body() = code_block;
872 "side-effects not allowed in assigns clause targets",
878 "ternary expressions not allowed in assigns clause targets",
901 <<
"function with possible side-effect called in target's condition"
905 if(condition.
type().
id() == ID_empty)
908 "void-typed expressions not allowed as assigns clause conditions",
918 "side-effects not allowed in assigns clause conditions",
925 "ternary expressions not allowed in assigns clause conditions",
932 const std::function<
void(
exprt &)> typecheck_target,
933 const std::string &clause_type)
937 for(
auto &target : targets)
942 "expected a conditional target group expression in " + clause_type +
943 "clause, found " +
id2string(target.id()),
944 target.source_location()};
951 auto &condition = conditional_target_group.condition();
954 if(condition.is_true())
958 for(
auto &actual_target : conditional_target_group.targets())
960 typecheck_target(actual_target);
961 new_targets.push_back(actual_target);
967 for(
auto &actual_target : conditional_target_group.targets())
969 typecheck_target(actual_target);
971 new_targets.push_back(std::move(target));
980 std::swap(targets, new_targets);
985 const std::function<void(
exprt &)> typecheck_target = [&](
exprt &target) {
993 const std::function<void(
exprt &)> typecheck_target = [&](
exprt &target) {
1006 if(target.
type().
id() == ID_empty)
1009 "lvalue expressions with void type not allowed in assigns clauses",
1021 "function pointer calls not allowed in assigns clauses",
1025 if(target.
type().
id() != ID_empty)
1028 "expecting void return type for function '" +
1030 "' called in assigns clause",
1034 for(
const auto &argument : funcall.arguments())
1041 "assigns clause target must be a non-void lvalue or a call to a function "
1051 const auto &type = target.
type();
1066 "function pointer calls not allowed in frees clauses",
1070 if(type.id() != ID_empty)
1073 "expecting void return type for function '" +
1075 "' called in frees clause",
1079 for(
const auto &argument : funcall.arguments())
1086 "frees clause target must be a pointer-typed expression or a call to a "
1087 "function returning void",
1096 for(
auto &invariant :
1113 for(
auto &decreases_clause_component :
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.
const declaratorst & declarators() const
bool get_is_static_assert() const
symbol_table_baset & symbol_table
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 throw_on_side_effects(const exprt &expr)
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)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_spec_frees_target(exprt &target)
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 typecheck_spec_condition(exprt &condition)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_conditional_targets(exprt::operandst &targets, const std::function< void(exprt &)> typecheck_target, const std::string &clause_type)
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_spec_frees(exprt::operandst &targets)
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
void add(const codet &code)
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.
const codet & body() const
const exprt & value() 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
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.
void reserve_operands(operandst::size_type n)
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
Thrown when we can't handle something in an input source file.
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
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
source_locationt source_location
mstreamt & warning() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A side_effect_exprt that returns a non-deterministically chosen value.
void value(const irep_idt &)
const irep_idt & get_identifier() const
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.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
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)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_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)
A range is a pair of a begin and an end iterators.