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)
120 error() <<
"static assertion failed";
121 if(code.
op1().
id() == ID_string_constant)
127 else if(statement==ID_CPROVER_try_catch ||
128 statement==ID_CPROVER_try_finally)
134 else if(statement==ID_CPROVER_throw)
138 else if(statement==ID_assume ||
139 statement==ID_assert)
150 error() <<
"unexpected statement: " << statement <<
eom;
176 code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
178 for(
auto &expr : op.operands())
182 else if(flavor==ID_msc)
194 error() <<
"assignment statement expected to have two operands"
217 if(code_op.is_not_nil())
218 new_ops.
add(std::move(code_op));
229 error() <<
"break not allowed here" <<
eom;
239 error() <<
"continue not allowed here" <<
eom;
250 error() <<
"decl expected to have 1 operand" <<
eom;
255 if(code.
op0().
id()!=ID_declaration)
258 error() <<
"decl statement expected to have declaration as operand"
268 codet new_code(ID_static_assert);
278 std::list<codet> new_code;
287 symbol_table_baset::symbolst::const_iterator s_it =
293 error() <<
"failed to find decl symbol '" << identifier
294 <<
"' in symbol table" <<
eom;
298 const symbolt &symbol=s_it->second;
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());
361 code_block.set_statement(ID_decl_block);
362 code.
swap(code_block);
368 if(type.
id() == ID_array)
372 if(array_type.size().is_nil())
377 else if(type.
id()==ID_struct || type.
id()==ID_union)
381 if(struct_union_type.is_incomplete())
384 for(
const auto &c : struct_union_type.components())
388 else if(type.
id()==ID_vector)
390 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
403 error() <<
"expression statement expected to have one operand"
417 error() <<
"for expected to have four operands" <<
eom;
495 code_block.
add(std::move(code));
496 code.
swap(code_block);
534 error() <<
"switch_case expected to have two operands" <<
eom;
545 error() <<
"did not expect default label here" <<
eom;
554 error() <<
"did not expect `case' here" <<
eom;
571 error() <<
"did not expect `case' here" <<
eom;
601 error() <<
"computed-goto expected to have one operand" <<
eom;
607 if(dest.
id()!=ID_dereference)
610 error() <<
"computed-goto expected to have dereferencing operand"
624 error() <<
"ifthenelse expected to have three operands" <<
eom;
633 if(cond.
id()==ID_sideeffect &&
634 cond.
get(ID_statement)==ID_assign)
636 warning(
"warning: assignment in if condition");
669 error() <<
"start_thread expected to have one operand" <<
eom;
689 warning() <<
"function has return void ";
690 warning() <<
"but a return statement returning ";
706 warning() <<
"non-void function should return a value" <<
eom;
742 for(
auto &statement : body_block.
statements())
744 if(statement.get_statement() == ID_switch_case)
746 else if(statement.get_statement() == ID_decl)
748 if(statement.operands().size() == 1)
751 wrapping_block.
statements().back().swap(statement);
756 wrapping_block.
add(statement);
757 wrapping_block.
statements().back().operands().pop_back();
758 statement.set_statement(ID_assign);
765 wrapping_block.
add(std::move(code));
766 code.
swap(wrapping_block);
781 error() <<
"while expected to have two operands" <<
eom;
798 code.
body() = code_block;
827 error() <<
"do while expected to have two operands" <<
eom;
844 code.
body() = code_block;
873 "side-effects not allowed in assigns clause targets",
879 "ternary expressions not allowed in assigns clause targets",
902 <<
"function with possible side-effect called in target's condition"
906 if(condition.
type().
id() == ID_empty)
909 "void-typed expressions not allowed as assigns clause conditions",
919 "side-effects not allowed in assigns clause conditions",
926 "ternary expressions not allowed in assigns clause conditions",
933 const std::function<
void(
exprt &)> typecheck_target,
934 const std::string &clause_type)
938 for(
auto &target : targets)
943 "expected a conditional target group expression in " + clause_type +
944 "clause, found " +
id2string(target.id()),
945 target.source_location()};
952 auto &condition = conditional_target_group.condition();
955 if(condition.is_true())
959 for(
auto &actual_target : conditional_target_group.targets())
961 typecheck_target(actual_target);
962 new_targets.push_back(actual_target);
968 for(
auto &actual_target : conditional_target_group.targets())
970 typecheck_target(actual_target);
972 new_targets.push_back(std::move(target));
981 std::swap(targets, new_targets);
986 const std::function<void(
exprt &)> typecheck_target = [&](
exprt &target) {
994 const std::function<void(
exprt &)> typecheck_target = [&](
exprt &target) {
1007 if(target.
type().
id() == ID_empty)
1010 "lvalue expressions with void type not allowed in assigns clauses",
1022 "function pointer calls not allowed in assigns clauses",
1026 if(target.
type().
id() != ID_empty)
1029 "expecting void return type for function '" +
1031 "' called in assigns clause",
1035 for(
const auto &argument : funcall.arguments())
1042 "assigns clause target must be a non-void lvalue or a call to a function "
1052 const auto &type = target.
type();
1067 "function pointer calls not allowed in frees clauses",
1071 if(type.id() != ID_empty)
1074 "expecting void return type for function '" +
1076 "' called in frees clause",
1080 for(
const auto &argument : funcall.arguments())
1087 "frees clause target must be a pointer-typed expression or a call to a "
1088 "function returning void",
1097 for(
auto &invariant :
1098 (
static_cast<exprt &
>(code.
add(ID_C_spec_loop_invariant)).operands()))
1114 for(
auto &decreases_clause_component :
1115 (
static_cast<exprt &
>(code.
add(ID_C_spec_decreases)).operands()))
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.
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
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
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.
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
const irep_idt & get(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 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 irep_idt & get_identifier() 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)
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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.
bool can_cast_expr< symbol_exprt >(const exprt &base)
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.