From 45c4a1f9dfd39b7aa6f558437c9cf7877ef47564 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 5 Jul 2024 12:15:10 +0200 Subject: [PATCH] [wp] cleanup vset.mlw --- src/plugins/wp/Vset.ml | 2 +- src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 19 +++++++------------ 2 files changed, 8 insertions(+), 13 deletions(-) diff --git a/src/plugins/wp/Vset.ml b/src/plugins/wp/Vset.ml index a5b1b571e3d..87bb24efac6 100644 --- a/src/plugins/wp/Vset.ml +++ b/src/plugins/wp/Vset.ml @@ -110,7 +110,7 @@ let typecheck_singleton (params:tau option list) : tau = let typecheck_range (_:tau option list) : tau = tau_of_set Logic.Int -let p_member = Lang.extern_p ~library ~bool:"member_bool" ~prop:"mem" () +let p_member = Lang.extern_p ~library ~bool:"memb" ~prop:"mem" () let f_empty = Lang.extern_f ~library "empty" let f_union = Lang.extern_f ~library ~typecheck:typecheck_binop "union" let f_inter = Lang.extern_f ~library ~typecheck:typecheck_binop "inter" diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw index 88ec3a1db1a..db63c2110a2 100644 --- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw +++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw @@ -21,32 +21,27 @@ (**************************************************************************) (* -------------------------------------------------------------------------- *) -(* --- Sets for Why-3 --- *) +(* --- Additional Sets Symbols for WP --- *) (* -------------------------------------------------------------------------- *) theory Vset - use bool.Bool use int.Int - use map.Map + use map.Const use export set.Set - (* -------------------------------------------------------------------------- *) - (* --- Classical Sets for Alt-Ergo --- *) - (* -------------------------------------------------------------------------- *) - - function member_bool (x:'a) (s:set 'a) : bool = s x + function memb (x:'a) (s:set 'a) : bool = s x let function range (inf sup:int) : set int (* [a..b] *) = - fun elt -> if inf <= elt <= sup then true else false + fun elt -> inf <= elt <= sup function range_sup (sup:int) : set int (* [a..] *) = - fun elt -> if elt <= sup then true else false + fun elt -> elt <= sup function range_inf (inf:int) : set int (* [..b] *) = - fun elt -> if inf <= elt then true else false + fun elt -> inf <= elt - function range_all : set int (* [..] *) = fun _ -> true + function range_all : set int (* [..] *) = const true (* -------------------------------------------------------------------------- *) -- GitLab