File tree Expand file tree Collapse file tree 3 files changed +30
-0
lines changed
regression/cbmc/cprover_id1 Expand file tree Collapse file tree 3 files changed +30
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+
3
+ void foo ()
4
+ {
5
+ static int local ;
6
+ local = 1 ;
7
+ }
8
+
9
+ int main ()
10
+ {
11
+ // foo::1::local is the fully qualified name generated by the C front-end at
12
+ // this time. This is an implementation detail that could change at any time,
13
+ // and the test would need to be adjusted accordingly.
14
+ assert (__CPROVER_ID "foo::1::local" == 0 );
15
+ foo ();
16
+ assert (__CPROVER_ID "foo::1::local" == 1 );
17
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ ^VERIFICATION SUCCESSFUL$
7
+ --
8
+ ^warning: ignoring
9
+ --
10
+ This test demonstrates the use of __CPROVER_ID to form identifier names that
11
+ would not otherwise constitute syntactically identifiers in C code.
Original file line number Diff line number Diff line change @@ -297,6 +297,8 @@ identifier:
297
297
TOK_IDENTIFIER
298
298
| TOK_CPROVER_ID TOK_STRING
299
299
{
300
+ // construct an identifier from a string that would otherwise not be a
301
+ // valid identifier in C
300
302
$$ =$1 ;
301
303
parser_stack ($$).id(ID_symbol);
302
304
irep_idt value=parser_stack($2 ).get(ID_value);
You can’t perform that action at this time.
0 commit comments