CBMC
|
#include <ansi_c_parser.h>
Public Types | |
enum class | decl_typet { TAG , MEMBER , PARAMETER , OTHER } |
typedef configt::ansi_ct::flavourt | modet |
typedef ansi_c_identifiert | identifiert |
typedef ansi_c_scopet | scopet |
typedef std::list< scopet > | scopest |
Public Member Functions | |
ansi_c_parsert (message_handlert &message_handler) | |
bool | parse () override |
scopet & | root_scope () |
const scopet & | root_scope () const |
void | pop_scope () |
scopet & | current_scope () |
void | add_declarator (exprt &declaration, irept &declarator) |
void | add_tag_with_body (irept &tag) |
void | copy_item (const ansi_c_declarationt &declaration) |
void | new_scope (const std::string &prefix) |
ansi_c_id_classt | lookup (const irep_idt &base_name, irep_idt &identifier, bool tag, bool label) |
irep_idt | lookup_label (const irep_idt base_name) |
bool | pragma_cprover_empty () |
True iff the CPROVER pragma stack is empty. More... | |
void | pragma_cprover_push () |
Pushes an empty level in the CPROVER pragma stack. More... | |
void | pragma_cprover_pop () |
Pops a level in the CPROVER pragma stack. More... | |
void | pragma_cprover_add_check (const irep_idt &name, bool enabled) |
Adds a check to the CPROVER pragma stack. More... | |
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. More... | |
void | set_pragma_cprover () |
Tags source_location with the current CPROVER pragma stack. More... | |
Public Member Functions inherited from parsert | |
parsert (message_handlert &message_handler) | |
virtual | ~parsert () |
bool | read (char &ch) |
bool | eof () |
void | parse_error (const std::string &message, const std::string &before) |
void | inc_line_no () |
void | set_line_no (unsigned _line_no) |
void | set_file (const irep_idt &file) |
irep_idt | get_file () const |
unsigned | get_line_no () const |
unsigned | get_column () const |
void | set_column (unsigned _column) |
void | set_source_location (exprt &e) |
void | set_function (const irep_idt &function) |
void | advance_column (unsigned token_width) |
Static Public Member Functions | |
static ansi_c_id_classt | get_class (const typet &type) |
Public Attributes | |
ansi_c_parse_treet | parse_tree |
bool | tag_following |
bool | asm_block_following |
unsigned | parenthesis_counter |
std::string | string_literal |
std::list< exprt > | pragma_pack |
modet | mode |
bool | cpp98 |
bool | cpp11 |
bool | for_has_scope |
bool | ts_18661_3_Floatn_types |
bool | __float128_is_keyword |
bool | float16_type |
bool | bf16_type |
bool | fp16_type |
scopest | scopes |
Public Attributes inherited from parsert | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Private Attributes | |
std::list< std::map< const irep_idt, bool > > | pragma_cprover_stack |
Additional Inherited Members | |
Protected Attributes inherited from parsert | |
messaget | log |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Definition at line 24 of file ansi_c_parser.h.
Definition at line 77 of file ansi_c_parser.h.
Definition at line 61 of file ansi_c_parser.h.
typedef std::list<scopet> ansi_c_parsert::scopest |
Definition at line 80 of file ansi_c_parser.h.
typedef ansi_c_scopet ansi_c_parsert::scopet |
Definition at line 78 of file ansi_c_parser.h.
|
strong |
Enumerator | |
---|---|
TAG | |
MEMBER | |
PARAMETER | |
OTHER |
Definition at line 104 of file ansi_c_parser.h.
|
inlineexplicit |
Definition at line 29 of file ansi_c_parser.h.
Definition at line 74 of file ansi_c_parser.cpp.
void ansi_c_parsert::add_tag_with_body | ( | irept & | tag | ) |
Definition at line 56 of file ansi_c_parser.cpp.
|
inline |
Definition at line 112 of file ansi_c_parser.h.
|
inline |
Definition at line 98 of file ansi_c_parser.h.
|
static |
Definition at line 147 of file ansi_c_parser.cpp.
ansi_c_id_classt ansi_c_parsert::lookup | ( | const irep_idt & | base_name, |
irep_idt & | identifier, | ||
bool | tag, | ||
bool | label | ||
) |
Definition at line 13 of file ansi_c_parser.cpp.
Definition at line 133 of file ansi_c_parser.h.
|
inline |
Definition at line 118 of file ansi_c_parser.h.
|
inlineoverridevirtual |
Implements parsert.
Definition at line 49 of file ansi_c_parser.h.
|
inline |
Definition at line 93 of file ansi_c_parser.h.
void ansi_c_parsert::pragma_cprover_add_check | ( | const irep_idt & | name, |
bool | enabled | ||
) |
Adds a check to the CPROVER pragma stack.
Definition at line 184 of file ansi_c_parser.cpp.
bool ansi_c_parsert::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.
Definition at line 194 of file ansi_c_parser.cpp.
bool ansi_c_parsert::pragma_cprover_empty | ( | ) |
True iff the CPROVER pragma stack is empty.
Definition at line 169 of file ansi_c_parser.cpp.
void ansi_c_parsert::pragma_cprover_pop | ( | ) |
Pops a level in the CPROVER pragma stack.
Definition at line 179 of file ansi_c_parser.cpp.
void ansi_c_parsert::pragma_cprover_push | ( | ) |
Pushes an empty level in the CPROVER pragma stack.
Definition at line 174 of file ansi_c_parser.cpp.
|
inline |
Definition at line 83 of file ansi_c_parser.h.
|
inline |
Definition at line 88 of file ansi_c_parser.h.
void ansi_c_parsert::set_pragma_cprover | ( | ) |
Tags source_location with the current CPROVER pragma stack.
Definition at line 201 of file ansi_c_parser.cpp.
bool ansi_c_parsert::__float128_is_keyword |
Definition at line 72 of file ansi_c_parser.h.
bool ansi_c_parsert::asm_block_following |
Definition at line 56 of file ansi_c_parser.h.
bool ansi_c_parsert::bf16_type |
Definition at line 74 of file ansi_c_parser.h.
bool ansi_c_parsert::cpp11 |
Definition at line 65 of file ansi_c_parser.h.
bool ansi_c_parsert::cpp98 |
Definition at line 65 of file ansi_c_parser.h.
bool ansi_c_parsert::float16_type |
Definition at line 73 of file ansi_c_parser.h.
bool ansi_c_parsert::for_has_scope |
Definition at line 68 of file ansi_c_parser.h.
bool ansi_c_parsert::fp16_type |
Definition at line 75 of file ansi_c_parser.h.
modet ansi_c_parsert::mode |
Definition at line 62 of file ansi_c_parser.h.
unsigned ansi_c_parsert::parenthesis_counter |
Definition at line 57 of file ansi_c_parser.h.
ansi_c_parse_treet ansi_c_parsert::parse_tree |
Definition at line 27 of file ansi_c_parser.h.
|
private |
Definition at line 161 of file ansi_c_parser.h.
std::list<exprt> ansi_c_parsert::pragma_pack |
Definition at line 59 of file ansi_c_parser.h.
scopest ansi_c_parsert::scopes |
Definition at line 81 of file ansi_c_parser.h.
std::string ansi_c_parsert::string_literal |
Definition at line 58 of file ansi_c_parser.h.
bool ansi_c_parsert::tag_following |
Definition at line 55 of file ansi_c_parser.h.
bool ansi_c_parsert::ts_18661_3_Floatn_types |
Definition at line 71 of file ansi_c_parser.h.