30 return expr2c(expr, *
this);
35 return type2c(type, *
this);
46 error() <<
"failed to move symbol '" << symbol.
name <<
"' into symbol table"
54 bool is_function=symbol.
type.
id()==ID_code;
82 warning() <<
"'extern' symbol '" << new_name
83 <<
"' should not have an initializer" <<
eom;
86 else if(!is_function && symbol.
value.
id()==ID_code)
89 error() <<
"only functions can have a function body" <<
eom;
94 if(symbol.
is_type && final_type.
id() == ID_struct)
98 else if(symbol.
is_type && final_type.
id() == ID_union)
102 else if(symbol.
is_type && final_type.
id() == ID_c_enum)
114 error() <<
"void-typed symbol not permitted" <<
eom;
119 symbol_table_baset::symbolst::const_iterator old_it =
132 if(old_it->second.is_type!=symbol.
is_type)
136 <<
"' as a different kind of symbol" <<
eom;
155 if(symbol.
type.
id()==ID_code)
168 parameter.set_identifier(
irep_idt());
187 (final_old.
id() == ID_struct &&
189 (final_old.
id() == ID_union &&
to_union_type(final_old).is_incomplete()) ||
194 final_new.
id() == final_old.
id() &&
195 ((final_new.
id() == ID_struct &&
197 (final_new.
id() == ID_union &&
199 (final_new.
id() == ID_c_enum &&
213 error() <<
"conflicting definition of type symbol '"
222 (final_new.
id() == ID_struct &&
224 (final_new.
id() == ID_union &&
226 (final_new.
id() == ID_c_enum &&
229 if(final_old.
id() == final_new.
id())
237 error() <<
"conflicting definition of tag symbol '"
243 final_new.
id()==ID_c_enum && final_old.
id()==ID_c_enum)
250 final_new.
id() == ID_pointer && final_old.
id() == ID_pointer &&
264 <<
"' defined twice:\n"
280 if(old_components.size() != new_components.size())
283 if(old_components.empty())
286 for(std::size_t i = 0; i < old_components.size() - 1; ++i)
288 if(old_components[i].type() != new_components[i].type())
293 old_components.back().type().id() != ID_array ||
294 new_components.back().type().id() != ID_array)
299 const auto &old_array_type =
to_array_type(old_components.back().type());
300 const auto &new_array_type =
to_array_type(new_components.back().type());
302 return old_array_type.element_type() == new_array_type.element_type() &&
303 old_array_type.get_bool(ID_C_flexible_array_member) &&
304 new_array_type.get_bool(ID_C_flexible_array_member) &&
305 (old_array_type.size().is_nil() || old_array_type.size().is_zero());
316 final_old.
id() == ID_array &&
318 initial_new.
id() == ID_array &&
327 final_old.
id() == ID_array &&
to_array_type(final_old).size().is_nil() &&
328 initial_new.
id() == ID_array &&
345 if(old_symbol.
type.
id()==ID_KnR)
348 if(final_new.
id()==ID_code)
351 error() <<
"function type not allowed for K&R function parameter"
361 if(final_new.
id()==ID_code)
363 if(final_old.
id()!=ID_code)
367 <<
"' redefined with a different type:\n"
378 !old_ct.
get_bool(ID_C_incomplete) &&
392 "' redefined with a different type:\n" +
407 error() <<
"code contract on incomplete function re-declaration" <<
eom;
440 for(
const auto &old_parameter : old_ct.
parameters())
442 const irep_idt &identifier = old_parameter.get_identifier();
444 symbol_table_baset::symbolst::const_iterator p_s_it =
454 <<
"' defined twice" <<
eom;
488 auto new_parameters_it = new_ct.
parameters().begin();
491 if(new_parameters_it != new_ct.
parameters().end())
493 new_parameters_it->set_identifier(p.get_identifier());
504 if(final_old!=final_new)
508 final_new.
id() == ID_array &&
516 final_old.
id() == ID_pointer &&
519 final_new.
id() == ID_pointer &&
528 final_old.
id() == ID_pointer &&
530 final_new.
id() == ID_pointer &&
539 final_old.
id() == ID_struct && final_new.
id() == ID_struct &&
549 <<
"' redefined with a different type:\n"
566 new_symbol.
is_macro && final_new.
id() == ID_c_enum &&
576 <<
"' already has an initial value" <<
eom;
600 if(symbol.
value.
id() != ID_code)
603 error() <<
"function '" << symbol.
name <<
"' is initialized with "
638 error() <<
"branching label '" << label.first
639 <<
"' is not defined in function" <<
eom;
654 if(!asm_label.
empty() &&
658 symbol.
name=asm_label;
662 if(symbol.
name!=orig_name)
665 std::make_pair(orig_name, asm_label)).second)
670 error() <<
"error: replacing asm renaming "
677 else if(asm_label.
empty())
679 asm_label_mapt::const_iterator entry=
683 symbol.
name=entry->second;
688 if(symbol.
name!=orig_name &&
689 symbol.
type.
id()==ID_code &&
696 const irep_idt &p_bn = p.get_base_name();
704 std::make_pair(p_id, p_new_id)).second)
714 std::string &clause_type)
717 expr, ID_old,
CPROVER_PREFIX "old is not allowed in " + clause_type +
".");
721 CPROVER_PREFIX "loop_entry is not allowed in " + clause_type +
".");
724 auto pred = [&](
const exprt &expr) {
741 std::string &clause_type)
745 auto pred = [&](
const exprt &expr) {
755 id2string(
id) +
" is not allowed in " + clause_type +
".",
765 codet code(ID_static_assert);
785 full_spec|=c_storage_spec;
806 error() <<
"alias attribute cannot be used with a body"
828 symbolt symbol_for_renaming = symbol;
843 if(asm_name[0] ==
'.')
845 std::string::size_type primary_section = asm_name.find(
'.', 1);
847 if(primary_section != std::string::npos)
848 asm_name.resize(primary_section);
862 declarator.set_name(identifier);
869 new_symbol.
type.
id() == ID_code &&
883 temporary_parameter_symbols.emplace_back(
887 std::size_t anon_counter = 0;
891 if(p.get_base_name().empty())
892 p.set_base_name(
"#anon" + std::to_string(anon_counter++));
895 const irep_idt &base_name = p.get_base_name();
899 p.set_identifier(parameter_identifier);
904 temporary_parameter_symbols.emplace_back(
905 parameter_identifier, p.type());
908 for(
auto &c_requires : code_type.
c_requires())
912 std::string clause_type =
"preconditions";
915 lambda_exprt lambda{temporary_parameter_symbols, c_requires};
916 lambda.add_source_location() = c_requires.source_location();
917 c_requires.swap(lambda);
921 for(
auto &assigns : code_type.
c_assigns())
923 std::string clause_type =
"assigns clauses";
925 lambda_exprt lambda{temporary_parameter_symbols, assigns};
926 lambda.add_source_location() = assigns.source_location();
927 assigns.swap(lambda);
931 for(
auto &frees : code_type.
c_frees())
933 lambda_exprt lambda{temporary_parameter_symbols, frees};
934 lambda.add_source_location() = frees.source_location();
938 for(
auto &ensures : code_type.
c_ensures())
946 lambda_exprt lambda{temporary_parameter_symbols, ensures};
947 lambda.add_source_location() = ensures.source_location();
948 ensures.swap(lambda);
951 for(
const auto ¶meter_sym : temporary_parameter_symbols)
960 contract.
type = code_type;
970 <<
"' already set at " << entry.first.location.
as_string()
992 unsigned anon_counter = 0;
998 if(p.get_base_name().empty())
1000 irep_idt base_name =
"#anon" + std::to_string(anon_counter++);
1001 p.set_base_name(base_name);
1005 irep_idt base_name = p.get_base_name();
1008 p.set_identifier(identifier);
1012 p_symbol.
type = p.type();
1013 p_symbol.
name = identifier;
1015 p_symbol.
location = p.source_location();
ANSI-CC Language Type Checking.
static bool is_instantiation_of_flexible_array(const struct_typet &old_type, const struct_typet &new_type)
ANSI-C Language Type Checking.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
static void make_already_typechecked(typet &type)
void set_is_thread_local(bool is_thread_local)
void set_is_weak(bool is_weak)
symbolt to_symbol(const ansi_c_declaratort &) const
const declaratorst & declarators() const
void set_is_register(bool is_register)
void set_is_inline(bool is_inline)
typet full_type(const ansi_c_declaratort &) const
void set_is_extern(bool is_extern)
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
void set_is_static(bool is_static)
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
std::vector< symbol_exprt > variablest
symbol_table_baset & symbol_table
virtual void check_history_expr_return_value(const exprt &expr, std::string &clause_type)
Checks that no history expr or return_value exists in expr.
void typecheck_function_body(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void check_was_freed(const exprt &expr, std::string &clause_type)
Checks that no occurence of the CPROVER_PREFIX was_freed predicate is found in expr.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
void typecheck_new_symbol(symbolt &symbol)
asm_label_mapt asm_label_map
virtual void adjust_function_parameter(typet &type) const
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
void add_parameters_to_symbol_table(symbolt &symbol)
Create symbols for parameter of the code-typed symbol symbol.
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_spec_frees(exprt::operandst &targets)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
id_type_mapt parameter_map
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_type(typet &type)
void typecheck_symbol(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_defined
void set_inlined(bool value)
const parameterst & parameters() const
const typet & return_type() const
bool has_ellipsis() const
const exprt::operandst & c_frees() const
const exprt::operandst & c_assigns() const
const exprt::operandst & c_requires() const
const exprt::operandst & c_ensures() const
bool has_contract() const
Data structure for representing an arbitrary statement in a program.
struct configt::ansi_ct ansi_c
Mangle identifiers by hashing their working directory with djb2 hash.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const std::string & as_string() 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).
bool is_constant() const
Return whether the expression is a constant.
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
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
const irep_idt & id() const
A (mathematical) lambda expression.
source_locationt source_location
mstreamt & warning() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_file() const
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
const irep_idt & display_name() const
Return language specific display name if present.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The type of an expression, extends irept.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
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.
bool has_contract(const irep_idt &function_identifier, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
Mangle names of file-local functions to make them unique.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
const codet & to_code(const exprt &expr)
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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.