26 return expr2c(expr, *
this);
31 return type2c(type, *
this);
42 error() <<
"failed to move symbol '" << symbol.
name <<
"' into symbol table"
50 bool is_function=symbol.
type.
id()==ID_code;
78 warning() <<
"`extern' symbol should not have an initializer" <<
eom;
81 else if(!is_function && symbol.
value.
id()==ID_code)
84 error() <<
"only functions can have a function body" <<
eom;
89 if(symbol.
is_type && final_type.
id() == ID_struct)
93 else if(symbol.
is_type && final_type.
id() == ID_union)
97 else if(symbol.
is_type && final_type.
id() == ID_c_enum)
109 error() <<
"void-typed symbol not permitted" <<
eom;
114 symbol_tablet::symbolst::const_iterator old_it=
127 if(old_it->second.is_type!=symbol.
is_type)
131 <<
"' as a different kind of symbol" <<
eom;
150 if(symbol.
type.
id()==ID_code)
161 parameter.set_identifier(
irep_idt());
180 (final_old.
id() == ID_struct &&
182 (final_old.
id() == ID_union &&
to_union_type(final_old).is_incomplete()) ||
187 final_new.
id() == final_old.
id() &&
188 ((final_new.
id() == ID_struct &&
190 (final_new.
id() == ID_union &&
192 (final_new.
id() == ID_c_enum &&
206 error() <<
"conflicting definition of type symbol '"
215 (final_new.
id() == ID_struct &&
217 (final_new.
id() == ID_union &&
219 (final_new.
id() == ID_c_enum &&
222 if(final_old.
id() == final_new.
id())
230 error() <<
"conflicting definition of tag symbol '"
236 final_new.
id()==ID_c_enum && final_old.
id()==ID_c_enum)
242 final_new.
id()==ID_pointer && final_old.
id()==ID_pointer &&
256 <<
"' defined twice:\n"
272 if(final_old.
id()==ID_array &&
274 initial_new.
id()==ID_array &&
281 else if(final_old.
id()==ID_array &&
283 initial_new.
id()==ID_array &&
299 if(old_symbol.
type.
id()==ID_KnR)
302 if(final_new.
id()==ID_code)
305 error() <<
"function type not allowed for K&R function parameter"
315 if(final_new.
id()==ID_code)
317 if(final_old.
id()!=ID_code)
321 <<
"' redefined with a different type:\n"
364 for(
const auto &old_parameter : old_ct.
parameters())
366 const irep_idt &identifier = old_parameter.get_identifier();
368 symbol_tablet::symbolst::const_iterator p_s_it=
378 <<
"' defined twice" <<
eom;
412 if(final_old!=final_new)
414 if(final_old.
id()==ID_array &&
416 final_new.
id()==ID_array &&
423 final_old.
id() == ID_pointer && final_old.
subtype().
id() == ID_code &&
425 final_new.
id() == ID_pointer && final_new.
subtype().
id() == ID_code)
433 final_old.
id() == ID_pointer && final_old.
subtype().
id() == ID_code &&
434 final_new.
id() == ID_pointer && final_new.
subtype().
id() == ID_code &&
445 <<
"' redefined with a different type:\n"
462 new_symbol.
is_macro && final_new.
id() == ID_c_enum &&
472 <<
"' already has an initial value" <<
eom;
496 if(symbol.
value.
id() != ID_code)
499 error() <<
"function '" << symbol.
name <<
"' is initialized with "
516 unsigned anon_counter=0;
522 if(p.get_base_name().empty())
525 p.set_base_name(base_name);
529 irep_idt base_name = p.get_base_name();
532 p.set_identifier(identifier);
536 p_symbol.
type = p.type();
537 p_symbol.
name=identifier;
539 p_symbol.
location = p.source_location();
554 error() <<
"branching label '" << label.first
555 <<
"' is not defined in function" <<
eom;
570 if(!asm_label.
empty() &&
574 symbol.
name=asm_label;
578 if(symbol.
name!=orig_name)
581 std::make_pair(orig_name, asm_label)).second)
586 error() <<
"error: replacing asm renaming "
593 else if(asm_label.
empty())
595 asm_label_mapt::const_iterator entry=
599 symbol.
name=entry->second;
604 if(symbol.
name!=orig_name &&
605 symbol.
type.
id()==ID_code &&
612 const irep_idt &p_bn = p.get_base_name();
620 std::make_pair(p_id, p_new_id)).second)
631 codet code(ID_static_assert);
651 contract.
add(ID_C_spec_assigns).
swap(spec_assigns);
654 contract.
add(ID_C_spec_ensures).
swap(spec_ensures);
657 contract.
add(ID_C_spec_requires).
swap(spec_requires);
664 full_spec|=c_storage_spec;
676 declaration.
to_symbol(declarator, symbol);
687 error() <<
"alias attribute cannot be used with a body"
710 if(asm_name[0] ==
'.')
714 if(primary_section != std::string::npos)
715 asm_name.resize(primary_section);
729 declarator.set_name(identifier);
745 static_cast<codet &
>(contract), ID_C_spec_assigns);
749 if(new_symbol.
type.
id()==ID_code)
752 if(ret_type.
id()!=ID_empty)
757 irept assigns_to_add = contract.
find(ID_C_spec_assigns);
759 new_symbol.
type.
add(ID_C_spec_assigns) = assigns_to_add;
760 irept requires_to_add = contract.
find(ID_C_spec_requires);
762 new_symbol.
type.
add(ID_C_spec_requires) = requires_to_add;
763 irept ensures_to_add = contract.
find(ID_C_spec_ensures);
765 new_symbol.
type.
add(ID_C_spec_ensures) = ensures_to_add;
ANSI-C Language Type Checking.
unsignedbv_typet size_type()
static void make_already_typechecked(typet &type)
void set_is_thread_local(bool is_thread_local)
const exprt & spec_assigns() const
void set_is_weak(bool is_weak)
const exprt & spec_requires() const
void set_is_register(bool is_register)
void set_is_inline(bool is_inline)
typet full_type(const ansi_c_declaratort &) const
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
const declaratorst & declarators() const
void set_is_extern(bool is_extern)
void set_is_used(bool is_used)
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
const exprt & spec_ensures() const
void set_is_static(bool is_static)
void typecheck_function_body(symbolt &symbol)
std::map< irep_idt, source_locationt > labels_used
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
symbol_tablet & symbol_table
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
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
id_type_mapt parameter_map
virtual void typecheck_type(typet &type)
void typecheck_symbol(symbolt &symbol)
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)
const typet & return_type() const
void set_inlined(bool value)
bool has_ellipsis() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
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
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
irept & add(const irep_namet &name)
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.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
irep_idt base_name
Base (non-scoped) name.
const irep_idt & display_name() const
Return language specific display name if present.
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.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The type of an expression, extends irept.
const typet & subtype() const
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)
const std::string & id2string(const irep_idt &d)
const codet & to_code(const exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.