diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml
index 727d2c77733d52b85bd88b6e909f69f36e46f6a5..b4d470ca682c49a31e0f02f6a45fe08c879d9dd7 100644
--- a/src/kernel_internals/typing/alpha.ml
+++ b/src/kernel_internals/typing/alpha.ml
@@ -161,7 +161,7 @@ let get_suffix_idx rename_mode infix =
* been used. *)
let alphaWorker ~(alphaTable: 'a alphaTable)
- ?undolist
+ ~undolist
~(lookupname: string) ~(data:'a)
(make_new: bool) : string * 'a =
let prefix, infix = splitNameForAlpha ~lookupname in
@@ -184,9 +184,7 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
(fun fmt (s,_) -> Format.fprintf fmt "%s" (Integer.to_string s)))
suffixes;
(* Save the undo info *)
- (match undolist with
- Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
- | _ -> ());
+ Option.iter (fun l -> l := AlphaChangedSuffix (rc, !rc) :: !l) undolist;
let newname, newmin, (olddata: 'a), newsuffixes =
match
List.filter (fun (n, _) -> Integer.equal n curr_idx) suffixes
@@ -211,9 +209,7 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
H.add
infixes newinfix
(ref (Integer.minus_one, [(Integer.minus_one, data)]));
- (match undolist with
- | Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
- | None -> ());
+ Option.iter (fun l -> l := AlphaAddedSuffix (prefix, newsuffix) :: !l) undolist;
base ^ newsuffix, newmin, l, (newmin, data) :: suffixes
end else lookupname, min, data, suffixes
| _ -> (Kernel.fatal "Cil.alphaWorker")
@@ -239,12 +235,12 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
newname, olddata
-let newAlphaName ~alphaTable ?undolist ~lookupname ~data =
- alphaWorker ~alphaTable ?undolist ~lookupname ~data true
+let newAlphaName ~alphaTable ~undolist ~lookupname ~data =
+ alphaWorker ~alphaTable ~undolist ~lookupname ~data true
(** Just register the name so that we will not use in the future *)
-let registerAlphaName ~alphaTable ?undolist ~lookupname ~data =
- ignore (alphaWorker ~alphaTable ?undolist ~lookupname ~data false)
+let registerAlphaName ~alphaTable ~lookupname ~data =
+ ignore (alphaWorker ~alphaTable ~undolist:None ~lookupname ~data false)
let getAlphaPrefix ~lookupname = splitNameForAlpha ~lookupname
diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 9101266f4187f9bad0896d686939301ff27b8c3b..ca29d22cc941731502af181e11db2856cfbcb98f 100644
--- a/src/kernel_internals/typing/alpha.mli
+++ b/src/kernel_internals/typing/alpha.mli
@@ -73,14 +73,13 @@ type 'a alphaTable =
* previous occurrence. This function knows about the location implicitly
* from the [(Cil.CurrentLoc.get ())]. *)
val newAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
+ undolist: 'a undoAlphaElement list ref option ->
lookupname:string -> data:'a -> string * 'a
(** Register a name with an alpha conversion table to ensure that when later
* we call newAlphaName we do not end up generating this one *)
val registerAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
lookupname:string -> data:'a -> unit
(** Split the name in preparation for newAlphaName. Returns a pair
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 703a2ea9f3b3548161133d0236d1928de8340b5d..953c0e68aca05f8b62e83ef531a97f8922ae892e 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -967,7 +967,7 @@ let alphaTable : location Alpha.alphaTable = H.create 307
* foo" or "union bar" *)
let fresh_global lookupname =
- fst (Alpha.newAlphaName alphaTable lookupname (CurrentLoc.get ()))
+ fst (Alpha.newAlphaName alphaTable None lookupname (CurrentLoc.get ()))
(* To keep different name scopes different, we add prefixes to names
* specifying the kind of name: the kind can be one of "" for variables or
@@ -1026,7 +1026,7 @@ let newAlphaName
in
let data = CurrentLoc.get () in
let newname, oldloc =
- Alpha.newAlphaName ~alphaTable ?undolist ~lookupname ~data
+ Alpha.newAlphaName ~alphaTable ~undolist ~lookupname ~data
in
(match undo_scope, undolist with
| None, None -> ()
@@ -1199,7 +1199,7 @@ let get_temp_name ghost () =
let data = CurrentLoc.get() in
let name = if ghost then "g_tmp" else "tmp" in
let name, _ =
- Alpha.newAlphaName ~alphaTable ~undolist ~lookupname:name ~data
+ Alpha.newAlphaName ~alphaTable ~undolist:(Some undolist) ~lookupname:name ~data
in
let undolist = !undolist in
Alpha.undoAlphaChanges ~alphaTable ~undolist;
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 3438e59ff51819ce28c437e4f00287ca463da39e..d9cb57f9193b322f97e4f69dbc54ca15714123a6 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -340,7 +340,7 @@ let computeFileCFG (f : file) =
let labelAlphaTable : unit Alpha.alphaTable = Hashtbl.create 11
let freshLabel (base:string) =
- fst (Alpha.newAlphaName labelAlphaTable base ())
+ fst (Alpha.newAlphaName labelAlphaTable None base ())
let xform_switch_block ?(keepSwitch=false) b =
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 5815b0145f26b0ab9c25bee502028062e76cdb18..9f5080a17cfde646576a6b769ddd491a2792a84e 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -618,7 +618,7 @@ module EnumMerging =
(e2.ename <-
fst
(Alpha.newAlphaName
- aeAlpha e2.ename Cil_datatype.Location.unknown);
+ aeAlpha None e2.ename Cil_datatype.Location.unknown);
Kernel.debug ~dkey:Kernel.dkey_linker
"new anonymous name %s" e2.ename;
false))))
@@ -1403,7 +1403,7 @@ let update_compinfo ci =
in
Alpha.registerAlphaName sAlpha ci.cname loc;
let orig_name = if ci.corig_name = "" then ci.cname else ci.corig_name in
- let n, _ = Alpha.newAlphaName sAlpha orig_name loc in
+ let n, _ = Alpha.newAlphaName sAlpha None orig_name loc in
let oldnode = PlainMerging.find true node in
if oldnode == node then begin
let node =
@@ -1440,7 +1440,7 @@ let rec update_type_repr t =
| None -> Cil_datatype.Location.unknown
in
Alpha.registerAlphaName vtAlpha ti.tname loc;
- let n,_ = Alpha.newAlphaName vtAlpha ti.torig_name loc in
+ let n,_ = Alpha.newAlphaName vtAlpha None ti.torig_name loc in
let oldnode = PlainMerging.find true node in
if oldnode == node then begin
let node =
@@ -1851,7 +1851,7 @@ let oneFilePass1 (f:file) : unit =
let orig_name =
if ei.eorig_name = "" then ei.ename else ei.eorig_name
in
- ignore (Alpha.newAlphaName aeAlpha orig_name l);
+ ignore (Alpha.newAlphaName aeAlpha None orig_name l);
ei.ereferenced <- false;
ignore
(EnumMerging.getNode eEq eSyn !currentFidx ei ei
@@ -2670,7 +2670,7 @@ let oneFilePass2 (f: file) =
(* Maybe it is static. Rename it then *)
if vi.vstorage = Static then begin
let newName, _ =
- Alpha.newAlphaName vtAlpha vi.vname (CurrentLoc.get ())
+ Alpha.newAlphaName vtAlpha None vi.vname (CurrentLoc.get ())
in
let formals_decl =
try Some (Cil.getFormalsDecl vi)
@@ -3026,7 +3026,7 @@ let oneFilePass2 (f: file) =
if ci.corig_name = "" then ci.cname else ci.corig_name
in
let newname, _ =
- Alpha.newAlphaName sAlpha orig_name (CurrentLoc.get ())
+ Alpha.newAlphaName sAlpha None orig_name (CurrentLoc.get ())
in
ci.cname <- newname;
ci.creferenced <- true;
@@ -3055,7 +3055,7 @@ let oneFilePass2 (f: file) =
if ei.eorig_name = "" then ei.ename else ei.eorig_name
in
let newname, _ =
- Alpha.newAlphaName eAlpha orig_name (CurrentLoc.get ())
+ Alpha.newAlphaName eAlpha None orig_name (CurrentLoc.get ())
in
ei.ename <- newname;
ei.ereferenced <- true;
@@ -3064,7 +3064,7 @@ let oneFilePass2 (f: file) =
List.iter
(fun item ->
let newname,_ =
- Alpha.newAlphaName vtAlpha item.eiorig_name item.eiloc
+ Alpha.newAlphaName vtAlpha None item.eiorig_name item.eiloc
in
item.einame <- newname)
ei.eitems;
@@ -3108,7 +3108,7 @@ let oneFilePass2 (f: file) =
with
None -> (* We must rename it and keep it *)
let newname, _ =
- Alpha.newAlphaName vtAlpha ti.torig_name (CurrentLoc.get ())
+ Alpha.newAlphaName vtAlpha None ti.torig_name (CurrentLoc.get ())
in
ti.tname <- newname;
ti.treferenced <- true;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 0edffb0dd95d3c08071125f6d65856aa016648ff..63e9bbc9a072dfc6b7a3e54751e03e526a397b4f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6219,7 +6219,8 @@ let uniqueVarNames (f: file) : unit =
let data = CurrentLoc.get () in
let newname, oldloc =
Alpha.newAlphaName
- ~alphaTable:gAlphaTable ~undolist ~lookupname ~data
+ ~alphaTable:gAlphaTable ~undolist:(Some undolist)
+ ~lookupname ~data
in
if false && newname <> v.vname then (* Disable this warning *)
Kernel.warning