CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
ansi_c_parser.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H
11#define CPROVER_ANSI_C_ANSI_C_PARSER_H
12
13#include <map>
14
15#include <util/parser.h>
16#include <util/config.h>
17
18#include "ansi_c_parse_tree.h"
19#include "ansi_c_scope.h"
20
21class ansi_c_parsert;
23
25{
26public:
28
29 explicit ansi_c_parsert(message_handlert &message_handler)
30 : parsert(message_handler),
34 mode(modet::NONE),
35 cpp98(false),
36 cpp11(false),
43 {
44 // set up global scope
45 scopes.clear();
46 scopes.push_back(scopet());
47 }
48
49 bool parse() override
50 {
51 return yyansi_cparse(*this) != 0;
52 }
53
54 // internal state of the scanner
58 std::string string_literal;
59 std::list<exprt> pragma_pack;
60
63
64 // recognize C++98 and C++11 keywords
65 bool cpp98, cpp11;
66
67 // in C99 and upwards, for(;;) has a scope
69
70 // ISO/IEC TS 18661-3:2015
76
79
80 typedef std::list<scopet> scopest;
82
84 {
85 return scopes.front();
86 }
87
88 const scopet &root_scope() const
89 {
90 return scopes.front();
91 }
92
93 void pop_scope()
94 {
95 scopes.pop_back();
96 }
97
99 {
100 PRECONDITION(!scopes.empty());
101 return scopes.back();
102 }
103
105
106 // convert a declarator and then add it to existing an declaration
107 void add_declarator(exprt &declaration, irept &declarator);
108
109 // adds a tag to the current scope
110 void add_tag_with_body(irept &tag);
111
112 void copy_item(const ansi_c_declarationt &declaration)
113 {
114 PRECONDITION(declaration.id() == ID_declaration);
115 parse_tree.items.push_back(declaration);
116 }
117
118 void new_scope(const std::string &prefix)
119 {
120 const scopet &current=current_scope();
121 scopes.push_back(scopet());
122 scopes.back().prefix=current.prefix+prefix;
123 }
124
126 const irep_idt &base_name, // in
127 irep_idt &identifier, // out
128 bool tag,
129 bool label);
130
131 static ansi_c_id_classt get_class(const typet &type);
132
134 {
135 irep_idt identifier;
136 lookup(base_name, identifier, false, true);
137 return identifier;
138 }
139
142
144 void pragma_cprover_push();
145
147 void pragma_cprover_pop();
148
150 void pragma_cprover_add_check(const irep_idt &name, bool enabled);
151
154 bool pragma_cprover_clash(const irep_idt &name, bool enabled);
155
158 void set_pragma_cprover();
159
160private:
161 std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
162};
163
165
166#endif // CPROVER_ANSI_C_ANSI_C_PARSER_H
int yyansi_cparse(ansi_c_parsert &)
void ansi_c_scanner_init(ansi_c_parsert &)
ansi_c_id_classt
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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)
ansi_c_scopet scopet
bool parse() override
bool __float128_is_keyword
ansi_c_parse_treet parse_tree
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
unsigned parenthesis_counter
scopet & root_scope()
scopet & current_scope()
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.
const scopet & root_scope() const
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)
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
std::string prefix
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
Parser utilities.
#define PRECONDITION(CONDITION)
Definition invariant.h:463