diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 6b824e148255cae1864bdac625fb84c6a2931960..ebb94ce0f2ebec61ecac0b5e194eb7a3c887aa5c 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes | Bornat
+type mheap = Hoare | ZeroAlias | Eva | Bytes | Region | Typed of MemTyped.pointer
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -69,7 +69,7 @@ let descr_mheap d = function
| Typed p -> main d "typed" ; descr_mtyped d p
| Eva -> main d "eva"
| Bytes -> main d "bytes"
- | Bornat -> main d "bornat"
+ | Region -> main d "region"
let descr_mvar d = function
| Var -> ()
@@ -207,7 +207,7 @@ module Register(V : MemVar.VarUsage)(M : Sigs.Model)
module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
module Model_Hoare_Ref = Register(Ref)(MemEmpty)
-module Model_Typed_Var = Register(Var)(MemTyped) (* modèle de base, mettre MemBornat *)
+module Model_Typed_Var = Register(Var)(MemTyped)
module Model_Typed_Ref = Register(Ref)(MemTyped)
module Model_Bytes_Var = Register(Var)(MemBytes)
module Model_Bytes_Ref = Register(Ref)(MemBytes)
@@ -240,11 +240,11 @@ module Comp_Bytes_Var = MakeCompiler(Model_Bytes_Var)
module Comp_Bytes_Ref = MakeCompiler(Model_Bytes_Ref)
module Comp_MemVal = MakeCompiler(MemVal)
-module Comp_Bornat =
+module Comp_Region =
MakeCompiler
(MemVar.Make
(MemVar.Static)
- (MemBornat.MemMake(RegionAnalysis.R)(MemBytes)))
+ (MemRegion.MemMake(RegionAnalysis.R)(MemBytes)))
let compiler mheap mvar : (module Sigs.Compiler) =
@@ -260,7 +260,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Bytes, Raw -> (module Comp_MemBytes)
| Bytes, Var -> (module Comp_Bytes_Var)
| Bytes, Ref -> (module Comp_Bytes_Ref)
- | Bornat, _ -> (module Comp_Bornat)
+ | Region, _ -> (module Comp_Region)
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -279,7 +279,7 @@ let configure_mheap = function
Context.pop MemTyped.pointer orig_memtyped_pointer
in
rollback
- | Bornat -> MemBytes.configure ()
+ | Region -> MemBytes.configure ()
let configure_driver setup driver () =
let rollback_mheap = configure_mheap setup.mheap in
@@ -355,7 +355,7 @@ let update_config ~warning m s = function
| "TYPED" -> { s with mheap = Typed MemTyped.Fits }
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
| "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
- | "BORNAT" -> { s with mheap = Bornat }
+ | "REGION" -> { s with mheap = Region }
| "EVA" -> { s with mheap = Eva }
| "BYTES" -> { s with mheap = Bytes }
| "CAVEAT" -> { s with mvar = Caveat }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 9dfc86205758d5f4470b0dbe59ba841374e8fb89..741faf0c4268a07813bdf8ebbad13505b133cca2 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes | Bornat
+type mheap = Hoare | ZeroAlias | Eva | Bytes | Region | Typed of MemTyped.pointer
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index dc0f62a17c808236ccdad901680750091e857712..5e63f1f5ed5bebdd460ffd8e05f4babd1c2d84da 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -1132,7 +1132,7 @@ let scope seq scope xs =
[ p_equal (Sigma.value seq.post Alloc) alloc ]
(* ********************************************************************** *)
-(* API with BORNAT *)
+(* API with Region *)
(* ********************************************************************** *)
let sizeof = protected_sizeof_object
diff --git a/src/plugins/wp/MemBornat.ml b/src/plugins/wp/MemRegion.ml
similarity index 76%
rename from src/plugins/wp/MemBornat.ml
rename to src/plugins/wp/MemRegion.ml
index 641c6d54bb27f63cb17fa79550c06b460e460090..1304f3efd6b33cb9ebd118eb200541652778a7e4 100644
--- a/src/plugins/wp/MemBornat.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -1,4 +1,4 @@
-(**************************************************************************)
+(*************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
@@ -18,10 +18,10 @@
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
-(**************************************************************************)
+(*************************************************************************)
(* -------------------------------------------------------------------------- *)
-(* --- Bornat Memory Model --- *)
+(* --- Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
open Cil_types
@@ -71,13 +71,13 @@ struct
type region = R.region
- (****************************************************************************)
+ (***************************************************************************)
(* *)
(* Extern API *)
(* *)
- (****************************************************************************)
- let datatype = "MemBornat.Make"
- (** For projectification. Must be unique among models. *)
+ (***************************************************************************)
+ let datatype = "MemRegion.Make"
+ (* For projectification. Must be unique among models. *)
let configure () =
begin
@@ -86,18 +86,18 @@ struct
in
rollback
end
- (** Initializers to be run before using the model.
+ (* Initializers to be run before using the model.
Typically push {i Context} values and returns a function to rollback.
*)
let configure_ia ia = (* TODO *) M.configure_ia ia
- (** Given an automaton, return a vertex's binder.
+ (* Given an automaton, return a vertex's binder.
Currently used by the automata compiler to bind current vertex.
*)
let hypotheses p = M.hypotheses p
- (** Computes the memory model partitionning of the memory locations.
+ (* Computes the memory model partitionning of the memory locations.
This function typically adds new elements to the partition received
in input (that can be empty).
============================> TODO <======================================
@@ -110,8 +110,8 @@ struct
| CVal of R.region
| CInit of R.region
- let self = "MemBornat.Make.Chunk"
- (** Chunk names, for pretty-printing. *)
+ let self = "MemRegion.Make.Chunk"
+ (* Chunk names, for pretty-printing. *)
let hash = function
| CModel c -> M.Chunk.hash c
@@ -127,9 +127,9 @@ struct
let compare c1 c2 = (hash c1) - (hash c2)
let pretty fmt = function
- | CModel c -> Format.fprintf fmt "BornatModel.%a" M.Chunk.pretty c
- | CVal r -> Format.fprintf fmt "BornatVal.%a" R.pretty r
- | CInit r -> Format.fprintf fmt "BornatInit.%a" R.pretty r
+ | CModel c -> Format.fprintf fmt "RegionModel.%a" M.Chunk.pretty c
+ | CVal r -> Format.fprintf fmt "RegionVal.%a" R.pretty r
+ | CInit r -> Format.fprintf fmt "RegionInit.%a" R.pretty r
let tau_of_primitive = function
@@ -157,19 +157,19 @@ struct
| CModel _ -> "ModelChunk"
| CVal _ -> "ValueChunk"
| CInit _ -> "InitChunk"
- (** Used when generating fresh variables for a chunk. *)
+ (* Used when generating fresh variables for a chunk. *)
let is_framed = function
| CModel c -> M.Chunk.is_framed c
| CVal _ | CInit _ -> false
- (** Whether the chunk is local to a function call.
+ (* Whether the chunk is local to a function call.
Means the chunk is separated from anyother call side-effects.
If [true], entails that a function assigning everything can not modify
the chunk. Only used for optimisation, it would be safe to always
return [false]. *)
end
- (** Memory Chunks.
+ (* Memory Chunks.
The concrete memory is partionned into a vector of abstract data.
Each component of the partition is called a {i memory chunk} and
@@ -403,14 +403,14 @@ struct
(* ************************************************************************ *)
- (****************************************************************************)
- (** module Bornat : MemLoader.Module **)
- (****************************************************************************)
+ (***************************************************************************)
+ (* module Region : MemLoader.Module **)
+ (***************************************************************************)
- module Bornat = struct
+ module Region = struct
module Chunk = Chunk
module Sigma = Sigma
- let name = "BornatModel"
+ let name = "RegionModel"
type loc =
| Null of { repr : M.loc }
@@ -423,19 +423,19 @@ struct
let last sigma ty = function
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.last"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.last"
~effect:"Loc is NULL" "loc=%a" M.pretty repr ;
M.pointer_val M.null
| Loc { repr } -> M.last sigma.Tuple.model ty repr
- (** Conversion among loc, t_pointer terms and t_addr terms *)
+ (* Conversion among loc, t_pointer terms and t_addr terms *)
let to_addr = function
| Null { repr } -> M.pointer_val repr
| Loc { repr } -> M.pointer_val repr
let to_region_pointer = function
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.to_region_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.to_region_pointer"
~effect:"Pointer NULL shall not be parsed in this function" "%a" M.pretty repr ;
(0, M.pointer_val M.null)
| Loc { repr ; region } -> (R.id_of_region region, M.pointer_val repr)
@@ -443,42 +443,42 @@ struct
let of_region_pointer id _ty term =
if id == 0 then
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
~effect:"No region has been found" "Region_id is zero"
in Null { repr = M.pointer_loc term }
else match R.region_of_id id with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
~effect:"No region has been found" "Region_id=%d" id ;
Null { repr = M.pointer_loc term }
| Some region -> Loc { repr = M.pointer_loc term ; region }
- (** Basic operations *)
+ (* Basic operations *)
let sizeof ty = M.sizeof ty
let field loc field : loc = (* TODO: reconstruction *) match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"Loc is NULL" "(%a).(%a)" M.pretty repr Printer.pp_field field ;
assert false
| Loc { repr ; region } ->
match R.field region field with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"No region for field" "field:%a" Printer.pp_field field ;
Null { repr = M.field repr field }
| Some region -> Loc { repr = M.field repr field ; region }
let shift loc ty offset = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.shift"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.shift"
~effect:"Loc is NULL" "pointer=%a and ty=%a and offset=%a"
M.pretty repr Ctypes.pp_object ty QED.pretty offset ;
assert false
| Loc { repr ; region } ->
match R.shift region ty offset with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"No region for field" "offset:%a" QED.pretty offset ;
Null { repr = M.shift repr ty offset }
| Some region ->
@@ -487,7 +487,7 @@ struct
let frames ty loc chunk =
match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.frames"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.frames"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -514,7 +514,7 @@ struct
let havoc ty loc ~length chunk ~fresh ~current = match loc with
| Null _ ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.havoc"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.havoc"
~effect:"Loc is NULL" "NULL loc" ;
assert false
| Loc loc ->
@@ -527,7 +527,7 @@ struct
let eqmem ty loc chunk m1 m2 = match loc with
| Null _ ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.eqmem"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.eqmem"
~effect:"Loc is NULL" "NULL loc" ;
p_true
| Loc loc ->
@@ -538,7 +538,7 @@ struct
let eqmem_forall ty loc chunk m1 m2 =match loc with
| Null _ ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.eqmem_forall"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.eqmem_forall"
~effect:"Loc is NULL" "NULL loc" ;
[], p_true, p_true
| Loc loc ->
@@ -558,7 +558,7 @@ struct
let load_int sigma (c_int:c_int) loc : term =match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -567,7 +567,7 @@ struct
if compare_c_int c_int c_int' = 0
then F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
else
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"Type is not the same in chunk and in argument" "%a!=%a"
Ctypes.pp_int c_int Ctypes.pp_int c_int'
in
@@ -581,7 +581,7 @@ struct
let load_float sigma (c_float:c_float) loc : term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_float"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -590,7 +590,7 @@ struct
if compare_c_float c_float c_float' = 0
then F.e_get (Sigma.value sigma (CVal loc.region)) (M.pointer_val loc.repr)
else
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_float"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
~effect:"Type is not the same in chunk and in argument" "%a!=%a"
Ctypes.pp_float c_float Ctypes.pp_float c_float'
in
@@ -601,7 +601,7 @@ struct
else assert false
| R.Garbled -> M.load_float sigma.model c_float loc.repr
| _ ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_float"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
~effect:"Type is not the same in chunk and in argument" "%a"
Ctypes.pp_float c_float
in
@@ -609,13 +609,13 @@ struct
let load_pointer sigma ty loc : loc = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
match R.points_to loc.region with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
~effect:"No pointed loc" "Region=%a" R.pretty loc.region ;
assert false
| Some region ->
@@ -626,7 +626,7 @@ struct
M.pointer_loc @@ Sigma.value sigma (CVal loc.region)
| R.Garbled -> M.load_pointer sigma.Tuple.model ty loc.repr
| _ ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_pointer"
~effect:"Kind of region is not a pointer" "Region=%a" R.pretty loc.region ;
assert false
in Loc { repr ; region }
@@ -637,7 +637,7 @@ struct
let store_int sigma c_int loc v : Chunk.t * term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.store_int"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -657,7 +657,7 @@ struct
let store_float sigma c_float loc v : Chunk.t * term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.store_float"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.store_float"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -678,7 +678,7 @@ struct
let store_pointer sigma ty loc v : Chunk.t * term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.store_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.store_pointer"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -699,7 +699,7 @@ struct
let set_init_atom sigma loc v = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.set_init_atom"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.set_init_atom"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -714,7 +714,7 @@ struct
let is_init_atom sigma loc : term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.is_init_atom"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.is_init_atom"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -728,7 +728,7 @@ struct
let is_init_range sigma ty loc length : pred = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.is_init_range"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.is_init_range"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -742,7 +742,7 @@ struct
let set_init ty loc ~length chunk ~current : term = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.set_init"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.set_init"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
assert false
| Loc loc ->
@@ -762,7 +762,7 @@ struct
let rec value_footprint ty loc = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.value_footprint"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.value_footprint"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
Sigma.empty
| Loc loc ->
@@ -775,7 +775,7 @@ struct
| (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
Heap.Set.singleton (Chunk.CVal loc.region)
| (R.Many _ | R.Single _), (C_int _ | C_float _ | C_pointer _) ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.value_footprint"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.value_footprint"
~effect:"Type is not the same in chunk and in argument" "%a" Ctypes.pretty ty ;
Heap.Set.singleton (Chunk.CVal loc.region)
| _, C_comp { cfields } ->
@@ -789,7 +789,7 @@ struct
let rec init_footprint ty loc = match loc with
| Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.init_footprint"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.init_footprint"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
Sigma.empty
| Loc loc ->
@@ -802,7 +802,7 @@ struct
| (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
Heap.Set.singleton (Chunk.CInit loc.region)
| (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.init_footprint"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.init_footprint"
~effect:"Type is not the same in chunk and in argument" "%a != %a"
R.pp_kind k Ctypes.pretty ty ;
Heap.Set.singleton (Chunk.CInit loc.region)
@@ -817,16 +817,16 @@ struct
end
- type loc = Bornat.loc
+ type loc = Region.loc
type domain = Sigma.domain
type chunk = Chunk.t
type segment = loc rloc
- (****************************************************************************)
- module LOADER = MemLoader.Make(Bornat)
- (******************************************************************************)
+ (***************************************************************************)
+ module LOADER = MemLoader.Make(Region)
+ (*****************************************************************************)
let load = LOADER.load
let load_init = LOADER.load_init
@@ -840,7 +840,7 @@ struct
(*
let sloc_oget = function
| Sloc None -> Sloc M.null, None
- | Sloc (Some { Bornat.repr = repr }) -> Sloc repr
+ | Sloc (Some { Region.repr = repr }) -> Sloc repr
| Sarray (None,a,b) ->
| Srange (None,_,_,_)
| Sdescr (_,None,_) ->
@@ -848,22 +848,22 @@ struct
*)
let assigned seq ty sloc = match sloc with
- | Sloc (Bornat.Null _) | Sarray (Bornat.Null _,_,_)
- | Srange (Bornat.Null _,_,_,_) | Sdescr (_,Bornat.Null _,_) ->
+ | Sloc (Region.Null _) | Sarray (Region.Null _,_,_)
+ | Srange (Region.Null _,_,_,_) | Sdescr (_,Region.Null _,_) ->
LOADER.assigned seq ty sloc
| _ ->
(* Maintain always initialized values initialized *)
let region = match sloc with
- | Sloc (Bornat.Loc loc) | Sarray (Bornat.Loc loc, _, _)
- | Srange (Bornat.Loc loc, _, _, _)
- | Sdescr (_, Bornat.Loc loc, _) -> loc.region
- | Sloc (Bornat.Null _) | Sarray (Bornat.Null _,_,_) | Srange (Bornat.Null _,_,_,_)
- | Sdescr (_,Bornat.Null _,_) -> assert false
+ | Sloc (Region.Loc loc) | Sarray (Region.Loc loc, _, _)
+ | Srange (Region.Loc loc, _, _, _)
+ | Sdescr (_, Region.Loc loc, _) -> loc.region
+ | Sloc (Region.Null _) | Sarray (Region.Null _,_,_) | Srange (Region.Null _,_,_,_)
+ | Sdescr (_,Region.Null _,_) -> assert false
in
Assert (MemMemory.cinits (Sigma.value seq.post (Chunk.CInit region))) ::
LOADER.assigned seq ty sloc
- (** {2 Reversing the Model} *)
+ (* {2 Reversing the Model} *)
type state = M.state
@@ -878,188 +878,188 @@ struct
let iter = M.iter
let pretty fmt = function
- | Bornat.Null { repr } -> Format.fprintf fmt "{ NULL=%a }" M.pretty repr
- | Bornat.Loc loc -> Format.fprintf fmt "{ repr=%a ; region=%a }" M.pretty loc.repr R.pretty loc.region
+ | Region.Null { repr } -> Format.fprintf fmt "{ NULL=%a }" M.pretty repr
+ | Region.Loc loc -> Format.fprintf fmt "{ repr=%a ; region=%a }" M.pretty loc.repr R.pretty loc.region
- (** {2 Memory Model API} *)
+ (* {2 Memory Model API} *)
let vars = function
- | Bornat.Null _ -> Vars.empty
- | Bornat.Loc { repr } -> M.vars repr
- (** Return the logic variables from which the given location depend on. *)
+ | Region.Null _ -> Vars.empty
+ | Region.Loc { repr } -> M.vars repr
+ (* Return the logic variables from which the given location depend on. *)
let occurs var = function
- | Bornat.Null _ -> false
- | Bornat.Loc { repr } -> M.occurs var repr
- (** Test if a location depend on a given logic variable *)
+ | Region.Null _ -> false
+ | Region.Loc { repr } -> M.occurs var repr
+ (* Test if a location depend on a given logic variable *)
- let null = Bornat.Null { repr = M.null }
- (** Return the location of the null pointer *)
+ let null = Region.Null { repr = M.null }
+ (* Return the location of the null pointer *)
let literal ~eid:eid name =
let repr = M.literal ~eid name in
match R.literal ~eid name with
- | None -> Bornat.Null { repr }
- | Some region -> Bornat.Loc { repr ; region }
- (** Return the memory location of a constant string,
+ | None -> Region.Null { repr }
+ | Some region -> Region.Loc { repr ; region }
+ (* Return the memory location of a constant string,
the id is a unique identifier. *)
let cvar var =
match R.cvar var with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.cvar"
+ Warning.emit ~severe:false ~source:"MemRegion.cvar"
~effect:"No region for this var" "%a" Printer.pp_varinfo var ;
- Bornat.Null { repr = M.cvar var }
- | Some region -> Bornat.Loc { repr = M.cvar var ; region }
- (** Return the location of a C variable. *)
+ Region.Null { repr = M.cvar var }
+ | Some region -> Region.Loc { repr = M.cvar var ; region }
+ (* Return the location of a C variable. *)
let pointer_loc term =
let repr = M.pointer_loc term in
if QED.equal term @@ M.pointer_val M.null
- then Bornat.Null { repr }
+ then Region.Null { repr }
else match R.pointer_loc () with
- | None -> Bornat.Null { repr }
- | Some region -> Bornat.Loc { repr ; region }
- (** Interpret an address value (a pointer) as an abstract location.
+ | None -> Region.Null { repr }
+ | Some region -> Region.Loc { repr ; region }
+ (* Interpret an address value (a pointer) as an abstract location.
Might fail on memory models not supporting pointers. *)
let pointer_val = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.pointer_val"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.pointer_val"
~effect:"No region for this loc" "%a" M.pretty repr ;
M.pointer_val repr
- | Bornat.Loc { repr } -> M.pointer_val repr
- (** Return the adress value (a pointer) of an abstract location.
+ | Region.Loc { repr } -> M.pointer_val repr
+ (* Return the adress value (a pointer) of an abstract location.
Might fail on memory models not capable of representing pointers. *)
let field loc fieldinfo = match loc with
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.field"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.field"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Bornat.Null { repr = M.field repr fieldinfo }
- | Bornat.Loc loc ->
+ Region.Null { repr = M.field repr fieldinfo }
+ | Region.Loc loc ->
match R.field loc.region fieldinfo with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.field"
+ Warning.emit ~severe:false ~source:"MemRegion.field"
~effect:"No region for this field" "%a.%a" M.pretty loc.repr Printer.pp_field fieldinfo ;
- Bornat.Null { repr = M.field loc.repr fieldinfo }
- | Some region -> Bornat.Loc { repr = M.field loc.repr fieldinfo ; region }
- (** Return the memory location obtained by field access from a given
+ Region.Null { repr = M.field loc.repr fieldinfo }
+ | Some region -> Region.Loc { repr = M.field loc.repr fieldinfo ; region }
+ (* Return the memory location obtained by field access from a given
memory location. *)
let shift loc ty term = match loc with
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.shift"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.shift"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Bornat.Null { repr = M.shift repr ty term }
- | Bornat.Loc loc ->
+ Region.Null { repr = M.shift repr ty term }
+ | Region.Loc loc ->
match R.shift loc.region ty term with
| None ->
- Warning.emit ~severe:false ~source:"MemBornat.shift"
+ Warning.emit ~severe:false ~source:"MemRegion.shift"
~effect:"No region for this shift" "pointer=%a and ty=%a and offset=%a"
M.pretty loc.repr Ctypes.pp_object ty QED.pretty term;
- Bornat.Null { repr = M.shift loc.repr ty term }
- | Some region -> Bornat.Loc { repr = M.shift loc.repr ty term ; region }
- (** Return the memory location obtained by array access at an index
+ Region.Null { repr = M.shift loc.repr ty term }
+ | Some region -> Region.Loc { repr = M.shift loc.repr ty term ; region }
+ (* Return the memory location obtained by array access at an index
represented by the given {!term}. The element of the array are of
the given {!c_object} type. *)
let base_addr = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.base_addr"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.base_addr"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Bornat.Null { repr = M.base_addr repr }
- | Bornat.Loc loc -> Bornat.Loc {
+ Region.Null { repr = M.base_addr repr }
+ | Region.Loc loc -> Region.Loc {
repr = M.base_addr loc.repr ;
region = R.base_addr loc.region ;
}
- (** Return the memory location of the base address of a given memory
+ (* Return the memory location of the base address of a given memory
location. *)
let base_offset = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.base_offset"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.base_offset"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
M.base_offset repr
- | Bornat.Loc { repr } -> M.base_offset repr
- (** Return the offset of the location, in bytes, from its base_addr. *)
+ | Region.Loc { repr } -> M.base_offset repr
+ (* Return the offset of the location, in bytes, from its base_addr. *)
let block_length sigma ty = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.block_length"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.block_length"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
M.block_length sigma.Tuple.model ty repr
- | Bornat.Loc { repr } -> M.block_length sigma.Tuple.model ty repr
- (** Returns the length (in bytes) of the allocated block containing
+ | Region.Loc { repr } -> M.block_length sigma.Tuple.model ty repr
+ (* Returns the length (in bytes) of the allocated block containing
the given location. *)
let cast objs = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.cast"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.cast"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
- Bornat.Null { repr = M.cast objs repr }
- | Bornat.Loc loc -> Bornat.Loc { loc with repr = M.cast objs loc.repr }
- (** Cast a memory location into another memory location.
+ Region.Null { repr = M.cast objs repr }
+ | Region.Loc loc -> Region.Loc { loc with repr = M.cast objs loc.repr }
+ (* Cast a memory location into another memory location.
For [cast ty loc] the cast is done from [ty.pre] to [ty.post].
Might fail on memory models not supporting pointer casts. *)
let loc_of_int ty term =
let repr = M.loc_of_int ty term in
if QED.equal term @@ M.pointer_val M.null
- then Bornat.Null { repr }
+ then Region.Null { repr }
else match R.loc_of_int () with
- | None -> Bornat.Null { repr }
- | Some region -> Bornat.Loc { repr ; region }
+ | None -> Region.Null { repr }
+ | Some region -> Region.Loc { repr ; region }
let int_of_loc c_int = function
- | Bornat.Null { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.int_of_loc"
+ | Region.Null { repr } ->
+ Warning.emit ~severe:false ~source:"MemRegion.int_of_loc"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr ;
M.pointer_val repr
- | Bornat.Loc { repr } -> M.int_of_loc c_int repr
- (** Cast a memory location into its absolute memory address,
+ | Region.Loc { repr } -> M.int_of_loc c_int repr
+ (* Cast a memory location into its absolute memory address,
given as an integer with the given C-type. *)
let is_null = function
- | Bornat.Null { repr } -> M.is_null repr
- | Bornat.Loc { repr } -> M.is_null repr
- (** Return the formula that check if a given location is null *)
+ | Region.Null { repr } -> M.is_null repr
+ | Region.Loc { repr } -> M.is_null repr
+ (* Return the formula that check if a given location is null *)
let get_repr = function
- | Bornat.Null { repr } -> repr
- | Bornat.Loc { repr } -> repr
+ | Region.Null { repr } -> repr
+ | Region.Loc { repr } -> repr
let loc_eq loc_a loc_b = M.loc_eq (get_repr loc_a) (get_repr loc_b)
let loc_lt loc_a loc_b = M.loc_lt (get_repr loc_a) (get_repr loc_b)
let loc_neq loc_a loc_b = M.loc_neq (get_repr loc_a) (get_repr loc_b)
let loc_leq loc_a loc_b = M.loc_leq (get_repr loc_a) (get_repr loc_b)
- (** Memory location comparisons *)
+ (* Memory location comparisons *)
let loc_diff ty loc_a loc_b = M.loc_diff ty (get_repr loc_a) (get_repr loc_b)
- (** Compute the length in bytes between two memory locations *)
+ (* Compute the length in bytes between two memory locations *)
let get_rloc = function
- | Rloc (ty, Bornat.Null { repr }) -> Rloc (ty, repr)
- | Rloc (ty, Bornat.Loc loc) ->
+ | Rloc (ty, Region.Null { repr }) -> Rloc (ty, repr)
+ | Rloc (ty, Region.Loc loc) ->
Rloc (ty, loc.repr)
- | Rrange (Bornat.Null { repr }, ty, inf, sup) ->
+ | Rrange (Region.Null { repr }, ty, inf, sup) ->
Rrange (repr, ty, inf, sup)
- | Rrange (Bornat.Loc loc, ty, inf, sup) ->
+ | Rrange (Region.Loc loc, ty, inf, sup) ->
Rrange (loc.repr, ty, inf, sup)
let get_rloc_region = function
| Rloc (ty, loc) ->
- Rloc (ty, (match loc with Bornat.Null { repr } -> repr | Bornat.Loc { repr } -> repr)),
- (match loc with Bornat.Null _ -> None | Bornat.Loc { region } -> Some region)
+ Rloc (ty, (match loc with Region.Null { repr } -> repr | Region.Loc { repr } -> repr)),
+ (match loc with Region.Null _ -> None | Region.Loc { region } -> Some region)
| Rrange (loc, ty, inf, sup) ->
- Rrange ((match loc with Bornat.Null { repr } -> repr | Bornat.Loc { repr } -> repr), ty, inf, sup),
- (match loc with Bornat.Null _ -> None | Bornat.Loc { region } -> Some region)
+ Rrange ((match loc with Region.Null { repr } -> repr | Region.Loc { repr } -> repr), ty, inf, sup),
+ (match loc with Region.Null _ -> None | Region.Loc { region } -> Some region)
let valid sigma acs (rloc : loc rloc) = M.valid sigma.Tuple.model acs @@ get_rloc rloc
- (** Return the formula that tests if a memory state is valid
+ (* Return the formula that tests if a memory state is valid
(according to {!acs}) in the given memory state at the given
segment.
*)
@@ -1076,25 +1076,25 @@ struct
ValSigma.Chunk.Set.fold (fun r l -> frame_value sigma r :: l) (ValSigma.domain sigma.Tuple.value)
@@ InitSigma.Chunk.Set.fold (fun r l -> frame_init sigma r :: l) (InitSigma.domain sigma.Tuple.init)
@@ M.frame sigma.Tuple.model
- (** Assert the memory is a proper heap state preceeding the function
+ (* Assert the memory is a proper heap state preceeding the function
entry point. *)
let alloc sigma vars =
if vars = [] then sigma else { sigma with Tuple.model = M.alloc sigma.Tuple.model vars }
- (** Allocates new chunk for the validity of variables. *)
+ (* Allocates new chunk for the validity of variables. *)
let invalid sigma rloc = M.invalid sigma.Tuple.model (get_rloc rloc)
- (** Returns the formula that tests if the entire memory is invalid
+ (* Returns the formula that tests if the entire memory is invalid
for write access. *)
let scope sigma scope vars =
let m_sigma = { pre = sigma.pre.Tuple.model ; post = sigma.post.Tuple.model } in
M.scope m_sigma scope vars
- (** Manage the scope of variables. Returns the updated memory model
+ (* Manage the scope of variables. Returns the updated memory model
and hypotheses modeling the new validity-scope of the variables. *)
let global sigma p = M.global sigma.Tuple.model p
- (** Given a pointer value [p], assumes this pointer [p] (when valid)
+ (* Given a pointer value [p], assumes this pointer [p] (when valid)
is allocated outside the function frame under analysis. This means
separated from the formals and locals of the function. *)
@@ -1145,13 +1145,13 @@ struct
type region = R.region
- (****************************************************************************)
+ (***************************************************************************)
(* *)
(* Extern API *)
(* *)
- (****************************************************************************)
- let datatype = "MemBornat.Make"
- (** For projectification. Must be unique among models. *)
+ (***************************************************************************)
+ let datatype = "MemRegion.Make"
+ (* For projectification. Must be unique among models. *)
let configure () =
begin
@@ -1160,18 +1160,18 @@ struct
in
rollback
end
- (** Initializers to be run before using the model.
+ (* Initializers to be run before using the model.
Typically push {i Context} values and returns a function to rollback.
*)
let configure_ia ia = (* TODO *) M.configure_ia ia
- (** Given an automaton, return a vertex's binder.
+ (* Given an automaton, return a vertex's binder.
Currently used by the automata compiler to bind current vertex.
*)
let hypotheses p = M.hypotheses p
- (** Computes the memory model partitionning of the memory locations.
+ (* Computes the memory model partitionning of the memory locations.
This function typically adds new elements to the partition received
in input (that can be empty).
============================> TODO <======================================
@@ -1187,7 +1187,7 @@ struct
| CInit of R.region
| CGhost of R.region
- let self = "MemBornat.Make.BornatChunk"
+ let self = "MemRegion.Make.RegionChunk"
let hash = function
@@ -1230,7 +1230,7 @@ struct
| CGhost _ -> "GhostChunk"
| CVal _ -> "ValueChunk"
| CInit _ -> "InitChunk"
- (** Used when generating fresh variables for a chunk. *)
+ (* Used when generating fresh variables for a chunk. *)
let is_framed _ = false
@@ -1246,46 +1246,46 @@ struct
struct
type t =
| CModel of M.chunk
- | CBornat of BChunk.t
+ | CRegion of BChunk.t
- let self = "MemBornat.Make.Chunk"
- (** Chunk names, for pretty-printing. *)
+ let self = "MemRegion.Make.Chunk"
+ (* Chunk names, for pretty-printing. *)
let hash = function
| CModel c -> M.Chunk.hash c
- | CBornat c -> 0x1000 * (B.hash c)
+ | CRegion c -> 0x1000 * (B.hash c)
let equal ca cb = match ca, cb with
| CModel c1, CModel c2 -> M.Chunk.equal c1 c2
- | CBornat c1, CBornat c2 -> B.equal c1 c2
- | CModel _, CBornat _ | CBornat _, CModel _ -> false
+ | CRegion c1, CRegion c2 -> B.equal c1 c2
+ | CModel _, CRegion _ | CRegion _, CModel _ -> false
let compare c1 c2 = (hash c1) - (hash c2)
let pretty fmt = function
| CModel c -> Format.fprintf fmt "CModel.%a" M.Chunk.pretty c
- | CBornat c -> Format.fprintf fmt "CBornat.%a" B.pretty c
+ | CRegion c -> Format.fprintf fmt "CRegion.%a" B.pretty c
let tau_of_chunk = function
| CModel c -> M.Chunk.tau_of_chunk c
- | CBornat c -> B.tau_of_chunk c
+ | CRegion c -> B.tau_of_chunk c
let basename_of_chunk = function
| CModel _ -> "Model"
- | CBornat _ -> "Bornat"
- (** Used when generating fresh variables for a chunk. *)
+ | CRegion _ -> "Region"
+ (* Used when generating fresh variables for a chunk. *)
let is_framed = function
| CModel c -> M.Chunk.is_framed c
- | CBornat _ -> false
- (** Whether the chunk is local to a function call.
+ | CRegion _ -> false
+ (* Whether the chunk is local to a function call.
Means the chunk is separated from anyother call side-effects.
If [true], entails that a function assigning everything can not modify
the chunk. Only used for optimisation, it would be safe to always
return [false]. *)
end
- (** Memory Chunks.
+ (* Memory Chunks.
The concrete memory is partionned into a vector of abstract data.
Each component of the partition is called a {i memory chunk} and
@@ -1303,45 +1303,45 @@ struct
module Tuple = struct
type ('a, 'b) tuple = {
model : 'a ;
- bornat : 'b ;
+ region : 'b ;
}
let create f1 f2 input = {
model = f1 input ;
- bornat = f2 input ;
+ region = f2 input ;
}
let iter f1 f2 tuple =
f1 tuple.model ;
- f2 tuple.bornat ;
+ f2 tuple.region ;
()
let iter2 f1 f2 t1 t2 =
f1 t1.model t2.model ;
- f2 t1.bornat t2.bornat ;
+ f2 t1.region t2.region ;
()
let choose_apply f1 f2 tuple = function
| Chunk.CModel c -> f1 tuple.model c
- | Chunk.CBornat c -> f2 tuple.bornat c
+ | Chunk.CRegion c -> f2 tuple.region c
let choose_map f1 f2 tuple = function
| Chunk.CModel c -> { tuple with model = f1 tuple.model c }
- | Chunk.CBornat c -> { tuple with bornat = f2 tuple.bornat c }
+ | Chunk.CRegion c -> { tuple with region = f2 tuple.region c }
let map f1 f2 tuple = {
model = f1 tuple.model ;
- bornat = f2 tuple.bornat ;
+ region = f2 tuple.region ;
}
let map2 f1 f2 t1 t2 = {
model = f1 t1.model t2.model ;
- bornat = f2 t1.bornat t2.bornat ;
+ region = f2 t1.region t2.region ;
}
let sequence_map f1 f2 seq = {
model = f1 { pre = seq.pre.model ; post = seq.post.model } ;
- bornat = f2 { pre = seq.pre.bornat ; post = seq.post.bornat } ;
+ region = f2 { pre = seq.pre.region ; post = seq.post.region } ;
}
end
@@ -1362,9 +1362,9 @@ struct
(* local *)
let chunk_split_list l =
let rec aux acc1 acc2 = function
- | [] -> { model = List.rev acc1 ; bornat = List.rev acc2 }
+ | [] -> { model = List.rev acc1 ; region = List.rev acc2 }
| CModel c :: rest -> aux (c::acc1) acc2 rest
- | CBornat c :: rest -> aux acc1 (c::acc2) rest
+ | CRegion c :: rest -> aux acc1 (c::acc2) rest
in aux [] [] l
let of_domain (domain:domain) : dom =
@@ -1376,10 +1376,10 @@ struct
let to_domain (dom:dom) : domain =
let cmodel = M.Heap.Set.elements dom.model in
- let cbornat = BSigma.Chunk.Set.elements dom.bornat in
+ let cRegion = BSigma.Chunk.Set.elements dom.region in
let model = Heap.Set.of_list (List.map (fun c -> CModel c) cmodel) in
- let bornat = Heap.Set.of_list (List.map (fun c -> CBornat c) cbornat) in
- Heap.Set.union model bornat
+ let region = Heap.Set.of_list (List.map (fun c -> CRegion c) cRegion) in
+ Heap.Set.union model region
module Chunk = Heap
@@ -1389,7 +1389,7 @@ struct
let pretty fmt sigma =
Format.fprintf fmt "@[{@[%a@];@[%a@]}@]"
M.Sigma.pretty sigma.model
- BSigma.pretty sigma.bornat
+ BSigma.pretty sigma.region
let empty : domain = Heap.Set.empty
@@ -1405,19 +1405,19 @@ struct
let join sigma1 sigma2 =
let r = Tuple.map2 M.Sigma.join BSigma.join sigma1 sigma2 in
- Passive.union r.model r.bornat
+ Passive.union r.model r.region
let assigned ~pre:sigma1 ~post:sigma2 domain =
let dom = of_domain domain in
Bag.concat (M.Sigma.assigned ~pre:sigma1.model ~post:sigma2.model dom.model)
- @@ BSigma.assigned ~pre:sigma1.bornat ~post:sigma2.bornat dom.bornat
+ @@ BSigma.assigned ~pre:sigma1.region ~post:sigma2.region dom.region
let choose = Tuple.map2 M.Sigma.choose BSigma.choose
let merge s1 s2 =
let (sm, pm1, pm2) = M.Sigma.merge s1.model s2.model in
- let (sb, pb1, pb2) = BSigma.merge s1.bornat s2.bornat in
- let s = { model = sm ; bornat = sb } in
+ let (sb, pb1, pb2) = BSigma.merge s1.region s2.region in
+ let s = { model = sm ; region = sb } in
let p1 = Passive.union pm1 pb1 in
let p2 = Passive.union pm2 pb2 in
(s,p1,p2)
@@ -1435,12 +1435,12 @@ struct
let iter f =
Tuple.iter
(M.Sigma.iter (fun c -> f (CModel c)))
- (BSigma.iter (fun c -> f (CBornat c)))
+ (BSigma.iter (fun c -> f (CRegion c)))
let iter2 f =
Tuple.iter2
(M.Sigma.iter2 (fun c -> f (CModel c)))
- (BSigma.iter2 (fun c -> f (CBornat c)))
+ (BSigma.iter2 (fun c -> f (CRegion c)))
let havoc_chunk = Tuple.choose_map M.Sigma.havoc_chunk BSigma.havoc_chunk
@@ -1462,7 +1462,7 @@ struct
Chunk.Set.of_list
@@ List.append
(List.map (fun l -> CModel l) (M.Heap.Set.elements dom.model))
- (List.map (fun c -> CBornat c) (BHeap.Set.elements dom.bornat))
+ (List.map (fun c -> CRegion c) (BHeap.Set.elements dom.region))
let union = Chunk.Set.union
@@ -1473,14 +1473,14 @@ struct
(* ************************************************************************ *)
- (****************************************************************************)
- (** module Bornat : MemLoader.Module **)
- (****************************************************************************)
+ (***************************************************************************)
+ (* module Region : MemLoader.Module **)
+ (***************************************************************************)
- module Bornat = struct
+ module Region = struct
module Chunk = Chunk
module Sigma = Sigma
- let name = "BornatModel"
+ let name = "RegionModel"
type loc =
| Null
@@ -1494,16 +1494,16 @@ struct
let last sigma ty = function
| Null ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.last"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.last"
~effect:"Loc is NULL" "loc=NULL" ;
M.pointer_val M.null
| Raw { repr } ->
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.last"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.last"
~effect:"Loc is Raw" "loc=%a" M.pretty repr ;
M.last sigma.Tuple.model ty repr
| Loc { repr } -> M.last sigma.Tuple.model ty repr
- (** Conversion among loc, t_pointer terms and t_addr terms *)
+ (* Conversion among loc, t_pointer terms and t_addr terms *)
let to_addr = function
| Null -> M.pointer_val M.null
| Raw { repr } -> M.pointer_val repr
@@ -1518,32 +1518,32 @@ struct
if id == 0 then
if QED.equal term (M.pointer_val M.null) then Null else
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
~effect:"No region has been found" "Region_id is zero for loc=%a"
QED.pretty term
in Raw { repr = M.pointer_loc term }
else match R.region_of_id id with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.of_region_pointer"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.of_region_pointer"
~effect:"No region has been found" "Region_id=%d for term=%a" id
QED.pretty term
in Raw { repr = M.pointer_loc term }
| Some region -> Loc { repr = M.pointer_loc term ; region }
- (** Basic operations *)
+ (* Basic operations *)
let sizeof ty = M.sizeof ty
let field loc field : loc = (* TODO: reconstruction *) match loc with
| Null -> Null
| Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"Loc is Raw" "(%a).(%a)"
M.pretty repr Printer.pp_field field
in Raw { repr = M.field repr field }
| Loc { repr ; region } ->
match R.field region field with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"No region for field" "(%a in %a).(%a)"
M.pretty repr R.pretty region Printer.pp_field field
in Raw { repr = M.field repr field }
@@ -1552,14 +1552,14 @@ struct
let shift loc ty offset = match loc with
| Null -> Null
| Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.shift"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.shift"
~effect:"Loc is Raw" "No region for (%a).[%a : %a]"
M.pretty repr QED.pretty offset Ctypes.pp_object ty
in Raw { repr = M.shift repr ty offset }
| Loc { repr ; region } ->
match R.shift region ty offset with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.field"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.field"
~effect:"No region for shift" "No region for (%a in %a).[%a : %a]"
M.pretty repr R.pretty region QED.pretty offset Ctypes.pp_object ty
in Raw { repr = M.shift repr ty offset }
@@ -1581,10 +1581,10 @@ struct
| Null -> []
| Raw { repr } -> begin match chunk with
| Chunk.CModel c ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.frames"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.frames"
~effect:"Loc is Raw" "Frames %a" M.pretty repr
in M.frames ty repr c
- | Chunk.CBornat (B.CVal r | B.CInit r | B.CGhost r) ->
+ | Chunk.CRegion (B.CVal r | B.CInit r | B.CGhost r) ->
frames_repr_region ty repr r chunk
end
| Loc { repr ; region } -> frames_repr_region ty repr region chunk
@@ -1602,7 +1602,7 @@ struct
| Null ->
F.e_fun f_havoc [fresh;current;M.pointer_val M.null;length]
| Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.havoc"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.havoc"
~effect:"Loc is Raw" "havoc of Raw=%a"
M.pretty repr
in F.e_fun f_havoc [fresh;current;M.pointer_val repr;length]
@@ -1610,19 +1610,19 @@ struct
(* TO CHECK *) assert (QED.equal length F.e_one) ;
match chunk with
| Chunk.CModel c -> M.havoc ty repr ~length c ~fresh ~current
- | Chunk.CBornat _ ->
+ | Chunk.CRegion _ ->
F.e_fun f_havoc [fresh;current;M.pointer_val repr;length]
let eqmem_forall ty loc chunk m1 m2 = match loc, chunk with
| Null, Chunk.CModel c -> M.eqmem_forall ty M.null c m1 m2
- | Null, Chunk.CBornat _ ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.eqmem_forall"
+ | Null, Chunk.CRegion _ ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.eqmem_forall"
~effect:"Loc is NULL" "Los is Null in eqmem_forall"
in [], p_true, p_true
| (Raw { repr } | Loc { repr }), Chunk.CModel c ->
M.eqmem_forall ty repr c m1 m2
- | (Raw { repr } | Loc { repr }), Chunk.CBornat _ ->
+ | (Raw { repr } | Loc { repr }), Chunk.CRegion _ ->
let xp = Lang.freshvar ~basename:"b" MemAddr.t_addr in
let p = F.e_var xp in
let n = M.sizeof ty in
@@ -1636,22 +1636,22 @@ struct
let load_int sigma (c_int:c_int) loc : term = match loc with
| Null ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"Loc is Null" "Attempt to load_int inside Null"
in M.load_int sigma.Tuple.model c_int M.null
| Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"Loc is Raw" "load_int(Raw %a)" M.pretty repr
in M.load_int sigma.Tuple.model c_int repr
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.kind region with
| R.Many (R.Int c_int') ->
if compare_c_int c_int c_int' = 0
then F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
else
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"C_int type is not the same in chunk and in argument"
"%a!=%a" Ctypes.pp_int c_int Ctypes.pp_int c_int'
in F.e_get (Sigma.value sigma c)
@@ -1661,14 +1661,14 @@ struct
then Sigma.value sigma c
else
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"C_int type is not the same in chunk and in argument"
"%a!=%a" Ctypes.pp_int c_int Ctypes.pp_int c_int'
in Sigma.value sigma c
| R.Garbled -> M.load_int sigma.model c_int repr
| k ->
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_int"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_int"
~effect:"Region's kind is not Int" "%a : %a != %a"
R.pretty region R.pp_kind k Ctypes.pp_int c_int
in assert false
@@ -1676,23 +1676,23 @@ struct
let load_float sigma (c_float:c_float) loc : term = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_float"
+ ~source:"MemRegion.Region.load_float"
~effect:"Loc is Null" "Attempt to load_float inside Null"
in M.load_float sigma.Tuple.model c_float M.null
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_float"
+ ~source:"MemRegion.Region.load_float"
~effect:"Loc is Raw" "load_float(Raw %a)" M.pretty repr
in M.load_float sigma.Tuple.model c_float repr
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.kind region with
| R.Many (R.Float c_float') ->
if compare_c_float c_float c_float' = 0
then F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_float"
+ ~source:"MemRegion.Region.load_float"
~effect:"Type is not the same in chunk and in argument" "%a!=%a"
Ctypes.pp_float c_float Ctypes.pp_float c_float'
in F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
@@ -1701,14 +1701,14 @@ struct
then Sigma.value sigma c
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_float"
+ ~source:"MemRegion.Region.load_float"
~effect:"Type is not the same in chunk and in argument" "%a!=%a"
Ctypes.pp_float c_float Ctypes.pp_float c_float'
in Sigma.value sigma c
| R.Garbled -> M.load_float sigma.model c_float repr
| k ->
let _ =
- Warning.emit ~severe:false ~source:"MemBornat.Bornat.load_float"
+ Warning.emit ~severe:false ~source:"MemRegion.Region.load_float"
~effect:"Region's kind is not Float" "%a : %a != %a"
R.pretty region R.pp_kind k Ctypes.pp_float c_float
in assert false
@@ -1716,23 +1716,23 @@ struct
let load_pointer sigma ty loc : loc = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_float"
+ ~source:"MemRegion.Region.load_float"
~effect:"Loc is Null" "Attempt to load_float inside Null"
in let mloc = M.load_pointer sigma.Tuple.model ty M.null in
if QED.equal (M.pointer_val mloc) (M.pointer_val M.null)
then Null else Raw { repr = mloc }
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_pointer"
+ ~source:"MemRegion.Region.load_pointer"
~effect:"Loc is Raw" "load_pointer(Raw %a : *%a)"
M.pretty repr Printer.pp_typ ty
in Raw { repr = M.load_pointer sigma.Tuple.model ty repr }
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.points_to region with
| None ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_pointer"
+ ~source:"MemRegion.Region.load_pointer"
~effect:"No region pointed" "No region for *(%a in %a)"
M.pretty repr R.pretty region
in Raw { repr = M.load_pointer sigma.Tuple.model ty repr }
@@ -1745,7 +1745,7 @@ struct
| R.Garbled -> M.load_pointer sigma.Tuple.model ty repr
| k ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.load_pointer"
+ ~source:"MemRegion.Region.load_pointer"
~effect:"Kind of region is not a pointer"
"Region %a : %a != %a"
R.pretty region R.pp_kind k Printer.pp_typ ty
@@ -1760,24 +1760,24 @@ struct
let store_int sigma c_int loc v : Chunk.t * term = match loc with
| Null ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.store_int"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
~effect:"Loc is Null" "Attempt to store_int inside Null"
in let c, t = M.store_int sigma.Tuple.model c_int M.null v in
Chunk.CModel c, t
| Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.Bornat.store_int"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.Region.store_int"
~effect:"Loc is Raw" "store_int(Raw %a)" M.pretty repr
in let c, t = M.store_int sigma.Tuple.model c_int repr v in
Chunk.CModel c, t
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.kind region with
| R.Many (R.Int c_int') as k ->
if compare_c_int c_int c_int' = 0
then (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_int"
+ ~source:"MemRegion.Region.store_int"
~effect:"Int types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_int c_int
@@ -1787,7 +1787,7 @@ struct
then (c, v)
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_int"
+ ~source:"MemRegion.Region.store_int"
~effect:"Int types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_int c_int
@@ -1797,7 +1797,7 @@ struct
(Chunk.CModel c', v)
| k ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_int"
+ ~source:"MemRegion.Region.store_int"
~effect:"Int types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_int c_int
@@ -1806,25 +1806,25 @@ struct
let store_float sigma c_float loc v : Chunk.t * term = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_float"
+ ~source:"MemRegion.Region.store_float"
~effect:"Loc is Null" "Attempt to store_float inside Null"
in let c, t = M.store_float sigma.Tuple.model c_float M.null v in
Chunk.CModel c, t
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_float"
+ ~source:"MemRegion.Region.store_float"
~effect:"Loc is Raw" "store_float(Raw %a)" M.pretty repr
in let c, t = M.store_float sigma.Tuple.model c_float repr v in
Chunk.CModel c, t
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.kind region with
| R.Many (R.Float c_float') as k ->
if compare_c_float c_float c_float' = 0
then (c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v)
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_float"
+ ~source:"MemRegion.Region.store_float"
~effect:"Float types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_float c_float
@@ -1834,7 +1834,7 @@ struct
then (c, v)
else
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_float"
+ ~source:"MemRegion.Region.store_float"
~effect:"Float types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_float c_float
@@ -1844,7 +1844,7 @@ struct
(Chunk.CModel c, t)
| k ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_float"
+ ~source:"MemRegion.Region.store_float"
~effect:"Float types are not the same"
"(%a in %a : %a != %a)"
M.pretty repr R.pretty region R.pp_kind k Ctypes.pp_float c_float
@@ -1853,19 +1853,19 @@ struct
let store_pointer sigma ty loc v : Chunk.t * term = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_pointer"
+ ~source:"MemRegion.Region.store_pointer"
~effect:"Loc is Null" "Attempt to store_pointer inside Null"
in let c, t = M.store_pointer sigma.Tuple.model ty M.null v in
Chunk.CModel c, t
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_pointer"
+ ~source:"MemRegion.Region.store_pointer"
~effect:"Loc is Raw" "store_pointer(Raw %a : *%a)"
M.pretty repr Printer.pp_typ ty
in let c, t = M.store_pointer sigma.Tuple.model ty repr v in
Chunk.CModel c, t
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CVal region) in
+ let c = Chunk.CRegion (B.CVal region) in
match R.kind region with
| R.Many (R.Ptr) ->
c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v
@@ -1875,7 +1875,7 @@ struct
(Chunk.CModel c, repr)
| k ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.store_pointer"
+ ~source:"MemRegion.Region.store_pointer"
~effect:"This is not a region with pointer type"
"(%a in %a : %a != *%a)"
M.pretty repr R.pretty region R.pp_kind k Printer.pp_typ ty
@@ -1888,13 +1888,13 @@ struct
let set_init_atom sigma ty loc v = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init_atom"
+ ~source:"MemRegion.Region.set_init_atom"
~effect:"Loc is Null" "Attempt to set_init_atom with Null"
in let (c, t) = M.set_init_atom sigma.Tuple.model ty M.null v in
(Chunk.CModel c, t)
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init_atom"
+ ~source:"MemRegion.Region.set_init_atom"
~effect:"Loc is Raw" "set_init_atom(Raw %a <- %a)"
M.pretty repr QED.pretty v
in let (c, t) = M.set_init_atom sigma.Tuple.model ty repr v in
@@ -1904,25 +1904,25 @@ struct
| R.Garbled ->
let (c, t) = M.set_init_atom sigma.Tuple.model ty repr v in
(Chunk.CModel c, t)
- | R.Single _-> Chunk.CBornat (B.CInit region), v
+ | R.Single _-> Chunk.CRegion (B.CInit region), v
| R.Many _ ->
- let c = Chunk.CBornat (B.CInit region) in
+ let c = Chunk.CRegion (B.CInit region) in
c, F.e_set (Sigma.value sigma c) (M.pointer_val repr) v
let is_init_atom sigma ty loc : term = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.is_init_atom"
+ ~source:"MemRegion.Region.is_init_atom"
~effect:"Loc is Null" "is_init_atom(Null)"
in M.is_init_atom sigma.Tuple.model ty M.null
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.is_init_atom"
+ ~source:"MemRegion.Region.is_init_atom"
~effect:"Loc is Raw" "is_init_atom(Raw %a)"
M.pretty repr
in M.is_init_atom sigma.Tuple.model ty repr
| Loc { repr ; region } ->
- let c = Chunk.CBornat (B.CInit region) in
+ let c = Chunk.CRegion (B.CInit region) in
match R.kind region with
| R.Garbled -> M.is_init_atom sigma.Tuple.model ty repr
| R.Many _ -> F.e_get (Sigma.value sigma c) @@ M.pointer_val repr
@@ -1931,12 +1931,12 @@ struct
let is_init_range sigma ty loc length : pred = match loc with
| Null ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.is_init_range"
+ ~source:"MemRegion.Region.is_init_range"
~effect:"Loc is Null" "is_init_range(Null)"
in M.is_init_range sigma.Tuple.model ty M.null length
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.is_init_range"
+ ~source:"MemRegion.Region.is_init_range"
~effect:"Loc is Raw" "is_init_range(%a, ty=%a, length=%a)"
M.pretty repr Ctypes.pp_object ty QED.pretty length
in M.is_init_range sigma.Tuple.model ty repr length
@@ -1944,12 +1944,12 @@ struct
match R.kind region with
| R.Garbled -> M.is_init_range sigma.Tuple.model ty repr length
| R.Many _ ->
- let c = Chunk.CBornat (B.CInit region) in
+ let c = Chunk.CRegion (B.CInit region) in
let n = F.e_mul (M.sizeof ty) length in
F.p_call p_is_init_r [Sigma.value sigma c;M.pointer_val repr;n]
| R.Single _ as k ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.is_init_range"
+ ~source:"MemRegion.Region.is_init_range"
~effect:"Region is Single kind" "is_init_range(%a in %a : %a, ty=%a, length=%a)"
M.pretty repr R.pretty region R.pp_kind k
Ctypes.pp_object ty QED.pretty length
@@ -1959,32 +1959,32 @@ struct
let set_init ty loc ~length chunk ~current : term = match loc, chunk with
| Null, Chunk.CModel c ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
+ ~source:"MemRegion.Region.set_init"
~effect:"Loc is Null" "set_init(Null)"
in M.set_init ty M.null ~length c ~current
- | Null, Chunk.CBornat _ ->
+ | Null, Chunk.CRegion _ ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
- ~effect:"Loc is Null" "set_init(Null) and Chunk is Bornat"
+ ~source:"MemRegion.Region.set_init"
+ ~effect:"Loc is Null" "set_init(Null) and Chunk is Region"
in assert false
| Raw { repr }, Chunk.CModel c ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
+ ~source:"MemRegion.Region.set_init"
~effect:"Loc is Null" "set_init(Raw %a)"
M.pretty repr
in M.set_init ty repr ~length c ~current
- | Raw { repr }, Chunk.CBornat _ ->
+ | Raw { repr }, Chunk.CRegion _ ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
- ~effect:"Loc is Null" "set_init(Raw %a) and Chunk is Bornat"
+ ~source:"MemRegion.Region.set_init"
+ ~effect:"Loc is Null" "set_init(Raw %a) and Chunk is Region"
M.pretty repr
in assert false
| Loc { repr }, Chunk.CModel c -> M.set_init ty repr ~length c ~current
- | Loc { repr ; region }, Chunk.CBornat c ->
+ | Loc { repr ; region }, Chunk.CRegion c ->
match R.kind region, c with
| R.Garbled, ( B.CVal _ | B.CInit _| B.CGhost _) ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
+ ~source:"MemRegion.Region.set_init"
~effect:"Garbled is not associated to low memory model"
"set_init(%a in %a : Garbled)"
M.pretty repr R.pretty region
@@ -1994,7 +1994,7 @@ struct
F.e_fun f_set_init [current;M.pointer_val repr;n]
| R.Single _, _ ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.set_init"
+ ~source:"MemRegion.Region.set_init"
~effect:"Single is not supported"
"set_init(%a in %a : Single)"
M.pretty repr R.pretty region
@@ -2009,29 +2009,29 @@ struct
| Null -> Sigma.empty
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.value_footprint"
+ ~source:"MemRegion.Region.value_footprint"
~effect:"Loc is Raw"
"value_footprint(Raw %a : %a)"
M.pretty repr Ctypes.pp_object ty
- in let mdom = M.value_footprint ty repr in
- let bdom = BSigma.empty in
- Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = bdom }
+ in
+ let model = M.value_footprint ty repr in
+ Sigma.to_domain Tuple.{ model ; region = BSigma.empty }
| Loc { repr ; region } ->
match R.kind region, ty with
| R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
- let mdom = M.value_footprint ty repr in
- Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = BSigma.empty }
+ let model = M.value_footprint ty repr in
+ Sigma.to_domain Tuple.{ model ; region = BSigma.empty }
| (R.Many (R.Int _) | R.Single (R.Int _)), C_int _
| (R.Many (R.Float _) | R.Single (R.Float _)), C_float _
| (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
- Heap.Set.singleton (Chunk.CBornat (B.CVal region))
+ Heap.Set.singleton (Chunk.CRegion (B.CVal region))
| (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.value_footprint"
+ ~source:"MemRegion.Region.value_footprint"
~effect:"Type is not the same in chunk and in argument"
"value_footprint(%a : %a in %a : %a)"
M.pretty repr Ctypes.pp_object ty R.pretty region R.pp_kind k
- in Heap.Set.singleton @@ Chunk.CBornat (B.CVal region)
+ in Heap.Set.singleton @@ Chunk.CRegion (B.CVal region)
| _, C_comp { cfields } ->
let none = Heap.Set.empty in
let f_fold acc fd =
@@ -2049,29 +2049,28 @@ struct
| Null -> Sigma.empty
| Raw { repr } ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.init_footprint"
+ ~source:"MemRegion.Region.init_footprint"
~effect:"Loc is Raw"
"init_footprint(Raw %a : %a)"
M.pretty repr Ctypes.pp_object ty
- in let mdom = M.init_footprint ty repr in
- let bdom = BSigma.empty in
- Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = bdom }
+ in let model = M.init_footprint ty repr in
+ Sigma.to_domain Tuple.{ model ; region = BSigma.empty }
| Loc { repr ; region } ->
match R.kind region, ty with
| R.Garbled, (C_int _ | C_float _ | C_pointer _) ->
- let mdom = M.init_footprint ty repr in
- Sigma.to_domain { Tuple.model = mdom ; Tuple.bornat = BSigma.empty }
+ let model = M.init_footprint ty repr in
+ Sigma.to_domain Tuple.{ model ; region = BSigma.empty }
| (R.Many (R.Int _) | R.Single (R.Int _)), C_int _
| (R.Many (R.Float _) | R.Single (R.Float _)), C_float _
| (R.Many (R.Ptr ) | R.Single (R.Ptr )), C_pointer _->
- Heap.Set.singleton @@ Chunk.CBornat (B.CInit region)
+ Heap.Set.singleton @@ Chunk.CRegion (B.CInit region)
| (R.Many _ | R.Single _) as k, (C_int _ | C_float _ | C_pointer _) ->
let _ = Warning.emit ~severe:false
- ~source:"MemBornat.Bornat.init_footprint"
+ ~source:"MemRegion.Region.init_footprint"
~effect:"Type is not the same in chunk and in argument"
"init_footprint(%a : %a in %a : %a)"
M.pretty repr Ctypes.pp_object ty R.pretty region R.pp_kind k
- in Heap.Set.singleton @@ Chunk.CBornat (B.CInit region)
+ in Heap.Set.singleton @@ Chunk.CRegion (B.CInit region)
| _, C_comp { cfields } ->
let none = Heap.Set.empty in
let f_fold acc fd =
@@ -2086,16 +2085,16 @@ struct
end
- type loc = Bornat.loc
+ type loc = Region.loc
type domain = Sigma.domain
type chunk = Chunk.t
type segment = loc rloc
- (****************************************************************************)
- module LOADER = MemLoader.Make(Bornat)
- (******************************************************************************)
+ (***************************************************************************)
+ module LOADER = MemLoader.Make(Region)
+ (*****************************************************************************)
let load = LOADER.load
let load_init = LOADER.load_init
@@ -2109,7 +2108,7 @@ struct
(*
let sloc_oget = function
| Sloc None -> Sloc M.null, None
- | Sloc (Some { Bornat.repr = repr }) -> Sloc repr
+ | Sloc (Some { Region.repr = repr }) -> Sloc repr
| Sarray (None,a,b) ->
| Srange (None,_,_,_)
| Sdescr (_,None,_) ->
@@ -2117,28 +2116,28 @@ struct
*)
let assigned seq ty sloc = match sloc with
- | Sloc (Bornat.Null) | Sarray (Bornat.Null,_,_)
- | Srange (Bornat.Null,_,_,_) | Sdescr (_,Bornat.Null,_) ->
+ | Sloc (Region.Null) | Sarray (Region.Null,_,_)
+ | Srange (Region.Null,_,_,_) | Sdescr (_,Region.Null,_) ->
LOADER.assigned seq ty sloc
- | Sloc (Bornat.Raw _) | Sarray (Bornat.Raw _,_,_)
- | Srange (Bornat.Raw _,_,_,_) | Sdescr (_,Bornat.Raw _,_) ->
+ | Sloc (Region.Raw _) | Sarray (Region.Raw _,_,_)
+ | Srange (Region.Raw _,_,_,_) | Sdescr (_,Region.Raw _,_) ->
LOADER.assigned seq ty sloc
| _ ->
(* Maintain always initialized values initialized *)
let region = match sloc with
- | Sloc (Bornat.Loc loc) | Sarray (Bornat.Loc loc, _, _)
- | Srange (Bornat.Loc loc, _, _, _)
- | Sdescr (_, Bornat.Loc loc, _) -> loc.region
- | Sloc (Bornat.Null|Bornat.Raw _)
- | Sarray ((Bornat.Null|Bornat.Raw _),_,_)
- | Srange ((Bornat.Null|Bornat.Raw _),_,_,_)
- | Sdescr (_,(Bornat.Null|Bornat.Raw _),_) -> assert false
+ | Sloc (Region.Loc loc) | Sarray (Region.Loc loc, _, _)
+ | Srange (Region.Loc loc, _, _, _)
+ | Sdescr (_, Region.Loc loc, _) -> loc.region
+ | Sloc (Region.Null|Region.Raw _)
+ | Sarray ((Region.Null|Region.Raw _),_,_)
+ | Srange ((Region.Null|Region.Raw _),_,_,_)
+ | Sdescr (_,(Region.Null|Region.Raw _),_) -> assert false
in
Assert (MemMemory.cinits
- @@ Sigma.value seq.post @@ Chunk.CBornat (B.CInit region)) ::
+ @@ Sigma.value seq.post @@ Chunk.CRegion (B.CInit region)) ::
LOADER.assigned seq ty sloc
- (** {2 Reversing the Model} *)
+ (* {2 Reversing the Model} *)
type state = M.state
@@ -2153,257 +2152,258 @@ struct
let iter = M.iter
let pretty fmt = function
- | Bornat.Null -> Format.fprintf fmt "NULL"
- | Bornat.Raw { repr } -> Format.fprintf fmt "{ Raw %a }" M.pretty repr
- | Bornat.Loc { repr ; region } ->
+ | Region.Null -> Format.fprintf fmt "NULL"
+ | Region.Raw { repr } -> Format.fprintf fmt "{ Raw %a }" M.pretty repr
+ | Region.Loc { repr ; region } ->
Format.fprintf fmt "{ %a in %a }"
M.pretty repr R.pretty region
- (** {2 Memory Model API} *)
+ (* {2 Memory Model API} *)
let vars = function
- | Bornat.Null -> Vars.empty
- | Bornat.Raw { repr } | Bornat.Loc { repr } -> M.vars repr
- (** Return the logic variables from which the given location depend on. *)
+ | Region.Null -> Vars.empty
+ | Region.Raw { repr } | Region.Loc { repr } -> M.vars repr
+ (* Return the logic variables from which the given location depend on. *)
let occurs var = function
- | Bornat.Null -> false
- | Bornat.Raw {repr } | Bornat.Loc { repr } -> M.occurs var repr
- (** Test if a location depend on a given logic variable *)
+ | Region.Null -> false
+ | Region.Raw {repr } | Region.Loc { repr } -> M.occurs var repr
+ (* Test if a location depend on a given logic variable *)
- let null = Bornat.Null
- (** Return the location of the null pointer *)
+ let null = Region.Null
+ (* Return the location of the null pointer *)
let literal ~eid:eid name =
let repr = M.literal ~eid name in
match R.literal ~eid name with
- | None -> Bornat.Raw { repr }
- | Some region -> Bornat.Loc { repr ; region }
- (** Return the memory location of a constant string,
+ | None -> Region.Raw { repr }
+ | Some region -> Region.Loc { repr ; region }
+ (* Return the memory location of a constant string,
the id is a unique identifier. *)
let cvar var =
match R.cvar var with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.cvar"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.cvar"
~effect:"No region for this var" "%a"
Printer.pp_varinfo var
- in Bornat.Raw { repr = M.cvar var }
- | Some region -> Bornat.Loc { repr = M.cvar var ; region }
- (** Return the location of a C variable. *)
+ in Region.Raw { repr = M.cvar var }
+ | Some region -> Region.Loc { repr = M.cvar var ; region }
+ (* Return the location of a C variable. *)
let pointer_loc term =
if QED.equal term @@ M.pointer_val M.null
- then Bornat.Null
+ then Region.Null
else let repr = M.pointer_loc term in
match R.pointer_loc () with
- | None -> Bornat.Raw { repr }
- | Some region -> Bornat.Loc { repr ; region }
- (** Interpret an address value (a pointer) as an abstract location.
+ | None -> Region.Raw { repr }
+ | Some region -> Region.Loc { repr ; region }
+ (* Interpret an address value (a pointer) as an abstract location.
Might fail on memory models not supporting pointers. *)
let pointer_val = function
- | Bornat.Null -> M.pointer_val M.null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.pointer_val"
+ | Region.Null -> M.pointer_val M.null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.pointer_val"
~effect:"No region for this loc" "%a" M.pretty repr
in M.pointer_val repr
- | Bornat.Loc { repr } -> M.pointer_val repr
- (** Return the adress value (a pointer) of an abstract location.
+ | Region.Loc { repr } -> M.pointer_val repr
+ (* Return the adress value (a pointer) of an abstract location.
Might fail on memory models not capable of representing pointers. *)
let field loc fieldinfo = match loc with
- | Bornat.Null ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.field"
+ | Region.Null ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
~effect:"Loc is NULL"
"NULL.(%a)" Printer.pp_field fieldinfo
- in Bornat.Null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.field"
+ in Region.Null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
~effect:"Loc is Raw"
"(%a).(%a)" M.pretty repr Printer.pp_field fieldinfo
- in Bornat.Raw { repr = M.field repr fieldinfo }
- | Bornat.Loc { repr ; region } ->
+ in Region.Raw { repr = M.field repr fieldinfo }
+ | Region.Loc { repr ; region } ->
match R.field region fieldinfo with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.field"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.field"
~effect:"No region for this field"
"(%a in %a).(%a in no region)"
M.pretty repr R.pretty region Printer.pp_field fieldinfo
- in Bornat.Raw { repr = M.field repr fieldinfo }
- | Some region -> Bornat.Loc { repr = M.field repr fieldinfo ; region }
- (** Return the memory location obtained by field access from a given
+ in Region.Raw { repr = M.field repr fieldinfo }
+ | Some region -> Region.Loc { repr = M.field repr fieldinfo ; region }
+ (* Return the memory location obtained by field access from a given
memory location. *)
let shift loc ty term = match loc with
- | Bornat.Null ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.shift"
+ | Region.Null ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
~effect:"Loc is NULL"
"NULL.[%a : %a]" QED.pretty term Ctypes.pp_object ty
- in Bornat.Null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.shift"
+ in Region.Null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
~effect:"Loc is Raw"
"(%a).[%a : %a]"
M.pretty repr QED.pretty term Ctypes.pp_object ty
- in Bornat.Raw { repr = M.shift repr ty term }
- | Bornat.Loc { repr ; region } ->
+ in Region.Raw { repr = M.shift repr ty term }
+ | Region.Loc { repr ; region } ->
match R.shift region ty term with
| None ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.shift"
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.shift"
~effect:"Loc is Raw"
"(%a in %a).[%a : %a] in no region"
M.pretty repr R.pretty region QED.pretty term Ctypes.pp_object ty
- in Bornat.Raw { repr = M.shift repr ty term }
- | Some region -> Bornat.Loc { repr = M.shift repr ty term ; region }
- (** Return the memory location obtained by array access at an index
+ in Region.Raw { repr = M.shift repr ty term }
+ | Some region -> Region.Loc { repr = M.shift repr ty term ; region }
+ (* Return the memory location obtained by array access at an index
represented by the given {!term}. The element of the array are of
the given {!c_object} type. *)
let base_addr = function
- | Bornat.Null -> Bornat.Null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.base_addr"
+ | Region.Null -> Region.Null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.base_addr"
~effect:"Loc is Raw" "base_addr(%a)" M.pretty repr
- in Bornat.Raw { repr = M.base_addr repr }
- | Bornat.Loc { repr ; region } ->
- Bornat.Loc { repr = M.base_addr repr ; region = R.base_addr region }
- (** Return the memory location of the base address of a given memory
+ in Region.Raw { repr = M.base_addr repr }
+ | Region.Loc { repr ; region } ->
+ Region.Loc { repr = M.base_addr repr ; region = R.base_addr region }
+ (* Return the memory location of the base address of a given memory
location. *)
let base_offset = function
- | Bornat.Null -> M.base_offset M.null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.base_offset"
+ | Region.Null -> M.base_offset M.null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.base_offset"
~effect:"Loc is Raw" "base_offset(%a)" M.pretty repr
in M.base_offset repr
- | Bornat.Loc { repr } -> M.base_offset repr
- (** Return the offset of the location, in bytes, from its base_addr. *)
+ | Region.Loc { repr } -> M.base_offset repr
+ (* Return the offset of the location, in bytes, from its base_addr. *)
let block_length sigma ty = function
- | Bornat.Null -> M.block_length sigma.Tuple.model ty M.null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.block_length"
+ | Region.Null -> M.block_length sigma.Tuple.model ty M.null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.block_length"
~effect:"Loc is Raw" "block_length(%a)" M.pretty repr
in M.block_length sigma.Tuple.model ty repr
- | Bornat.Loc { repr } -> M.block_length sigma.Tuple.model ty repr
- (** Returns the length (in bytes) of the allocated block containing
+ | Region.Loc { repr } -> M.block_length sigma.Tuple.model ty repr
+ (* Returns the length (in bytes) of the allocated block containing
the given location. *)
let cast objs = function
- | Bornat.Null -> Bornat.Null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.cast"
+ | Region.Null -> Region.Null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.cast"
~effect:"Loc is NULL" "NULL=%a" M.pretty repr
- in Bornat.Raw { repr = M.cast objs repr }
- | Bornat.Loc loc -> Bornat.Loc { loc with repr = M.cast objs loc.repr }
- (** Cast a memory location into another memory location.
+ in Region.Raw { repr = M.cast objs repr }
+ | Region.Loc loc -> Region.Loc { loc with repr = M.cast objs loc.repr }
+ (* Cast a memory location into another memory location.
For [cast ty loc] the cast is done from [ty.pre] to [ty.post].
Might fail on memory models not supporting pointer casts. *)
let loc_of_int ty term =
if QED.equal term @@ M.pointer_val M.null
- then Bornat.Null
+ then Region.Null
else match R.loc_of_int () with
- | None -> Bornat.Raw { repr = M.loc_of_int ty term }
- | Some region -> Bornat.Loc { repr = M.loc_of_int ty term ; region }
+ | None -> Region.Raw { repr = M.loc_of_int ty term }
+ | Some region -> Region.Loc { repr = M.loc_of_int ty term ; region }
let int_of_loc c_int = function
- | Bornat.Null -> M.int_of_loc c_int M.null
- | Bornat.Raw { repr } ->
- let _ = Warning.emit ~severe:false ~source:"MemBornat.int_of_loc"
+ | Region.Null -> M.int_of_loc c_int M.null
+ | Region.Raw { repr } ->
+ let _ = Warning.emit ~severe:false ~source:"MemRegion.int_of_loc"
~effect:"Loc is Raw" "NULL=%a" M.pretty repr
in M.int_of_loc c_int repr
- | Bornat.Loc { repr } -> M.int_of_loc c_int repr
- (** Cast a memory location into its absolute memory address,
+ | Region.Loc { repr } -> M.int_of_loc c_int repr
+ (* Cast a memory location into its absolute memory address,
given as an integer with the given C-type. *)
let is_null = function
- | Bornat.Null -> p_true
- | Bornat.Raw { repr } | Bornat.Loc { repr } -> M.is_null repr
- (** Return the formula that check if a given location is null *)
+ | Region.Null -> p_true
+ | Region.Raw { repr } | Region.Loc { repr } -> M.is_null repr
+ (* Return the formula that check if a given location is null *)
let get_repr = function
- | Bornat.Null -> M.null
- | Bornat.Raw { repr } -> repr
- | Bornat.Loc { repr } -> repr
+ | Region.Null -> M.null
+ | Region.Raw { repr } -> repr
+ | Region.Loc { repr } -> repr
let loc_eq loc_a loc_b = M.loc_eq (get_repr loc_a) (get_repr loc_b)
let loc_lt loc_a loc_b = M.loc_lt (get_repr loc_a) (get_repr loc_b)
let loc_neq loc_a loc_b = M.loc_neq (get_repr loc_a) (get_repr loc_b)
let loc_leq loc_a loc_b = M.loc_leq (get_repr loc_a) (get_repr loc_b)
- (** Memory location comparisons *)
+ (* Memory location comparisons *)
let loc_diff ty loc_a loc_b = M.loc_diff ty (get_repr loc_a) (get_repr loc_b)
- (** Compute the length in bytes between two memory locations *)
+ (* Compute the length in bytes between two memory locations *)
let get_rloc = function
- | Rloc (ty, Bornat.Null) -> Rloc (ty, M.null)
- | Rloc (ty, Bornat.Raw { repr }) -> Rloc (ty, repr)
- | Rloc (ty, Bornat.Loc loc) ->
+ | Rloc (ty, Region.Null) -> Rloc (ty, M.null)
+ | Rloc (ty, Region.Raw { repr }) -> Rloc (ty, repr)
+ | Rloc (ty, Region.Loc loc) ->
Rloc (ty, loc.repr)
- | Rrange (Bornat.Null, ty, inf, sup) ->
+ | Rrange (Region.Null, ty, inf, sup) ->
Rrange (M.null, ty, inf, sup)
- | Rrange (Bornat.Raw { repr }, ty, inf, sup) ->
+ | Rrange (Region.Raw { repr }, ty, inf, sup) ->
Rrange (repr, ty, inf, sup)
- | Rrange (Bornat.Loc loc, ty, inf, sup) ->
+ | Rrange (Region.Loc loc, ty, inf, sup) ->
Rrange (loc.repr, ty, inf, sup)
let get_rloc_region = function
| Rloc (ty, loc) ->
- Rloc (ty, (match loc with Bornat.Null -> M.null
- | Bornat.Raw { repr } | Bornat.Loc { repr } -> repr)),
- (match loc with Bornat.Null | Bornat.Raw _ -> None
- | Bornat.Loc { region } -> Some region)
+ Rloc (ty, (match loc with Region.Null -> M.null
+ | Region.Raw { repr } | Region.Loc { repr } -> repr)),
+ (match loc with Region.Null | Region.Raw _ -> None
+ | Region.Loc { region } -> Some region)
| Rrange (loc, ty, inf, sup) ->
- Rrange ((match loc with Bornat.Null -> M.null
- | Bornat.Raw { repr } | Bornat.Loc { repr } -> repr), ty, inf, sup),
- (match loc with Bornat.Null | Bornat.Raw _ -> None
- | Bornat.Loc { region } -> Some region)
+ Rrange ((match loc with Region.Null -> M.null
+ | Region.Raw { repr } | Region.Loc { repr } -> repr), ty, inf, sup),
+ (match loc with Region.Null | Region.Raw _ -> None
+ | Region.Loc { region } -> Some region)
let valid sigma acs (rloc : loc rloc) =
M.valid sigma.Tuple.model acs @@ get_rloc rloc
- (** Return the formula that tests if a memory state is valid
+ (* Return the formula that tests if a memory state is valid
(according to {!acs}) in the given memory state at the given
segment.
*)
let frame sigma =
- let bornat_frame sigma = function
+ let region_frame sigma = function
| B.CInit region ->
- MemMemory.cinits @@ Sigma.value sigma @@ Chunk.CBornat (B.CInit region)
+ MemMemory.cinits @@ Sigma.value sigma @@ Chunk.CRegion (B.CInit region)
| B.CVal region | B.CGhost region -> match R.kind region with
| R.Many R.Ptr | R.Single R.Ptr ->
- MemMemory.framed @@ Sigma.value sigma @@ Chunk.CBornat (B.CVal region)
+ MemMemory.framed @@ Sigma.value sigma @@ Chunk.CRegion (B.CVal region)
| R.Garbled | R.Many (R.Int _ | R.Float _)
| R.Single (R.Int _ | R.Float _) -> p_true
in
- BSigma.Chunk.Set.fold (fun c l -> bornat_frame sigma c :: l)
- (BSigma.domain sigma.Tuple.bornat)
- @@ M.frame sigma.Tuple.model
- (** Assert the memory is a proper heap state preceeding the function
+ BSigma.Chunk.Set.fold
+ (fun c l -> region_frame sigma c :: l)
+ (BSigma.domain sigma.region)
+ @@ M.frame sigma.model
+ (* Assert the memory is a proper heap state preceeding the function
entry point. *)
- let alloc sigma vars =
+ let alloc (sigma:sigma) vars =
if vars = [] then sigma
- else { sigma with Tuple.model = M.alloc sigma.Tuple.model vars }
- (** Allocates new chunk for the validity of variables. *)
+ else { sigma with model = M.alloc sigma.model vars }
+ (* Allocates new chunk for the validity of variables. *)
- let invalid sigma rloc = M.invalid sigma.Tuple.model (get_rloc rloc)
- (** Returns the formula that tests if the entire memory is invalid
+ let invalid (sigma:sigma) rloc = M.invalid sigma.model (get_rloc rloc)
+ (* Returns the formula that tests if the entire memory is invalid
for write access. *)
- let scope sigma scope vars =
- let m_sigma = { pre = sigma.pre.Tuple.model ; post = sigma.post.Tuple.model } in
+ let scope (s:sigma sequence) scope vars =
+ let m_sigma = { pre = s.pre.model ; post = s.post.model } in
M.scope m_sigma scope vars
- (** Manage the scope of variables. Returns the updated memory model
+ (* Manage the scope of variables. Returns the updated memory model
and hypotheses modeling the new validity-scope of the variables. *)
- let global sigma p = M.global sigma.Tuple.model p
- (** Given a pointer value [p], assumes this pointer [p] (when valid)
+ let global (sigma:sigma) p = M.global sigma.model p
+ (* Given a pointer value [p], assumes this pointer [p] (when valid)
is allocated outside the function frame under analysis. This means
separated from the formals and locals of the function. *)
@@ -2427,9 +2427,9 @@ struct
else M.separated rl1 rl2
let chunk_is_well_formed sigma chunk = match chunk with
- | Chunk.CModel _ | Chunk.CBornat (B.CInit _)
- | Chunk.CBornat (B.CGhost _) -> p_true
- | Chunk.CBornat (B.CVal region) -> match R.kind region with
+ | Chunk.CModel _ | Chunk.CRegion (B.CInit _)
+ | Chunk.CRegion (B.CGhost _) -> p_true
+ | Chunk.CRegion (B.CVal region) -> match R.kind region with
| R.Garbled -> p_true
| R.Many (R.Float _ | R.Ptr )
| R.Single (R.Float _ | R.Ptr ) -> p_true
diff --git a/src/plugins/wp/MemBornat.mli b/src/plugins/wp/MemRegion.mli
similarity index 97%
rename from src/plugins/wp/MemBornat.mli
rename to src/plugins/wp/MemRegion.mli
index 828341de2e6a98d6306c5a88653a37af9b58cecb..34dcd4a10daa131bb0c6af052da081099751c3ad 100644
--- a/src/plugins/wp/MemBornat.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -26,7 +26,7 @@ open Lang.F
open Sigs
(* -------------------------------------------------------------------------- *)
-(* --- Bornat Memory Model --- *)
+(* --- Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
module type ModelLoader = sig
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 7028c992e2b8c3a2401926eeaf6929f57c518ee1..25811dce3fc478144c33d4794a0d463e973dd9e6 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -26,7 +26,7 @@ open Lang.F
(* -------------------------------------------------------------------------- *)
-(* --- Region Analysis API for Bornat Memory Model --- *)
+(* --- Region Analysis API for Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
module type API = sig
@@ -65,7 +65,7 @@ end
(* -------------------------------------------------------------------------- *)
-(* --- Region Analysis for Bornat Memory Model --- *)
+(* --- Region Analysis for Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
module R (*: API*) =
diff --git a/src/plugins/wp/RegionAnalysis.mli b/src/plugins/wp/RegionAnalysis.mli
index 057c8124af295824a965825e5581f3bd524a2bbd..a50d0bc4bd80ea41a1842793c22684b38c324593 100644
--- a/src/plugins/wp/RegionAnalysis.mli
+++ b/src/plugins/wp/RegionAnalysis.mli
@@ -25,7 +25,7 @@ open Ctypes
open Lang.F
(* -------------------------------------------------------------------------- *)
-(* --- Region Analysis API for Bornat Memory Model --- *)
+(* --- Region Analysis API for Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
module type API = sig
diff --git a/src/plugins/wp/gui/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml
index 50025d407fd771cfa98469c2e56a71f1b4514890..1a5432b15c19d0cbe023205cccc5c35f2b751f2b 100644
--- a/src/plugins/wp/gui/GuiPanel.ml
+++ b/src/plugins/wp/gui/GuiPanel.ml
@@ -99,7 +99,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | EVA | BYTES | BORNAT
+type memory = TREE | HOARE | TYPED | EVA | BYTES | Region
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -152,7 +152,7 @@ class model_selector (main : Design.main_window_extension_points) =
| Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
| Eva -> memory#set EVA
| Bytes -> memory#set BYTES
- | Bornat -> memory#set BORNAT
+ | Region -> memory#set Region
) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
@@ -168,7 +168,7 @@ class model_selector (main : Design.main_window_extension_points) =
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
| EVA -> Eva
| BYTES -> Bytes
- | BORNAT -> Bornat
+ | Region -> Region
in {
mheap = m ;
mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;