25 for(scopest::const_reverse_iterator it=
scopes.rbegin();
29 scopet::name_mapt::const_iterator
n_it=
32 if(
n_it!=it->name_map.end())
34 identifier=
n_it->second.prefixed_name;
35 return n_it->second.id_class;
103 if(!base_name.
empty())
197 auto found = top.find(name);
216 std::string full_name =
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
ansi_c_id_classt id_class
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
bool pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
void add_declarator(exprt &declaration, irept &declarator)
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
void add_tag_with_body(irept &tag)
bool pragma_cprover_clash(const irep_idt &name, bool enabled)
Returns true iff the same check with polarity is already present at top of the stack.
static ansi_c_id_classt get_class(const typet &type)
ansi_c_id_classt lookup(const irep_idt &base_name, irep_idt &identifier, bool tag, bool label)
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
source_locationt _source_location
void add_pragma(const irep_idt &pragma)
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)