24 return expr2c(expr, *
this);
29 return type2c(type, *
this);
40 error() <<
"failed to move symbol `" << symbol.
name 41 <<
"' into symbol table" <<
eom;
48 bool is_function=symbol.
type.
id()==ID_code;
70 else if(!is_function && symbol.
value.
id()==ID_code)
73 error() <<
"only functions can have a function body" <<
eom;
79 (final_type.
id()==ID_struct ||
80 final_type.
id()==ID_incomplete_struct))
85 (final_type.
id()==ID_union ||
86 final_type.
id()==ID_incomplete_union))
91 (final_type.
id()==ID_c_enum ||
92 final_type.
id()==ID_incomplete_c_enum))
102 symbol_tablet::symbolst::iterator old_it=
115 if(old_it->second.is_type!=symbol.
is_type)
119 <<
"' as a different kind of symbol" <<
eom;
137 if(symbol.
type.
id()==ID_code)
146 for(code_typet::parameterst::iterator
168 if(final_old.
id()==ID_incomplete_struct ||
169 final_old.
id()==ID_incomplete_union ||
170 final_old.
id()==ID_incomplete_c_enum)
186 error() <<
"conflicting definition of type symbol `" 195 if(final_new.
id()==ID_incomplete_struct ||
196 final_new.
id()==ID_incomplete_union ||
197 final_new.
id()==ID_incomplete_c_enum)
207 error() <<
"conflicting definition of tag symbol `" 214 final_new.
id()==ID_c_enum && final_old.
id()==ID_c_enum)
220 final_new.
id()==ID_pointer && final_old.
id()==ID_pointer &&
233 error() <<
"type symbol `" 250 if(final_old.
id()==ID_array &&
252 initial_new.
id()==ID_array &&
268 if(old_symbol.
type.
id()==ID_KnR)
271 if(final_new.
id()==ID_code)
274 error() <<
"function type not allowed for K&R function parameter" 284 if(final_new.
id()==ID_code)
290 if(final_old.
id()!=ID_code)
293 error() <<
"error: function symbol `" 295 <<
"' redefined with a different type:\n" 311 old_symbol.
type.
set(ID_C_inlined,
true);
312 new_symbol.
type.
set(ID_C_inlined,
true);
335 for(code_typet::parameterst::const_iterator
340 const irep_idt &identifier=p_it->get_identifier();
342 symbol_tablet::symbolst::iterator p_s_it=
352 <<
"' defined twice" <<
eom;
386 if(final_old!=final_new)
388 if(final_old.
id()==ID_array &&
390 final_new.
id()==ID_array &&
395 if(old_symbol.
type.
id()==ID_symbol)
401 symbol_tablet::symbolst::iterator s_it=
407 error() <<
"typecheck_redefinition_non_type: " 408 <<
"failed to find symbol `" << identifier <<
"'" 415 symbol.
type=final_new;
420 else if((final_old.
id()==ID_incomplete_c_enum ||
421 final_old.
id()==ID_c_enum) &&
422 (final_new.
id()==ID_incomplete_c_enum ||
423 final_new.
id()==ID_c_enum))
427 else if(final_old.
id()==ID_pointer &&
430 final_new.
id()==ID_pointer &&
438 else if(final_old.
id()==ID_pointer &&
440 final_new.
id()==ID_pointer &&
452 <<
"' redefined with a different type:\n" 480 (final_new.
id()==ID_incomplete_c_enum ||
481 final_new.
id()==ID_c_enum) &&
492 <<
"' already has an initial value" <<
eom;
531 unsigned anon_counter=0;
535 for(code_typet::parameterst::iterator
536 p_it=parameters.begin();
537 p_it!=parameters.end();
541 if(p_it->get_base_name().empty())
543 irep_idt base_name=
"#anon"+std::to_string(anon_counter++);
544 p_it->set_base_name(base_name);
548 irep_idt base_name=p_it->get_base_name();
551 p_it->set_identifier(identifier);
555 p_symbol.
type=p_it->type();
556 p_symbol.
name=identifier;
558 p_symbol.
location=p_it->source_location();
568 if(symbol.
name==ID_main)
572 for(std::map<irep_idt, source_locationt>::const_iterator
578 error() <<
"branching label `" << it->first
579 <<
"' is not defined in function" <<
eom;
594 if(!asm_label.
empty() &&
598 symbol.
name=asm_label;
602 if(symbol.
name!=orig_name)
605 std::make_pair(orig_name, asm_label)).second)
610 error() <<
"error: replacing asm renaming " 617 else if(asm_label.
empty())
619 asm_label_mapt::const_iterator entry=
623 symbol.
name=entry->second;
628 if(symbol.
name!=orig_name &&
629 symbol.
type.
id()==ID_code &&
634 for(code_typet::parameterst::const_iterator
639 const irep_idt &p_bn=p_it->get_base_name();
647 std::make_pair(p_id, p_new_id)).second)
658 assert(declaration.
operands().size()==2);
677 static_cast<const exprt&
>(declaration.
find(ID_C_spec_requires));
678 contract.
add(ID_C_spec_requires).
swap(spec_requires);
681 static_cast<const exprt&
>(declaration.
find(ID_C_spec_ensures));
682 contract.
add(ID_C_spec_ensures).
swap(spec_ensures);
686 for(ansi_c_declarationt::declaratorst::iterator
692 full_spec|=c_storage_spec;
709 if(!full_spec.alias.empty())
714 error() <<
"alias attribute cannot be used with a body" 725 if(full_spec.section.empty())
729 std::string asm_name;
730 asm_name=
id2string(full_spec.section)+
"$$";
731 if(!full_spec.asm_label.empty())
732 asm_name+=
id2string(full_spec.asm_label);
739 d_it->set_name(identifier);
746 symbol_tablet::symbolst::iterator s_it=
749 symbolt &new_symbol=s_it->second;
754 if(new_symbol.type.id()==ID_code)
757 if(ret_type.
id()!=ID_empty)
762 if(contract.find(ID_C_spec_requires).is_not_nil())
763 new_symbol.type.add(ID_C_spec_requires)=
764 contract.find(ID_C_spec_requires);
765 if(contract.find(ID_C_spec_ensures).is_not_nil())
766 new_symbol.type.add(ID_C_spec_ensures)=
767 contract.find(ID_C_spec_ensures);
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
bool get_is_static_assert() const
The type of an expression.
irep_idt name
The unique identifier.
std::map< irep_idt, source_locationt > labels_used
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_declaration(ansi_c_declarationt &)
const std::string & id2string(const irep_idt &d)
asm_label_mapt asm_label_map
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
irep_idt mode
Language mode.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
bool has_ellipsis() const
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
id_type_mapt parameter_map
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
irep_idt module
Name of module the symbol belongs to.
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
virtual std::string to_string(const exprt &expr)
typet full_type(const ansi_c_declaratort &) const
symbol_tablet & symbol_table
void set_is_weak(bool is_weak)
const irep_idt & id() const
void set_is_thread_local(bool is_thread_local)
const declaratorst & declarators() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void typecheck_new_symbol(symbolt &symbol)
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
ANSI-C Language Type Checking.
const source_locationt & find_source_location() const
void make_already_typechecked(typet &dest)
source_locationt source_location
const irep_idt & get(const irep_namet &name) const
std::string type2c(const typet &type, const namespacet &ns)
const exprt & size() const
virtual void typecheck_expr(exprt &expr)
void set_is_register(bool is_register)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void adjust_function_parameter(typet &type) const
const irep_idt & display_name() const
void set_is_static(bool is_static)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void set_is_extern(bool is_extern)
Base class for all expressions.
void add_argc_argv(const symbolt &main_symbol)
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
irept & add(const irep_namet &name)
std::map< irep_idt, source_locationt > labels_defined
std::string expr2c(const exprt &expr, const namespacet &ns)
void typecheck_symbol(symbolt &symbol)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
const codet & to_code(const exprt &expr)
void set_is_typedef(bool is_typedef)
void typecheck_function_body(symbolt &symbol)
Expression to hold a symbol (variable)
virtual void typecheck_type(typet &type)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A statement in a programming language.
void set_is_inline(bool is_inline)
const typet & subtype() const
const irept & find(const irep_namet &name) const
const typet & return_type() const
const irep_idt & get_identifier() const
void set(const irep_namet &name, const irep_idt &value)
virtual void typecheck_code(codet &code)