From a71cec602c3c3ab3284d38ef928f16a23bc94a21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 15 Feb 2019 16:19:03 +0100
Subject: [PATCH] [Eva] Fixes the storage of unmarshallable domains.
---
src/plugins/value/domains/domain_store.ml | 28 +++++++++++++++++++++--
1 file changed, 26 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 22d08a62838..6bcf2d60866 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -40,14 +40,38 @@ module Make (Domain: InputDomain) = struct
let dependencies = [ Db.Value.self ]
let size = 16
- module Storage =
- State_builder.Ref (Datatype.Bool)
+ module type Ref = sig
+ val get : unit -> bool
+ val set : bool -> unit
+ end
+
+ (* Boolean reference saved on the disk. *)
+ module Bool_Ref_State =
+ State_builder.Ref
+ (Datatype.Bool)
(struct
let dependencies = dependencies
let name = name ^ ".Storage"
let default () = false
end)
+ (* Boolean reference. Not saved on the disk. *)
+ module Bool_Ref = struct
+ let x = ref false
+ let set y = x := y
+ let get () = !x
+ end
+
+ (* A boolean reference indicating whether the states of the domain have been
+ saved. False by default, it becomes true when the engine calls
+ [register_global_state] at the start of the analysis.
+ If the domain is unmarshallable, its states cannot be saved on the
+ disk, and this boolean should not be saved either. *)
+ module Storage =
+ (val (if Descr.is_unmarshable Domain.descr
+ then (module Bool_Ref)
+ else (module Bool_Ref_State)) : Ref)
+
module Global_State =
State_builder.Option_ref (Domain)
(struct
--
GitLab