CBMC
ansi_c_parser.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
21 class ansi_c_parsert;
23 
24 class ansi_c_parsert:public parsert
25 {
26 public:
28 
29  explicit ansi_c_parsert(message_handlert &message_handler)
30  : parsert(message_handler),
31  tag_following(false),
32  asm_block_following(false),
34  mode(modet::NONE),
35  cpp98(false),
36  cpp11(false),
37  for_has_scope(false),
39  __float128_is_keyword(false),
40  float16_type(false),
41  bf16_type(false),
42  fp16_type(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
74  bool bf16_type;
75  bool fp16_type;
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 
104  enum class decl_typet { TAG, MEMBER, PARAMETER, OTHER };
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 
133  irep_idt lookup_label(const irep_idt base_name)
134  {
135  irep_idt identifier;
136  lookup(base_name, identifier, false, true);
137  return identifier;
138  }
139 
141  bool pragma_cprover_empty();
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 
160 private:
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
Definition: ansi_c_scope.h:18
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
ansi_c_parsert(message_handlert &message_handler)
Definition: ansi_c_parser.h:29
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
std::list< exprt > pragma_pack
Definition: ansi_c_parser.h:59
bool asm_block_following
Definition: ansi_c_parser.h:56
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
Definition: ansi_c_parser.h:71
ansi_c_identifiert identifiert
Definition: ansi_c_parser.h:77
void add_declarator(exprt &declaration, irept &declarator)
ansi_c_scopet scopet
Definition: ansi_c_parser.h:78
bool parse() override
Definition: ansi_c_parser.h:49
scopet & root_scope()
Definition: ansi_c_parser.h:83
bool __float128_is_keyword
Definition: ansi_c_parser.h:72
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:27
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
unsigned parenthesis_counter
Definition: ansi_c_parser.h:57
configt::ansi_ct::flavourt modet
Definition: ansi_c_parser.h:61
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
Definition: ansi_c_parser.h:80
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.
scopet & current_scope()
Definition: ansi_c_parser.h:98
std::string string_literal
Definition: ansi_c_parser.h:58
irep_idt lookup_label(const irep_idt base_name)
const scopet & root_scope() const
Definition: ansi_c_parser.h:88
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
std::string prefix
Definition: ansi_c_scope.h:47
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
Definition: parser.h:24
The type of an expression, extends irept.
Definition: type.h:29
Parser utilities.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463