diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 57c91da7c3e5adeaec0514ec0a812b6f2a7e7da6..59bf19445ebf5ab7ae5c84c774aa3af77098cf5b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1585,7 +1585,9 @@ struct
end else SkipChildren
end
in
- let cleanup_var vi = vi.vtype <- Cil.visitCilType cleanup_types vi.vtype in
+ let cleanup_var vi =
+ Cil.update_var_type vi (Cil.visitCilType cleanup_types vi.vtype)
+ in
List.iter cleanup_var c.locals;
!currentFunctionFDEC.slocals <- !currentFunctionFDEC.slocals @ !vars;
let vars = !vars @ c.locals in
@@ -4332,7 +4334,7 @@ let fixFormalsType formals =
end
in
let treat_one_formal v =
- v.vtype <- Cil.visitCilType vis v.vtype;
+ Cil.update_var_type v (Cil.visitCilType vis v.vtype);
Hashtbl.add table v.vname v;
in
List.iter treat_one_formal formals
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index d8b6f8868179ff641e14b26f401c59ff928a1dfe..f1a939b213fea3855fc5daace5581dae11cbe600 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1733,7 +1733,7 @@ let oneFilePass1 (f:file) : unit =
"%s@\nOld declaration is unused, silently removing it"
msg;
ignore_vi oldvi;
- vi.vtype <- update_type_repr vi.vtype;
+ Cil.update_var_type vi (update_type_repr vi.vtype);
H.replace vEnv vi.vname vinode;
vinode.nrep <- vinode;
oldvinode.nrep <- vinode;
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index ca932fad3b227fb3d5e737cb2a127dbee1478fa9..a75151352f640348731a343532d6cfa4da1a5646 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -603,10 +603,13 @@ object(self)
(match v with
| Catch_all -> b
| Catch_exn (v,[]) ->
- v.vtype <- purify v.vtype; update_locals v b;assign_catched_obj v b; b
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b; b
| Catch_exn(v,aux) ->
let add_one_aux stmts (v,b) =
- v.vtype <- purify v.vtype; update_locals v b;
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
assign_catched_obj v b;
add_unreachable_block b :: stmts
in
@@ -615,7 +618,7 @@ object(self)
List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
in
let main_block = Cil.mkBlock aux_blocks in
- v.vtype <- purify v.vtype;
+ Cil.update_var_type v (purify v.vtype);
update_locals v main_block;
main_block)
in
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d9330b5ab30f40d29fe55592cb0e8b55df311915..1a2e39284a84cb0930db031a8a4c5600771d39a2 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -644,6 +644,14 @@ and enforceGhostBlockCoherence ?(force_ghost=false) block =
let force_ghost = force_ghost || is_ghost_else block in
List.iter (enforceGhostStmtCoherence ~force_ghost) block.bstmts
+(* makes sure that the type of a C variable and the type of its associated
+ logic variable -if any- stay synchronized. See bts 1538 *)
+let update_var_type v t =
+ v.vtype <- if v.vghost then typeAddGhost t else t;
+ match v.vlogic_var_assoc with
+ | None -> ()
+ | Some lv -> lv.lv_type <- Ctype t
+
(* Make a varinfo. Used mostly as a helper function below *)
let makeVarinfo
?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false) ?(loc=Location.unknown)
@@ -728,10 +736,10 @@ let setFormals (f: fundec) (forms: varinfo list) =
assert (getFormalsDecl f.svar == f.sformals);
match unrollType f.svar.vtype with
TFun(rt, _, isva, fa) ->
- f.svar.vtype <-
- TFun(rt,
- Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) forms),
- isva, fa)
+ update_var_type f.svar
+ (TFun(rt,
+ Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) forms),
+ isva, fa));
| _ ->
Kernel.fatal "Set formals. %s does not have function type" f.svar.vname
@@ -2649,9 +2657,10 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
let o = Visitor_behavior.Get_orig.logic_var vis#behavior lv in
visitCilLogicVarDecl vis o
in
- v.vtype <- visitCilType vis v.vtype;
+ let typ = visitCilType vis v.vtype in
v.vattr <- visitCilAttributes vis v.vattr;
v.vlogic_var_assoc <- optMapNoCopy visit_orig_var_assoc v.vlogic_var_assoc;
+ update_var_type v typ;
v
and visitCilVarUse vis v =
@@ -3610,7 +3619,7 @@ let getReturnType t =
let setReturnTypeVI (v: varinfo) (t: typ) =
match unrollType v.vtype with
| TFun (_, args, va, a) ->
- v.vtype <- TFun (t, args, va, a)
+ update_var_type v (TFun (t, args, va, a));
| _ -> Kernel.fatal "setReturnType: not a function type"
let setReturnType (f:fundec) (t:typ) =
@@ -5383,12 +5392,11 @@ let setFunctionType (f: fundec) (t: typ) =
if List.length f.sformals <> List.length args then
Kernel.fatal ~current:true "setFunctionType: number of arguments differs from the number of formals" ;
(* Change the function type. *)
- f.svar.vtype <- t;
+ update_var_type f.svar t;
(* Change the sformals and we know that indirectly we'll change the
* function type *)
List.iter2
- (fun (_an,at,aa) f ->
- f.vtype <- at; f.vattr <- aa)
+ (fun (_an,at,aa) f -> update_var_type f at; f.vattr <- aa)
args f.sformals
| _ -> Kernel.fatal ~current:true "setFunctionType: not a function type"
@@ -5402,7 +5410,7 @@ let setFunctionTypeMakeFormals (f: fundec) (t: typ) =
Kernel.fatal ~current:true "setFunctionTypMakeFormals called on function %s with some formals already"
f.svar.vname ;
(* Change the function type. *)
- f.svar.vtype <- t;
+ update_var_type f.svar t;
f.sformals <-
List.map (fun (n,t,_a) -> makeLocal ~formal:true f n t) args;
setFunctionType f t
@@ -6505,14 +6513,6 @@ let is_modifiable_lval lv =
| _ -> (not (isConstType t)
|| is_mutable_or_initialized lv) && isCompleteType t
-(* makes sure that the type of a C variable and the type of its associated
- logic variable -if any- stay synchronized. See bts 1538 *)
-let update_var_type v t =
- v.vtype <- if v.vghost then typeAddGhost t else t;
- match v.vlogic_var_assoc with
- | None -> ()
- | Some lv -> lv.lv_type <- Ctype t
-
(** Uniquefy the variable names *)
let uniqueVarNames (f: file) : unit =
(* Setup the alpha conversion table for globals *)
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index f3fe41bffc04fa6babd8b1ae1f333103ff93b641..74c0ccc46228142312e913fac4c99a8b5ee62e37 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -820,7 +820,7 @@ end = struct
let mytype = TFun(rt,Some args,va,attrs) in
let new_formals = List.map makeFormalsVarDecl args in
self#add_formals_bindings new_var new_formals;
- new_var.vtype <- mytype;
+ Cil.update_var_type new_var mytype;
List.iter2
(fun x y ->
Visitor_behavior.Set.varinfo self#behavior x y;
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 5cdbfc0f1e2ce52638d2a875594fc5b184183d98..b35db0760de8d187a2808397456db0636c0cfb48 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -248,7 +248,8 @@ let inliner functions_to_inline = object (self)
(* Inlining will prevent r to be syntactically seen as initialized
or const: *)
r.vdefined <- false;
- r.vtype <- Cil.typeRemoveAttributes ["const"] r.vtype;
+ Cil.update_var_type
+ r (Cil.typeRemoveAttributes ["const"] r.vtype);
false, None, (Cil.mkAddrOf loc (Cil.var r)) :: args
| Some _, _ ->
Kernel.fatal "Attempt to initialize an inexistent varinfo"
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index f7ad17a93863b45e27e6cea9e98eb0da3b421ec1..004941db6742cd482c8910fc0e7a1d3f3d0f197a 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -125,7 +125,7 @@ class visit_adding_code_for_synchronisation =
- what about varargs?
*)
let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
- vi_pre.vtype <- TFun(Cil.voidType, args, varargs,[]);
+ Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
vi_pre.vattr <- [];
(* in particular get rid of __no_return if set in vi*)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 40d9c3ea1a23bc99a9903513eaed31061c4a4ac6..58f3b018d525da5cea25fead897c3ca9e1a7a35a 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -584,7 +584,7 @@ let inject_in_fundec main fundec =
(* convert ghost variables *)
vi.vghost <- false;
let unghost_local vi =
- vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ;
+ Cil.update_var_type vi (Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype);
vi.vghost <- false
in
List.iter unghost_local fundec.slocals;
@@ -621,12 +621,12 @@ let unghost_vi vi =
(* do not convert extern ghost variables, because they can't be linked,
see bts #1392 *)
if vi.vstorage <> Extern then vi.vghost <- false;
- vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ;
+ Cil.update_var_type vi (Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype);
match Cil.unrollType vi.vtype with
| TFun(res, Some l, va, attr) ->
(* unghostify function's parameters *)
let retype (n, t, a) = n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a in
- vi.vtype <- TFun(res, Some (List.map retype l), va, attr)
+ Cil.update_var_type vi (TFun(res, Some (List.map retype l), va, attr))
| _ ->
()