forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
1 parent
c801126
commit 87c5948
Showing
5 changed files
with
68 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
#include <stdio.h> | ||
#include <assert.h> | ||
|
||
int some_global = 10; | ||
|
||
void shadow() | ||
{ | ||
int some_global = 5; | ||
|
||
printf("local: %d\n", some_global); | ||
{ | ||
int some_global = 0; | ||
++some_global; | ||
printf("local2: %d\n", some_global); | ||
} | ||
|
||
printf("local: %d\n", some_global); | ||
{ | ||
extern int some_global; | ||
++some_global; | ||
printf("global: %d\n", some_global); | ||
assert(some_global == 11); | ||
} | ||
|
||
assert(some_global == 5); | ||
} | ||
|
||
int main(void) | ||
{ | ||
shadow(); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
CORE | ||
main.c | ||
|
||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
#include <stdio.h> | ||
#include <assert.h> | ||
|
||
int param; | ||
void function(int param) | ||
{ | ||
printf("%d\n", param); | ||
{ | ||
extern int param; | ||
printf("%d\n", param); | ||
assert(param == 2); | ||
} | ||
assert(param == 1); | ||
} | ||
|
||
int main(void) | ||
{ | ||
param = 2; | ||
function(1); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
CORE | ||
main.c | ||
|
||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "ansi_c_parser.h" | ||
|
||
#include <iostream> | ||
|
||
#include "c_storage_spec.h" | ||
|
||
ansi_c_parsert ansi_c_parser; | ||
|
@@ -35,8 +33,6 @@ ansi_c_id_classt ansi_c_parsert::lookup( | |
|
||
if(n_it!=it->name_map.end()) | ||
{ | ||
assert(id2string(n_it->second.prefixed_name)== | ||
it->prefix+id2string(scope_name)); | ||
identifier=n_it->second.prefixed_name; | ||
return n_it->second.id_class; | ||
} | ||
|
@@ -150,6 +146,9 @@ void ansi_c_parsert::add_declarator( | |
ansi_c_identifiert &identifier=scope.name_map[base_name]; | ||
identifier.id_class=id_class; | ||
identifier.prefixed_name=prefixed_name; | ||
|
||
if(force_root_scope) | ||
current_scope().name_map[base_name] = identifier; | ||
} | ||
|
||
ansi_c_declaration.declarators().push_back(new_declarator); | ||
|