10 #ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H
11 #define CPROVER_ANSI_C_ANSI_C_PARSER_H
136 lookup(base_name, identifier,
false,
true);
int yyansi_cparse(ansi_c_parsert &)
void ansi_c_scanner_init(ansi_c_parsert &)
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
ansi_c_parsert(message_handlert &message_handler)
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
std::list< exprt > pragma_pack
void new_scope(const std::string &prefix)
bool pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
bool ts_18661_3_Floatn_types
ansi_c_identifiert identifiert
void add_declarator(exprt &declaration, irept &declarator)
bool __float128_is_keyword
ansi_c_parse_treet parse_tree
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
unsigned parenthesis_counter
configt::ansi_ct::flavourt modet
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.
std::list< scopet > scopest
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 copy_item(const ansi_c_declarationt &declaration)
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
std::string string_literal
irep_idt lookup_label(const irep_idt base_name)
const scopet & root_scope() const
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 & id() const
The type of an expression, extends irept.
#define PRECONDITION(CONDITION)