cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
;
22
int
yyansi_cparse
(
ansi_c_parsert
&);
23
24
class
ansi_c_parsert
:
public
parsert
25
{
26
public
:
27
ansi_c_parse_treet
parse_tree
;
28
29
explicit
ansi_c_parsert
(
message_handlert
&message_handler)
30
:
parsert
(message_handler),
31
tag_following
(false),
32
asm_block_following
(false),
33
parenthesis_counter
(0),
34
mode
(
modet
::
NONE
),
35
cpp98
(false),
36
cpp11
(false),
37
for_has_scope
(false),
38
ts_18661_3_Floatn_types
(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
55
bool
tag_following
;
56
bool
asm_block_following
;
57
unsigned
parenthesis_counter
;
58
std::string
string_literal
;
59
std::list<exprt>
pragma_pack
;
60
61
typedef
configt::ansi_ct::flavourt
modet
;
62
modet
mode
;
63
64
// recognize C++98, C++11, C17, C23 keywords
65
bool
cpp98
,
cpp11
,
c17
,
c23
;
66
67
// in C99 and upwards, for(;;) has a scope
68
bool
for_has_scope
;
69
70
// ISO/IEC TS 18661-3:2015
71
bool
ts_18661_3_Floatn_types
;
72
bool
__float128_is_keyword
;
73
bool
float16_type
;
74
bool
bf16_type
;
75
bool
fp16_type
;
76
77
typedef
ansi_c_identifiert
identifiert
;
78
typedef
ansi_c_scopet
scopet
;
79
80
typedef
std::list<scopet>
scopest
;
81
scopest
scopes
;
82
83
scopet
&
root_scope
()
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
98
scopet
&
current_scope
()
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
¤t=
current_scope
();
121
scopes
.push_back(
scopet
());
122
scopes
.back().prefix=current.
prefix
+prefix;
123
}
124
125
ansi_c_id_classt
lookup
(
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
164
void
ansi_c_scanner_init
(
ansi_c_parsert
&);
165
166
#endif
// CPROVER_ANSI_C_ANSI_C_PARSER_H
ansi_c_parse_tree.h
yyansi_cparse
int yyansi_cparse(ansi_c_parsert &)
ansi_c_scanner_init
void ansi_c_scanner_init(ansi_c_parsert &)
ansi_c_scope.h
ansi_c_id_classt
ansi_c_id_classt
Definition
ansi_c_scope.h:18
ansi_c_declarationt
Definition
ansi_c_declaration.h:72
ansi_c_identifiert
Definition
ansi_c_scope.h:29
ansi_c_parse_treet
Definition
ansi_c_parse_tree.h:18
ansi_c_parsert
Definition
ansi_c_parser.h:25
ansi_c_parsert::float16_type
bool float16_type
Definition
ansi_c_parser.h:73
ansi_c_parsert::pragma_cprover_pop
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
Definition
ansi_c_parser.cpp:179
ansi_c_parsert::ansi_c_parsert
ansi_c_parsert(message_handlert &message_handler)
Definition
ansi_c_parser.h:29
ansi_c_parsert::set_pragma_cprover
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
Definition
ansi_c_parser.cpp:201
ansi_c_parsert::pragma_pack
std::list< exprt > pragma_pack
Definition
ansi_c_parser.h:59
ansi_c_parsert::asm_block_following
bool asm_block_following
Definition
ansi_c_parser.h:56
ansi_c_parsert::new_scope
void new_scope(const std::string &prefix)
Definition
ansi_c_parser.h:118
ansi_c_parsert::pragma_cprover_empty
bool pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
Definition
ansi_c_parser.cpp:169
ansi_c_parsert::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition
ansi_c_parser.h:71
ansi_c_parsert::tag_following
bool tag_following
Definition
ansi_c_parser.h:55
ansi_c_parsert::mode
modet mode
Definition
ansi_c_parser.h:62
ansi_c_parsert::identifiert
ansi_c_identifiert identifiert
Definition
ansi_c_parser.h:77
ansi_c_parsert::add_declarator
void add_declarator(exprt &declaration, irept &declarator)
Definition
ansi_c_parser.cpp:74
ansi_c_parsert::scopet
ansi_c_scopet scopet
Definition
ansi_c_parser.h:78
ansi_c_parsert::parse
bool parse() override
Definition
ansi_c_parser.h:49
ansi_c_parsert::for_has_scope
bool for_has_scope
Definition
ansi_c_parser.h:68
ansi_c_parsert::fp16_type
bool fp16_type
Definition
ansi_c_parser.h:75
ansi_c_parsert::c17
bool c17
Definition
ansi_c_parser.h:65
ansi_c_parsert::__float128_is_keyword
bool __float128_is_keyword
Definition
ansi_c_parser.h:72
ansi_c_parsert::parse_tree
ansi_c_parse_treet parse_tree
Definition
ansi_c_parser.h:27
ansi_c_parsert::pragma_cprover_stack
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
Definition
ansi_c_parser.h:161
ansi_c_parsert::parenthesis_counter
unsigned parenthesis_counter
Definition
ansi_c_parser.h:57
ansi_c_parsert::root_scope
scopet & root_scope()
Definition
ansi_c_parser.h:83
ansi_c_parsert::cpp98
bool cpp98
Definition
ansi_c_parser.h:65
ansi_c_parsert::current_scope
scopet & current_scope()
Definition
ansi_c_parser.h:98
ansi_c_parsert::bf16_type
bool bf16_type
Definition
ansi_c_parser.h:74
ansi_c_parsert::modet
configt::ansi_ct::flavourt modet
Definition
ansi_c_parser.h:61
ansi_c_parsert::add_tag_with_body
void add_tag_with_body(irept &tag)
Definition
ansi_c_parser.cpp:56
ansi_c_parsert::pragma_cprover_clash
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.
Definition
ansi_c_parser.cpp:194
ansi_c_parsert::root_scope
const scopet & root_scope() const
Definition
ansi_c_parser.h:88
ansi_c_parsert::scopest
std::list< scopet > scopest
Definition
ansi_c_parser.h:80
ansi_c_parsert::get_class
static ansi_c_id_classt get_class(const typet &type)
Definition
ansi_c_parser.cpp:147
ansi_c_parsert::lookup
ansi_c_id_classt lookup(const irep_idt &base_name, irep_idt &identifier, bool tag, bool label)
Definition
ansi_c_parser.cpp:13
ansi_c_parsert::cpp11
bool cpp11
Definition
ansi_c_parser.h:65
ansi_c_parsert::scopes
scopest scopes
Definition
ansi_c_parser.h:81
ansi_c_parsert::copy_item
void copy_item(const ansi_c_declarationt &declaration)
Definition
ansi_c_parser.h:112
ansi_c_parsert::pragma_cprover_push
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
Definition
ansi_c_parser.cpp:174
ansi_c_parsert::string_literal
std::string string_literal
Definition
ansi_c_parser.h:58
ansi_c_parsert::pop_scope
void pop_scope()
Definition
ansi_c_parser.h:93
ansi_c_parsert::lookup_label
irep_idt lookup_label(const irep_idt base_name)
Definition
ansi_c_parser.h:133
ansi_c_parsert::pragma_cprover_add_check
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
Definition
ansi_c_parser.cpp:184
ansi_c_parsert::decl_typet
decl_typet
Definition
ansi_c_parser.h:104
ansi_c_parsert::decl_typet::MEMBER
@ MEMBER
Definition
ansi_c_parser.h:104
ansi_c_parsert::decl_typet::PARAMETER
@ PARAMETER
Definition
ansi_c_parser.h:104
ansi_c_parsert::decl_typet::TAG
@ TAG
Definition
ansi_c_parser.h:104
ansi_c_parsert::c23
bool c23
Definition
ansi_c_parser.h:65
ansi_c_scopet
Definition
ansi_c_scope.h:40
ansi_c_scopet::prefix
std::string prefix
Definition
ansi_c_scope.h:47
exprt
Base class for all expressions.
Definition
expr.h:57
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::id
const irep_idt & id() const
Definition
irep.h:388
message_handlert
Definition
message.h:27
parsert::parsert
parsert(message_handlert &message_handler)
Definition
parser.h:33
typet
The type of an expression, extends irept.
Definition
type.h:29
complexity_violationt::NONE
@ NONE
Definition
complexity_violation.h:19
config.h
OTHER
@ OTHER
Definition
goto_program.h:36
parser.h
Parser utilities.
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
configt::ansi_ct::flavourt
flavourt
Definition
config.h:271
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
ansi-c
ansi_c_parser.h
Generated by
1.17.0