From e70719e67596e142aa092ba3f0b6db0e6fc80723 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 27 Jan 2022 11:21:02 +0100
Subject: [PATCH] [aorai] Use appropriate API for creating global variables
Meddling with mutable fields is not the proper way to do it
---
src/plugins/aorai/aorai_utils.ml | 3 +--
src/plugins/aorai/data_for_aorai.ml | 13 +++++++++----
src/plugins/aorai/yaparser.mly | 5 ++++-
3 files changed, 14 insertions(+), 7 deletions(-)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 077cc38480e..ca4ed6893bb 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -679,7 +679,6 @@ let add_global glob = globals_queue := glob :: !globals_queue
(* Utilities for global variables *)
let add_gvar ?init vi =
let initinfo = {Cil_types.init} in
- vi.vghost <- true;
vi.vstorage <- NoStorage;
add_global (GVar(vi,initinfo,vi.vdecl));
Globals.Vars.add vi initinfo;
@@ -700,7 +699,7 @@ let mk_gvar ?init ~ty name =
Globals.Vars.remove vi;
vi
with Not_found ->
- Cil.makeGlobalVar name ty
+ Cil.makeGlobalVar ~ghost:true name ty
in
add_gvar ?init vi
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 14d19b1b085..272897682ca 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -99,7 +99,7 @@ module State_var =
end)
let get_state_var =
- let add_var state = Cil.makeVarinfo true false state.name Cil.intType in
+ let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil.intType in
State_var.memo add_var
let get_state_logic_var state = Cil.cvar_to_lvar (get_state_var state)
@@ -339,7 +339,9 @@ let pebble_set_at li lab =
let memo_multi_state st =
match st.multi_state with
| None ->
- let aux = Cil.makeGlobalVar (get_fresh "aorai_aux") Cil.intType in
+ let aux =
+ Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil.intType
+ in
let laux = Cil.cvar_to_lvar aux in
let set = Cil_const.make_logic_info (get_fresh (st.name ^ "_pebble")) in
let typ = Logic_const.make_set_type (Ctype Cil.intType) in
@@ -572,7 +574,7 @@ let memo_aux_variable tr counter used_prms vi =
| Some _ -> TArray(vi.vtype,None,[])
in
let my_var =
- Cil.makeGlobalVar (get_fresh ("aorai_" ^ vi.vname)) my_type
+ Cil.makeGlobalVar ~ghost:true (get_fresh ("aorai_" ^ vi.vname)) my_type
in
add_aux_variable my_var;
let my_lvar = Cil.cvar_to_lvar my_var in
@@ -1156,7 +1158,9 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
else Cil.intType
in (* We won't always need a counter *)
lazy (
- let vi = Cil.makeGlobalVar (get_fresh "aorai_counter") ty in
+ let
+ vi = Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_counter") ty
+ in
add_aux_variable vi;
vi
)
@@ -1358,6 +1362,7 @@ let type_trans auto metaenv env tr =
let start = tr.start in
let count = (* TODO: make it an integer. *)
Cil.makeGlobalVar
+ ~ghost:true
(get_fresh ("aorai_cnt_" ^ start.name)) Cil.intType
in
add_aux_variable count;
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index fc6ea315e04..3e715519933 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -100,7 +100,10 @@ let add_metavariable map (name,typename) =
in
if Datatype.String.Map.mem name map then
Aorai_option.abort "The metavariable %s is declared twice" name;
- let vi = Cil.makeGlobalVar (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty in
+ let vi =
+ Cil.makeGlobalVar
+ ~ghost:true (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty
+ in
Datatype.String.Map.add name vi map
let check_state st =
--
GitLab