aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2019-04-08 16:51:12 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2019-04-16 18:33:34 +0200
commit5cee733c33bd53c0f58e9896f238ab862e224e46 (patch)
treec0ab63ad6c026703802c66535d86b600247ff91f
parentbfadad2c55c2088ee66de974bf2ad98b051c92cc (diff)
downloadcompcert-5cee733c33bd53c0f58e9896f238ab862e224e46.tar.gz
compcert-5cee733c33bd53c0f58e9896f238ab862e224e46.zip
Reset scope ids later.
In order to avoid adding ranges to the wrong scopes due to inlining they are numbered consecutively for the whole compilation unit. Bug 26234
-rw-r--r--cparser/Unblock.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index da8049a5..66b497cc 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -340,7 +340,6 @@ and unblock_block env ctx ploc = function
let unblock_fundef env f =
local_variables := [];
- next_scope_id := 0;
curr_fun_id:= f.fd_name.stamp;
(* TODO: register the parameters as being declared in function scope *)
let body = unblock_stmt env [] no_loc f.fd_body in
@@ -398,5 +397,6 @@ let rec unblock_glob env accu = function
(* Entry point *)
let program p =
+ next_scope_id := 0;
{gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
unblock_glob (Builtins.environment()) [] p