From 38d46cea4a685b762d93ed837b67fd6c2927f439 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 12 Oct 2021 16:06:51 +0200
Subject: [PATCH] [wp] Typing predicates are coloring predicates
---
src/plugins/wp/Cint.ml | 3 ++-
src/plugins/wp/Cvalues.ml | 4 ++--
src/plugins/wp/LogicCompiler.ml | 2 +-
src/plugins/wp/MemMemory.ml | 10 +++++-----
src/plugins/wp/MemTyped.ml | 2 +-
5 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 3ec3b7227a1..dbf2df8ce7a 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -59,7 +59,8 @@ let library = "cint"
let make_fun_int op i =
Lang.extern_f ~library ~result:Logic.Int "%s_%a" op Ctypes.pp_int i
let make_pred_int op i =
- Lang.extern_f ~library ~result:Logic.Prop "%s_%a" op Ctypes.pp_int i
+ Lang.extern_f
+ ~library ~result:Logic.Prop ~coloring:true "%s_%a" op Ctypes.pp_int i
(* let fun_int op = Ctypes.imemo (make_fun_int op) *) (* unused for now *)
(* let pred_int op = Ctypes.imemo (make_pred_int op) *) (* unused for now *)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index d26aee33e7d..207ac81a387 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -241,7 +241,7 @@ struct
and is_record c s =
Definitions.call_pred
- (Lang.generated_p (C.prefix ^ Lang.comp_id c))
+ (Lang.generated_p ~coloring:true (C.prefix ^ Lang.comp_id c))
(fun lfun ->
let basename = if c.cstruct then "S" else "U" in
let s = Lang.freshvar ~basename (Lang.t_comp c) in
@@ -261,7 +261,7 @@ struct
and is_array elt ds t =
Definitions.call_pred
- (Lang.generated_p (array_name elt ds))
+ (Lang.generated_p ~coloring:true (array_name elt ds))
(fun lfun ->
let cluster =
match elt with
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 238250786e7..81aa77b29c4 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -759,7 +759,7 @@ struct
let frame = logic_frame lt_name [] in
in_frame frame
begin fun () ->
- let lfun = Lang.generated_p ("is_" ^ lt_name) in
+ let lfun = Lang.generated_p ~coloring:true ("is_" ^ lt_name) in
let tau_lt = Lang.tau_of_ltype (Ltype(lt, [])) in
Typedefs.update lt (Some lfun) ;
let term_constraint ltyp =
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index cc27b7e46b1..2a1f2ec14ab 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -80,15 +80,15 @@ let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
let p_eqmem = Lang.extern_fp ~library "eqmem"
let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
-let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
-let p_linked = Lang.extern_fp ~library "linked" (* allocation-table -> prop *)
-let p_sconst = Lang.extern_fp ~library "sconst" (* int-memory -> prop *)
+let f_region = Lang.extern_f ~coloring:true ~library ~result:L.Int "region" (* base -> region *)
+let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
+let p_linked = Lang.extern_fp ~coloring:true ~library "linked" (* allocation-table -> prop *)
+let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
let f_set_init =
Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
-let p_cinits = Lang.extern_fp ~library "cinits" (* initializaton-table -> prop *)
+let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits" (* initializaton-table -> prop *)
let p_is_init_r = Lang.extern_fp ~library "is_init_range"
let p_monotonic = Lang.extern_fp ~library "monotonic_init"
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0eee23062cc..f79ee802cf5 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -987,7 +987,7 @@ module ChunkContent = WpContext.Generator(Chunk)
let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
let m = e_var p in
let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
- let lfun = Lang.generated_p name in
+ let lfun = Lang.generated_p ~coloring:true name in
let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
let is_int = Cint.range k in
let def = p_forall [l] (is_int (F.e_get m (e_var l))) in
--
GitLab