From 0122d62d11d191ac26584cd38ee479a954688f36 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 31 Oct 2019 15:16:53 +0100
Subject: [PATCH] [kernel] Removes renaming phase in Cabs2Cil (done by Cil)
---
src/kernel_internals/typing/cabs2cil.ml | 18 +-----------------
1 file changed, 1 insertion(+), 17 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a1f20a0caa8..b14ad59df17 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1135,23 +1135,7 @@ let alphaConvertVarAndAddToEnv addtoenv vi =
because of previous occurrence at %a"
vi.vname newname Cil_printer.pp_location oldloc;
end
- end else begin
- (* favor renaming ghost variables over non-ghost ones *)
- if not vi.vghost then begin
- let siblings =
- fst @@ List.split @@
- Datatype.String.Hashtbl.find_all ghost_env vi.vname
- in
- let check = function
- | EnvVar vi' -> vi!=vi' && vi.vname = vi'.vname
- | _ -> false
- in
- match List.find_opt check siblings with
- | Some (EnvVar ({ vghost = true } as oldvi)) ->
- oldvi.vname <- newname; vi
- | _ -> copyVarinfo vi newname
- end else copyVarinfo vi newname
- end
+ end else copyVarinfo vi newname
end
in
(* Store all locals in the slocals (in reversed order). *)
--
GitLab