Skip to content

Commit 87c5948

Browse files
committed
C front-end: Record extern declarations in current scope
Previously, extern declarations would only be recorded in the global scope. While they do belong to the global scope, they still need to take precedence in name lookups in the local/current scope as well. Also removing an unnecessary iostream include. Fixes: diffblue#1867
1 parent c801126 commit 87c5948

File tree

5 files changed

+68
-4
lines changed

5 files changed

+68
-4
lines changed

regression/cbmc/extern1/main.c

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <stdio.h>
2+
#include <assert.h>
3+
4+
int some_global = 10;
5+
6+
void shadow()
7+
{
8+
int some_global = 5;
9+
10+
printf("local: %d\n", some_global);
11+
{
12+
int some_global = 0;
13+
++some_global;
14+
printf("local2: %d\n", some_global);
15+
}
16+
17+
printf("local: %d\n", some_global);
18+
{
19+
extern int some_global;
20+
++some_global;
21+
printf("global: %d\n", some_global);
22+
assert(some_global == 11);
23+
}
24+
25+
assert(some_global == 5);
26+
}
27+
28+
int main(void)
29+
{
30+
shadow();
31+
}

regression/cbmc/extern1/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

regression/cbmc/extern2/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <stdio.h>
2+
#include <assert.h>
3+
4+
int param;
5+
void function(int param)
6+
{
7+
printf("%d\n", param);
8+
{
9+
extern int param;
10+
printf("%d\n", param);
11+
assert(param == 2);
12+
}
13+
assert(param == 1);
14+
}
15+
16+
int main(void)
17+
{
18+
param = 2;
19+
function(1);
20+
}

regression/cbmc/extern2/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

src/ansi-c/ansi_c_parser.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
88

99
#include "ansi_c_parser.h"
1010

11-
#include <iostream>
12-
1311
#include "c_storage_spec.h"
1412

1513
ansi_c_parsert ansi_c_parser;
@@ -35,8 +33,6 @@ ansi_c_id_classt ansi_c_parsert::lookup(
3533

3634
if(n_it!=it->name_map.end())
3735
{
38-
assert(id2string(n_it->second.prefixed_name)==
39-
it->prefix+id2string(scope_name));
4036
identifier=n_it->second.prefixed_name;
4137
return n_it->second.id_class;
4238
}
@@ -150,6 +146,9 @@ void ansi_c_parsert::add_declarator(
150146
ansi_c_identifiert &identifier=scope.name_map[base_name];
151147
identifier.id_class=id_class;
152148
identifier.prefixed_name=prefixed_name;
149+
150+
if(force_root_scope)
151+
current_scope().name_map[base_name] = identifier;
153152
}
154153

155154
ansi_c_declaration.declarators().push_back(new_declarator);

0 commit comments

Comments
 (0)