From 49eb46df9bf722d0f528f52dbfcb2c8a524ede19 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 4 Dec 2023 19:08:36 +0100 Subject: [PATCH] Cleanup --- src/cdomains/apron/relationDomain.apron.ml | 59 ++++++++++------------ 1 file changed, 26 insertions(+), 33 deletions(-) diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index e68540c41b..aca2346820 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -1,7 +1,7 @@ (** Signatures for relational value domains. See {!ApronDomain} and {!AffineEqualityDomain}. *) - +open GobApron open Batteries open GoblintCil @@ -11,23 +11,6 @@ sig val var_name: t -> string end -module VarMetadataTbl (VM: VarMetadata) = -struct - open GobApron - module VH = Hashtbl.Make (Var) - - let vh = VH.create 113 - - let make_var ?name metadata = - let name = Option.default_delayed (fun () -> VM.var_name metadata) name in - let var = Var.of_string name in - VH.replace vh var metadata; - var - - let find_metadata (var: Var.t) = - VH.find_option vh var -end - module VM = struct type t = @@ -45,10 +28,26 @@ struct | Global g -> g.vname end +module VarMetadataTbl (VM: VarMetadata) = +struct + module VH = Hashtbl.Make (Var) + + let vh = VH.create 113 + + let make_var ?name metadata = + let name = Option.default_delayed (fun () -> VM.var_name metadata) name in + let var = Var.of_string name in + VH.replace vh var metadata; + var + + let find_metadata (var: Var.t) = + VH.find_option vh var +end + module type RV = sig - type t = GobApron.Var.t - type vartable + type t = Var.t + type vartable = VM.t VarMetadataTbl (VM).VH.t val vh: vartable val make_var: ?name:string -> VM.t -> t @@ -60,13 +59,13 @@ sig val to_cil_varinfo: t -> varinfo Option.t end -module V: (RV with type vartable = VM.t VarMetadataTbl (VM).VH.t) = +module V: RV = struct - open GobApron + open VM + type t = Var.t module VMT = VarMetadataTbl (VM) include VMT - open VM type vartable = VM.t VMT.VH.t @@ -81,12 +80,6 @@ struct | _ -> None end -module type LinCons = -sig - type t - val num_vars: t -> int -end - module type Tracked = sig val type_tracked: typ -> bool @@ -96,7 +89,7 @@ end module type S2 = sig type t - type var = GobApron.Var.t + type var = Var.t type marshal module Tracked: Tracked @@ -135,8 +128,8 @@ module type S3 = sig include S2 - val cil_exp_of_lincons1: Apron.Lincons1.t -> exp option - val invariant: t -> Apron.Lincons1.t list + val cil_exp_of_lincons1: Lincons1.t -> exp option + val invariant: t -> Lincons1.t list end type ('a, 'b) relcomponents_t = { @@ -206,6 +199,6 @@ end module type RD = sig - module V : module type of struct include V end + module V : RV include S3 end