diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml index 22d08a628389a8585217a2e021dd8e381598a756..6bcf2d60866172e9f4e3e0889fa671f5c0d0dec4 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