diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 5a7c98edd..019f7e04c 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -351,7 +351,8 @@ let genv : (string, envdata * location) H.t = H.create 307 hash table easily *) type undoScope = UndoRemoveFromEnv of string - | UndoResetAlphaCounter of location AL.alphaTableData ref * + | UndoResetAlphaCounter of string * + location AL.alphaTableData ref * location AL.alphaTableData | UndoRemoveFromAlphaTable of string @@ -426,14 +427,29 @@ let newAlphaName (globalscope: bool) (* The name should have global scope *) let prefix = AL.getAlphaPrefix ~lookupname:lookupname in try let countref = H.find alphaTable prefix in - s := (UndoResetAlphaCounter (countref, !countref)) :: !s + s := (UndoResetAlphaCounter (prefix, countref, !countref)) :: !s with Not_found -> s := (UndoRemoveFromAlphaTable prefix) :: !s end | _ :: rest -> findEnclosingFun rest in if not globalscope then - findEnclosingFun !scopes; + findEnclosingFun !scopes + else ( + let rec checkScopes = (function + [s] -> + let prefix = AL.getAlphaPrefix ~lookupname:lookupname in + s := List.filter (function + UndoResetAlphaCounter (p, _, _) when p = prefix -> false + | UndoRemoveFromAlphaTable p when p = prefix -> false + | _ -> true + ) !s + | _ :: rest -> checkScopes rest + | _ -> () + ) + in + checkScopes !scopes + ); let newname, oldloc = AL.newAlphaName ~alphaTable:alphaTable ~undolist:None ~lookupname:lookupname ~data:!currentLoc in stripKind kind newname, oldloc @@ -502,7 +518,7 @@ let exitScope () = | UndoRemoveFromEnv n :: t -> H.remove env n; loop t | UndoRemoveFromAlphaTable n :: t -> H.remove alphaTable n; loop t - | UndoResetAlphaCounter (vref, oldv) :: t -> + | UndoResetAlphaCounter (_, vref, oldv) :: t -> vref := oldv; loop t in diff --git a/test/small1/scope13.c b/test/small1/scope13.c new file mode 100644 index 000000000..cbb7b9654 --- /dev/null +++ b/test/small1/scope13.c @@ -0,0 +1,27 @@ +/* Note how the statics each have the same name as a formal parameter, + * hiding it. This has consequences for the alpha table scope handling. */ +#include + +static int +b(int *p) +{ + { + static int p[] = { 41 }; + return p[0]; + } +} +int +c(int *p) +{ + { + static int p[] = { 42 }; + return b(p); + } +} + +int main(void) +{ + int x = 3; + if (c(&x) != 41) abort(); + return 0; +} \ No newline at end of file diff --git a/test/testcil.pl b/test/testcil.pl index 40e01b4a2..30a24bc60 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -371,10 +371,11 @@ sub addToGroup { addTest("testrun/scope5 _GNUCC=1"); addTest("testrun/scope6"); addTest("testrun/scope8"); -addTest("testrun/scope9 "); -addTest("testrun/scope10 "); -addTest("testrun/scope11 "); -addTest("test/scope12 "); +addTest("testrun/scope9"); +addTest("testrun/scope10"); +addTest("testrun/scope11"); +addTest("test/scope12"); +addTest("test/scope13"); addTest("test/voidstar"); addTest("testrun/memcpy1"); addTest("testrun/land_expr");