From f84688455cc29bc2c9158c326b8039c362a48285 Mon Sep 17 00:00:00 2001
From: Bouillaguet Quentin <quentin.bouillaguet@cea.fr>
Date: Thu, 24 Jan 2019 16:58:39 +0100
Subject: [PATCH] [Wp/Model] IA binder
---
src/plugins/wp/MemEmpty.ml | 2 ++
src/plugins/wp/MemTyped.ml | 2 ++
src/plugins/wp/MemVar.ml | 2 ++
src/plugins/wp/MemZeroAlias.ml | 2 ++
src/plugins/wp/Sigs.ml | 8 ++++++++
5 files changed, 16 insertions(+)
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index a9999cc1990..cf7d3dc1740 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -35,6 +35,8 @@ let configure () =
Context.set Lang.pointer (fun _typ -> Logic.Int) ;
Context.set Cvalues.null (p_equal e_zero) ;
end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
let hypotheses () = []
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 4fbf8ef305e..1f21bfb47d4 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -391,6 +391,8 @@ let configure () =
Context.set Lang.pointer (fun _ -> t_addr) ;
Context.set Cvalues.null (p_equal a_null) ;
end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
type pointer = NoCast | Fits | Unsafe
let pointer = Context.create "MemTyped.pointer"
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index cd5dcfd28d4..b4d8a304b5e 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -49,6 +49,8 @@ struct
let datatype = "MemVar." ^ V.datatype ^ M.datatype
let configure = M.configure
+ let no_binder = { bind = fun _ f v -> f v }
+ let configure_ia _ = no_binder
let hypotheses () = V.hypotheses () @ M.hypotheses ()
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 1983f2361f4..c88f4531a43 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -39,6 +39,8 @@ let configure () =
Context.set Lang.pointer (fun _typ -> Logic.Int) ;
Context.set Cvalues.null F.(p_equal e_zero) ;
end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
(* TODO: compute actual separation hypotheses *)
let hypotheses () = []
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index aa49e4f9d21..d451e04f15f 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -27,6 +27,7 @@
open Cil_types
open Ctypes
open Lang.F
+open Interpreted_automata
(* -------------------------------------------------------------------------- *)
(** {1 General Definitions} *)
@@ -34,6 +35,8 @@ open Lang.F
type 'a sequence = { pre : 'a ; post : 'a }
+type 'a binder = { bind: 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c }
+
(** Oriented equality or arbitrary relation *)
type equation =
| Set of term * term (** [Set(a,b)] is [a := b]. *)
@@ -267,6 +270,11 @@ sig
(** Initializers to be run before using the model.
Typically sets {!Context} values. *)
+ val configure_ia: automaton -> vertex binder
+ (** Given an automaton, return a vertex's binder.
+ Currently used by the automata compiler to bind current vertex.
+ See {!StmtSemantics}. *)
+
val datatype : string
(** For projectification. Must be unique among models. *)
--
GitLab