diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 8cd2d6366bb5baa79e2c7c6919e4fb2dc60d3ad9..de29014d0865e23b357e3572cea4879c96b58ce0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1184,21 +1184,6 @@ let prover_task env prover task =
let prover_config = Why3.Whyconf.get_prover_config config prover in
let drv = Why3.Driver.load_driver_for_prover (Why3.Whyconf.get_main config)
env prover_config in
- let remove_for_prover =
- if prover.prover_name = "Alt-Ergo"
- then Filter_axioms.remove_for_altergo
- else Filter_axioms.remove_for_why3
- in
- let trans = Why3.Trans.seq [
- remove_for_prover;
- Filter_axioms.trans;
- Filter_axioms.def_into_axiom
- ] in
- let task =
- if prover.prover_name = "Coq"
- then task
- else Why3.Trans.apply trans task
- in
drv , prover_config , Why3.Driver.prepare_task drv task
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/filter_axioms.ml b/src/plugins/wp/filter_axioms.ml
deleted file mode 100644
index e63c6508b923a8617ca6637b9542e1f350eb714c..0000000000000000000000000000000000000000
--- a/src/plugins/wp/filter_axioms.ml
+++ /dev/null
@@ -1,176 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Why3
-open Term
-open Decl
-
-let meta_remove_altergo =
- Theory.register_meta "remove_for_altergo"
- [Theory.MTprsymbol]
- ~desc:"Don't@ translate@ this@ lemma@ for@ altergo."
-
-let meta_remove_why3 =
- Theory.register_meta "remove_for_why3"
- [Theory.MTprsymbol]
- ~desc:"Don't@ translate@ this@ lemma@ for@ why3."
-
-let meta_remove_ =
- Theory.register_meta "remove_for_"
- [Theory.MTprsymbol]
- ~desc:"Don't@ translate@ this@ lemma@ for@ why3 and altergo."
-
-
-let elim_abstract remove_pr d = match d.d_node with
- | Dprop (Paxiom,pr,_) when Spr.mem pr remove_pr -> []
- | Dprop (Paxiom,_,_) -> [d]
- | _ -> [d]
-
-let remove_prop meta =
- Trans.on_tagged_pr meta
- (fun remove_pr ->
- Trans.on_tagged_pr meta_remove_
- (fun remove_pr2 ->
- Trans.decl (elim_abstract (Spr.union remove_pr remove_pr2)) None))
-
-let remove_for_altergo = remove_prop meta_remove_altergo
-let remove_for_why3 = remove_prop meta_remove_why3
-
-
-let () =
- Trans.register_transform "remove_for_altergo"
- remove_for_altergo
- ~desc:"Remove@ tagged@ proposition@ with \"remove_for_altergo\"@ and \
- \"remove_for_\"@ metas."
-
-let () =
- Trans.register_transform "remove_for_why3"
- remove_for_why3
- ~desc:"Remove@ tagged@ proposition@ with \"remove_for_why3\"@ and \
- \"remove_for_\" metas."
-
-
-(** inlining *)
-
-let meta_inline_in =
- Theory.register_meta "inline_in"
- [Theory.MTlsymbol;Theory.MTprsymbol;]
- ~desc:"Inline@ the@ symbol@ in@ the@ proposition."
-
-let t_unfold defs fs tl ty =
- match Mls.find_opt fs defs with
- | None ->
- assert false (* absurd: it is in mpr so it is in sls so added in defs *)
- | Some (vl,e) ->
- let add (mt,mv) x y = Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
- let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl tl in
- let mt = Ty.oty_match mt e.t_ty ty in
- t_ty_subst mt mv e
-
-(* inline every symbol *)
-
-let rec t_replace_all defs s t =
- let t = t_map (t_replace_all defs s) t in
- match t.t_node with
- | Tapp (fs,tl) when Sls.mem fs s ->
- t_attr_copy t (t_unfold defs fs tl t.t_ty)
- | _ -> t
-
-let fold mpr sls d (defs, task) =
- (* replace *)
- let d = match d.d_node with
- | Dprop (k,pr,f) ->
- let s = Mpr.find_def Sls.empty pr mpr in
- if Sls.is_empty s then d
- else create_prop_decl k pr (t_replace_all defs s f)
- | _ -> d
- in
- (* add to defs if needed *)
- match d.d_node with
- | Dlogic [ls,ld] when Sls.mem ls sls ->
- let vl,e = open_ls_defn ld in
- Mls.add ls (vl,e) defs, Task.add_decl task d
- | _ ->
- defs, Task.add_decl task d
-
-let fold mpr sls task_hd (defs, task) =
- match task_hd.Task.task_decl.Theory.td_node with
- | Theory.Decl d ->
- fold mpr sls d (defs, task)
- | _ ->
- defs, Task.add_tdecl task task_hd.Task.task_decl
-
-let trans =
- let add (mpr,sls) = function
- | [Theory.MAls ls; Theory.MApr pr] ->
- Mpr.change (function None -> Some (Sls.singleton ls)
- | Some s -> Some (Sls.add ls s)) pr mpr,
- Sls.add ls sls
- | _ -> assert false
- in
- Trans.on_meta meta_inline_in (fun l ->
- let mpr, sls = List.fold_left add (Mpr.empty,Sls.empty) l in
- Trans.fold_map (fold mpr sls) Mls.empty None)
-
-
-let () =
- Trans.register_transform "inline_in"
- trans
- ~desc:"Inline@ the@ symbol@ in@ the@ proposition(meta@ of@ the@ same@ name)"
-
-(*** eliminate function *)
-let meta_def_into_axiom =
- Theory.register_meta "def_into_axiom"
- [Theory.MTlsymbol]
- ~desc:"Turn the marked function into an axiom"
-
-let add_ld which (ls,ld) (abst,defn,axl) =
- if which ls then
- let vl,e = open_ls_defn ld in
- let nm = ls.ls_name.Ident.id_string ^ "_def" in
- let pr = create_prsymbol (Ident.id_derive nm ls.ls_name) in
- let hd = t_app ls (List.map t_var vl) e.t_ty in
- let e = TermTF.t_selecti Term.t_equ_simp Term.t_iff_simp hd e in
- let ax = t_forall_close vl [[hd]] e in
- let ax = create_prop_decl Paxiom pr ax in
- let ld = create_param_decl ls in
- ld :: abst, defn, ax :: axl
- else
- abst, (ls,ld) :: defn, axl
-
-let elim_decl which l =
- let abst,defn,axl = List.fold_right (add_ld which) l ([],[],[]) in
- let defn = if defn = [] then [] else [create_logic_decl defn] in
- abst @ defn @ axl
-
-let elim which d = match d.d_node with
- | Dlogic l -> elim_decl which l
- | _ -> [d]
-
-let def_into_axiom =
- Trans.on_tagged_ls meta_def_into_axiom (fun sls ->
- Trans.decl (elim (fun ls -> Term.Sls.mem ls sls)) None)
-
-let () =
- Trans.register_transform "def_into_axiom"
- def_into_axiom
- ~desc:"Turn the marked function into an axiom"
diff --git a/src/plugins/wp/filter_axioms.mli b/src/plugins/wp/filter_axioms.mli
deleted file mode 100644
index e5f86a99e8a46871c1258b028cdc1a4657eab07d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/filter_axioms.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-val remove_for_altergo : Why3.Task.task Why3.Trans.trans
-val remove_for_why3 : Why3.Task.task Why3.Trans.trans
-val trans : Why3.Task.task Why3.Trans.trans
-val def_into_axiom : Why3.Task.task Why3.Trans.trans
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw b/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
index 41202b023aaa69c832dcfbe41d8bcf187078bd2f..5b404b69afad998baa87517e0893b76ee92b97af 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
@@ -61,9 +61,6 @@ theory Cbits
axiom land_0bis: forall x:int [land x 0]. (land x 0) = 0
axiom land_1: forall x:int [land (-1) x]. (land (-1) x) = x
axiom land_1bis: forall x:int [land x (-1)]. (land x (-1)) = x
- axiom land_bool:
- (land 0 0) = 0 /\ (land 0 1) = 0 /\ (land 1 0) = 0 /\ (land 1 1) = 1
- meta "remove_for_" axiom land_bool
(** ** lor identities *)
axiom lor_idemp: forall x:int [lor x x]. (lor x x) = x
@@ -72,9 +69,6 @@ theory Cbits
axiom lor_1bis: forall x:int [lor x (-1)]. (lor x (-1)) = -1
axiom lor_0: forall x:int [lor 0 x]. (lor 0 x) = x
axiom lor_0bis: forall x:int [lor x 0]. (lor x 0) = x
- axiom lor_bool:
- (lor 0 0) = 0 /\ (lor 0 1) = 1 /\ (lor 1 0) = 1 /\ (lor 1 1) = 1
- meta "remove_for_" axiom lor_bool
(** ** lxor identities *)
axiom lxor_nilpotent: forall x:int [lxor x x]. (lxor x x) = 0
@@ -83,9 +77,6 @@ theory Cbits
axiom lxor_1bis: forall x:int [lxor x (-1)]. (lxor x (-1)) = (lnot x)
axiom lxor_0: forall x:int [lxor 0 x]. (lxor 0 x) = x
axiom lxor_0bis: forall x:int [lxor x 0]. (lxor x 0) = x
- axiom lxor_bool:
- (lxor 0 0) = 0 /\ (lxor 0 1) = 1 /\ (lxor 1 0) = 1 /\ (lxor 1 1) = 0
- meta "remove_for_" axiom lxor_bool
(** ** lsl identities *)
@@ -115,9 +106,6 @@ theory Cbits
axiom bit_test_extraction: forall x k:int [land x (lsl 1 k)|land (lsl 1 k) x].
0<=k -> (land x (lsl 1 k))<>0 <-> (bit_test x k)
- lemma bit_test_extraction_eq: forall x k:int [land x (lsl 1 k)|land (lsl 1 k) x].
- 0<=k -> (land x (lsl 1 k))=(lsl 1 k) <-> (bit_test x k)
- meta "remove_for_" lemma bit_test_extraction_eq
axiom lsl_1_0:
lsl 1 0 = 1
@@ -126,276 +114,97 @@ theory Cbits
axiom bit_test_extraction_bis_eq: forall x :int [land x 1|land 1 x].
(bit_test x 0) -> (land 1 x)=1
- lemma lnot_extraction_bool: forall x i:int [bit_testb (lnot x) i].
- 0<=i -> bit_testb (lnot x) i = notb (bit_testb x i)
axiom lnot_extraction: forall x i:int [bit_test (lnot x) i].
0<=i -> (bit_test (lnot x) i) <-> not (bit_test x i)
- meta "remove_for_" lemma lnot_extraction_bool
- lemma land_extraction_bool: forall x y i:int [bit_testb (land x y) i].
- 0<=i -> bit_testb (land x y) i = andb (bit_testb x i) (bit_testb y i)
axiom land_extraction: forall x y i:int [bit_test (land x y) i].
0<=i -> bit_test (land x y) i <-> ((bit_test x i) /\ (bit_test y i))
- meta "remove_for_" lemma land_extraction_bool
- lemma lor_extraction_bool: forall x y i:int [bit_testb (lor x y) i].
- 0<=i -> bit_testb (lor x y) i = orb (bit_testb x i) (bit_testb y i)
axiom lor_extraction: forall x y i:int [bit_test (lor x y) i].
0<=i -> (bit_test (lor x y) i) <-> ((bit_test x i) \/ (bit_test y i))
- meta "remove_for_" lemma lor_extraction_bool
- lemma lxor_extraction_bool: forall x y i:int [bit_testb (lxor x y) i].
- 0<=i -> bit_testb (lxor x y) i = xorb (bit_testb x i) (bit_testb y i)
axiom lxor_extraction: forall x y i:int [bit_test (lxor x y) i].
0<=i -> (bit_test (lxor x y) i) <-> ((bit_test x i) <-> not (bit_test y i))
- meta "remove_for_" lemma lxor_extraction_bool
(** ** Shift operators *)
- lemma lsl_1_two_power : forall n : int. 0 <= n -> lsl 1 n = Cint.two_power_abs n
- meta "remove_for_" lemma lsl_1_two_power
axiom land_1_lsl_1 : forall a x n : int [(lsl 1 (1+n)),(lsl 1 n),(2*a+(land 1 x))] .
0<=n -> a<lsl 1 n -> 2*a+(land 1 x)<lsl 1 (1+n)
- lemma lsl_extraction_sup_bool: forall x n m:int [bit_testb (lsl x n) m].
- 0<=n -> 0<=m -> m>=n -> bit_testb (lsl x n) m = bit_testb x (m-n)
axiom lsl_extraction_sup: forall x n m:int [bit_test (lsl x n) m].
0<=n -> 0<=m -> m>=n -> (bit_test (lsl x n) m) <-> (bit_test x (m-n))
- meta "remove_for_" lemma lsl_extraction_sup_bool
- lemma lsl_extraction_inf_bool: forall x n m:int [bit_testb (lsl x n) m].
- 0<=n -> 0<=m -> m< n -> bit_testb (lsl x n) m = False
axiom lsl_extraction_inf: forall x n m:int [bit_test (lsl x n) m].
0<=n -> 0<=m -> m< n -> not (bit_test (lsl x n) m)
- meta "remove_for_" lemma lsl_extraction_inf_bool
- lemma lsr_extraction_bool: forall x n m:int [bit_testb (lsr x n) m].
- 0<=n -> 0<=m -> bit_testb (lsr x n) m = bit_testb x (m+n)
axiom lsr_extractionl: forall x n m:int [bit_test (lsr x n) m].
0<=n -> 0<=m -> (bit_test (lsr x n) m) <-> (bit_test x (m+n))
- meta "remove_for_" lemma lsr_extraction_bool
- lemma lsl1_extraction_bool: forall i j:int [bit_testb (lsl 1 i) j].
- 0<=i -> 0<=j -> bit_testb (lsl 1 i) j = eqb i j
axiom lsl1_extraction: forall i j:int [bit_test (lsl 1 i) j].
0<=i -> 0<=j -> (bit_test (lsl 1 i) j) <-> i=j
- meta "remove_for_" lemma lsl1_extraction_bool
-
- lemma pos_extraction_sup: forall x i j:int [(lsl 1 i),(bit_test x j)].
- 0<=x -> 0<=i -> x < (lsl 1 i) -> i <= j -> not (bit_test x j)
- meta "remove_for_" lemma pos_extraction_sup
-
- lemma pos_extraction_sup_inv: forall x i :int .
- 0<=i -> (forall j: int . i <= j -> not (bit_test x j)) -> 0<= x < (lsl 1 i)
- meta "remove_for_" lemma pos_extraction_sup_inv
(** * Link between Bit extraction and C type conversions *)
-(** ** Unsigned conversions *)
-
- lemma to_uint_extraction_sup: forall n x i:int .
- 0<=n<=i -> is_uint n x -> not (bit_test x i)
- lemma to_uint_extraction_inf_bool: forall n x i:int .
- 0<=i<n -> (bit_testb (to_uint n x) i) = (bit_testb x i)
- lemma to_uint_extraction_inf: forall n x i:int .
- 0<=i<n -> (bit_test (to_uint n x) i) <-> (bit_test x i)
- lemma is_uint_ext : forall n x y:int .
- 0<=n -> is_uint n x -> is_uint n y
- -> (forall i: int. 0<=i<n -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma to_uint_extraction_sup
- meta "remove_for_" lemma to_uint_extraction_inf_bool
- meta "remove_for_" lemma to_uint_extraction_inf
- meta "remove_for_" lemma is_uint_ext
(** *** Cast to uint8 C type *)
axiom to_uint8_extraction_sup: forall x i:int [(is_uint8 x),(bit_test x i)].
8<=i -> is_uint8 x -> not (bit_test x i)
- lemma to_uint8_extraction_inf_bool: forall x i:int [bit_testb (to_uint8 x) i].
- 0<=i<8 -> (bit_testb (to_uint8 x) i) = (bit_testb x i)
axiom to_uint8_extraction_inf: forall x i:int [bit_test (to_uint8 x) i].
0<=i<8 -> (bit_test (to_uint8 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_uint8_extraction_inf_bool
-
- lemma is_uint8_ext : forall x y:int .
- is_uint8 x -> is_uint8 y
- -> (forall i: int. 0<=i<8 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_uint8_ext
(** *** Cast to uint16 C type *)
axiom to_uint16_extraction_sup: forall x i:int [(is_uint16 x),(bit_test x i)].
16<=i -> is_uint16 x -> not (bit_test x i)
- lemma to_uint16_extraction_inf_bool: forall x i:int [bit_testb (to_uint16 x) i].
- 0<=i<16 -> (bit_testb (to_uint16 x) i) = (bit_testb x i)
axiom to_uint16_extraction_inf: forall x i:int [bit_test (to_uint16 x) i].
0<=i<16 -> (bit_test (to_uint16 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_uint16_extraction_inf_bool
-
- lemma is_uint16_ext : forall x y:int .
- is_uint16 x -> is_uint16 y
- -> (forall i: int. 0<=i<16 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_uint16_ext
(** *** Cast to uint32 C type *)
axiom to_uint32_extraction_sup: forall x i:int [(is_uint32 x),(bit_test x i)].
32<=i -> is_uint32 x -> not (bit_test x i)
- lemma to_uint32_extraction_inf_bool: forall x i:int [bit_testb (to_uint32 x) i].
- 0<=i<32 -> (bit_testb (to_uint32 x) i) = (bit_testb x i)
axiom to_uint32_extraction_inf: forall x i:int [bit_test (to_uint32 x) i].
0<=i<32 -> (bit_test (to_uint32 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_uint32_extraction_inf_bool
-
- lemma is_uint32_ext : forall x y:int .
- is_uint32 x -> is_uint32 y
- -> (forall i: int. 0<=i<32 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_uint32_ext
(** *** Cast to uint64 C type *)
axiom to_uint64_extraction_sup: forall x i:int [(is_uint64 x),(bit_test x i)].
64<=i -> (is_uint64 x) -> not (bit_test x i)
- lemma to_uint64_extraction_inf_bool: forall x i:int [bit_testb (to_uint64 x) i].
- 0<=i<64 -> (bit_testb (to_uint64 x) i) = (bit_testb x i)
axiom to_uint64_extraction_inf: forall x i:int [bit_test (to_uint64 x) i].
0<=i<64 -> (bit_test (to_uint64 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_uint64_extraction_inf_bool
-
- lemma is_uint64_ext : forall x y:int .
- is_uint64 x -> is_uint64 y
- -> (forall i: int. 0<=i<64 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_uint64_ext
-
-(** ** Signed conversions *)
- lemma to_sint_extraction_sup: forall n x i:int .
- 0<=n<=i -> is_sint n x -> (bit_test x i) <-> x < 0
- lemma to_sint_extraction_inf_bool: forall n x i:int .
- 0<=i<n -> (bit_testb (to_sint n x) i) = (bit_testb x i)
- lemma to_sint_extraction_inf: forall n x i:int .
- 0<=i<n -> (bit_test (to_sint n x) i) <-> (bit_test x i)
- lemma is_sint_ext : forall n x y:int .
- 0<=n -> is_sint n x -> is_sint n y
- -> (forall i: int. 0<=i<=n -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma to_sint_extraction_sup
- meta "remove_for_" lemma to_sint_extraction_inf_bool
- meta "remove_for_" lemma to_sint_extraction_inf
- meta "remove_for_" lemma is_sint_ext
(** *** Cast to sint8 C type *)
axiom to_sint8_extraction_sup: forall x i:int [(is_sint8 x),(bit_test x i)].
7<=i -> is_sint8 x -> (bit_test x i) <-> x < 0
- lemma to_sint8_extraction_inf_bool: forall x i:int [(bit_testb (to_sint8 x) i)].
- 0<=i<7 -> (bit_testb (to_sint8 x) i) = (bit_testb x i)
axiom to_sint8_extraction_inf: forall x i:int [(bit_test (to_sint8 x) i)].
0<=i<7 -> (bit_test (to_sint8 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_sint8_extraction_inf_bool
-
- lemma is_sint8_ext : forall x y:int .
- is_sint8 x -> is_sint8 y
- -> (forall i: int. 0<=i<=7 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_sint8_ext
(** *** Cast to sint16 C type *)
axiom to_sint16_extraction_sup: forall x i:int [(is_sint16 x),(bit_test x i)].
15<=i -> is_sint16 x -> (bit_test x i) <-> x < 0
- lemma to_sint16_extraction_inf_bool: forall x i:int [bit_testb (to_sint16 x) i].
- 0<=i<15 -> (bit_testb (to_sint16 x) i) = (bit_testb x i)
axiom to_sint16_extraction_inf: forall x i:int [bit_test (to_sint16 x) i].
0<=i<15 -> (bit_test (to_sint16 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_sint16_extraction_inf_bool
-
- lemma is_sint16_ext : forall x y:int .
- is_sint16 x -> is_sint16 y
- -> (forall i: int. 0<=i<=15 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_sint16_ext
(** *** Cast to sint32 C type *)
axiom to_sint32_extraction_sup: forall x i:int [(is_sint32 x),(bit_test x i)].
31<=i -> is_sint32 x -> (bit_test x i) <-> x < 0
- lemma to_sint32_extraction_inf_bool: forall x i:int [bit_testb (to_sint32 x) i].
- 0<=i<31 -> (bit_testb (to_sint32 x) i) = (bit_testb x i)
axiom to_sint32_extraction_inf: forall x i:int [bit_test (to_sint32 x) i].
0<=i<31 -> (bit_test (to_sint32 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_sint32_extraction_inf_bool
-
- lemma is_sint32_ext : forall x y:int .
- is_sint32 x -> is_sint32 y
- -> (forall i: int. 0<=i<=31 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_sint32_ext
(** *** Cast to sint64 C type *)
axiom to_sint64_extraction_sup: forall x i:int [(is_sint64 x),(bit_test x i)].
63<=i -> is_sint64 x -> (bit_test x i) <-> x < 0
- lemma to_sint64_extraction_inf_bool: forall x i:int [bit_testb (to_sint64 x) i].
- 0<=i<63 -> (bit_testb (to_sint64 x) i) = (bit_testb x i)
axiom to_sint64_extraction_inf: forall x i:int [bit_test (to_sint64 x) i].
0<=i<63 -> (bit_test (to_sint64 x) i) <-> (bit_test x i)
- meta "remove_for_" lemma to_sint64_extraction_inf_bool
-
- lemma is_sint64_ext : forall x y:int .
- is_sint64 x -> is_sint64 y
- -> (forall i: int. 0<=i<=63 -> (bit_test x i <-> bit_test y i))
- -> x = y
- meta "remove_for_" lemma is_sint64_ext
-
-(** * Some C-Integer Bits Conversions are distributive *)
-(** ** Unsigned conversions *)
- lemma to_uint_lor : forall n x y:int.
- to_uint n (lor x y) = lor (to_uint n x) (to_uint n y)
- meta "remove_for_" lemma to_uint_lor
-
-(** *** Cast to uint8 C type *)
- lemma to_uint8_lor : forall x y:int [to_uint8 (lor x y)].
- to_uint8 (lor x y) = lor (to_uint8 x) (to_uint 8 y)
- meta "remove_for_" lemma to_uint8_lor
-
-(** *** Cast to uint16 C type *)
- lemma to_uint16_lor : forall x y:int [to_uint16 (lor x y)].
- to_uint16 (lor x y) = lor (to_uint16 x) (to_uint16 y)
- meta "remove_for_" lemma to_uint16_lor
-
-(** *** Cast to uint32 C type *)
- axiom to_uint32_lor : forall x y:int [to_uint32 (lor x y)].
- to_uint32 (lor x y) = lor (to_uint32 x) (to_uint32 y)
- meta "remove_for_" axiom to_uint32_lor
-
-(** *** Cast to uint64 C type *)
- lemma to_uint64_lor : forall x y:int [to_uint64 (lor x y)].
- to_uint64 (lor x y) = lor (to_uint64 x) (to_uint64 y)
- meta "remove_for_" lemma to_uint64_lor
(** * Some C-Integer Bits Conversions are identity *)
(** ** Unsigned conversions *)
lemma is_uint_lxor : forall n x y:int.
is_uint n x -> is_uint n y -> to_uint n (lxor x y) = lxor x y
- lemma is_uint_lor : forall n x y:int.
- is_uint n x -> is_uint n y -> to_uint n (lor x y) = lor x y
- lemma is_uint_land : forall n x y:int.
- is_uint n x -> is_uint n y -> to_uint n (land x y) = land x y
- lemma is_uint_lsr : forall n x y:int.
- 0<=y -> is_uint n x -> to_uint n (lsr x y) = lsr x y
- lemma is_uint_lsl1_inf : forall n y:int.
- 0<=y<n -> to_uint n (lsl 1 y) = lsl 1 y
- lemma is_uint_lsl1_sup : forall n y:int.
- 0<=n<=y -> to_uint n (lsl 1 y) = 0
- meta "remove_for_" lemma is_uint_lor
- meta "remove_for_" lemma is_uint_land
- meta "remove_for_" lemma is_uint_lsr
- meta "remove_for_" lemma is_uint_lsl1_inf
- meta "remove_for_" lemma is_uint_lsl1_sup
(** *** Cast to uint8 C type *)
axiom is_uint8_lxor : forall x y:int [to_uint8 (lxor x y)].
@@ -473,29 +282,6 @@ theory Cbits
axiom is_uint64_lsl1_sup : forall y:int [to_uint64 (lsl 1 y)].
64<=y -> to_uint64 (lsl 1 y) = 0
-(** ** Signed conversions *)
- lemma is_sint_lnot: forall n x:int.
- is_sint n x -> to_sint n (lnot x) = lnot x
- lemma is_sint_lxor: forall n x y:int.
- is_sint n x -> is_sint n y -> to_sint n (lxor x y) = lxor x y
- lemma is_sint_lor: forall n x y:int.
- is_sint n x -> is_sint n y -> to_sint n (lor x y) = lor x y
- lemma is_sint_land: forall n x y:int.
- is_sint n x -> is_sint n y -> to_sint n (land x y) = land x y
- lemma is_sint_lsr: forall n x y:int.
- 0<=y -> is_sint n x -> to_sint n (lsr x y) = lsr x y
- lemma is_sint_lsl1_inf : forall n y:int.
- 0<=y<n -> to_sint n (lsl 1 y) = (lsl 1 y)
- lemma is_sint_lsl1_sup : forall n y:int.
- 0<=n<y -> to_sint n (lsl 1 y) = 0
- meta "remove_for_" lemma is_sint_lnot
- meta "remove_for_" lemma is_sint_lxor
- meta "remove_for_" lemma is_sint_lor
- meta "remove_for_" lemma is_sint_land
- meta "remove_for_" lemma is_sint_lsr
- meta "remove_for_" lemma is_sint_lsl1_inf
- meta "remove_for_" lemma is_sint_lsl1_sup
-
(** *** Cast to sint8 C type *)
lemma is_sint8_lnot: forall x:int [to_sint8 (lnot x)].
is_sint8 x -> to_sint8 (lnot x) = lnot x
@@ -596,27 +382,6 @@ theory Cbits
axiom is_sint64_lsl1_sup : forall y:int [to_sint64 (lsl 1 y)].
64<=y -> to_sint64 (lsl 1 y) = 0
-(** * Range of some bitwise operations *)
- lemma uint_land_range : forall x y: int .
- 0<=x -> 0 <= land x y <= x
- meta "remove_for_" lemma uint_land_range
-
- lemma uint_lor_inf : forall x y: int .
- -1<=x -> 0<=y -> x <= lor x y
- meta "remove_for_" lemma uint_lor_inf
-
- lemma sint_land_inf : forall x y: int .
- x<=0 -> y<0 -> land x y <= x
- meta "remove_for_" lemma sint_land_inf
-
- lemma sint_lor_range : forall x y: int .
- x<0 -> x <= lor x y < 0
- meta "remove_for_" lemma sint_lor_range
-
- lemma is_uint_lor_distrib : forall n x y: int .
- (is_uint n (lor x y)) <-> ((is_uint n x) && (is_uint n y))
- meta "remove_for_" lemma is_uint_lor_distrib
-
(** * Link between bitwise operators and addition *)
axiom lor_addition : forall x y: int [(land x y), (lor x y) ].
land x y = 0 -> x + y = lor x y
@@ -624,9 +389,4 @@ theory Cbits
axiom lxor_addition : forall x y: int [(land x y), (lxor x y) ].
land x y = 0 -> x + y = lxor x y
-(** * Link between land and cast operator *)
- lemma to_uint_land_edge : forall x n: int.
- 0<=n -> to_uint n x = land ((lsl 1 n) - 1) x
- meta "remove_for_" lemma to_uint_land_edge
-
end
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
index 22f2e79f9ec522f3af333431a0fdbf07e0b1cbc6..471483d7973536f23fc05ce497726f001542b8ce 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
@@ -44,28 +44,48 @@ theory Cint
(** * C-Integer Ranges * **)
- predicate is_bool(x:int) = x = 0 \/ x = 1
- predicate is_uint8(x:int) = 0 <= x < max_uint8
- predicate is_sint8(x:int) = -max_sint8 <= x < max_sint8
- predicate is_uint16(x:int) = 0 <= x < max_uint16
- predicate is_sint16(x:int) = -max_sint16 <= x < max_sint16
- predicate is_uint32(x:int) = 0 <= x < max_uint32
- predicate is_sint32(x:int) = -max_sint32 <= x < max_sint32
- predicate is_uint64(x:int) = 0 <= x < max_uint64
- predicate is_sint64(x:int) = -max_sint64 <= x < max_sint64
-
- lemma is_bool0: is_bool(0)
- lemma is_bool1: is_bool(1)
-
- (* meta "def_into_axiom" predicate is_bool *)
- meta "def_into_axiom" predicate is_uint8
- meta "def_into_axiom" predicate is_sint8
- meta "def_into_axiom" predicate is_uint16
- meta "def_into_axiom" predicate is_uint16
- meta "def_into_axiom" predicate is_sint32
- meta "def_into_axiom" predicate is_uint32
- meta "def_into_axiom" predicate is_sint64
- meta "def_into_axiom" predicate is_uint64
+ predicate is_bool (x:int) = x = 0 \/ x = 1
+
+ predicate is_uint8 int
+
+ axiom is_uint8_def :
+ forall x:int [is_uint8 x]. is_uint8 x <-> 0 <= x /\ x < max_uint8
+
+ predicate is_sint8 int
+
+ axiom is_sint8_def :
+ forall x:int [is_sint8 x]. is_sint8 x <-> (- max_sint8) <= x /\ x < max_sint8
+
+ predicate is_uint16 int
+
+ axiom is_uint16_def :
+ forall x:int [is_uint16 x]. is_uint16 x <-> 0 <= x /\ x < max_uint16
+
+ predicate is_sint16 (x:int) = (- max_sint16) <= x /\ x < max_sint16
+
+ predicate is_uint32 int
+
+ axiom is_uint32_def :
+ forall x:int [is_uint32 x]. is_uint32 x <-> 0 <= x /\ x < max_uint32
+
+ predicate is_sint32 int
+
+ axiom is_sint32_def :
+ forall x:int [is_sint32 x]. is_sint32 x <-> (- max_sint32) <= x /\ x < max_sint32
+
+ predicate is_uint64 int
+
+ axiom is_uint64_def :
+ forall x:int [is_uint64 x]. is_uint64 x <-> 0 <= x /\ x < max_uint64
+
+ predicate is_sint64 int
+
+ axiom is_sint64_def :
+ forall x:int [is_sint64 x]. is_sint64 x <-> (- max_sint64) <= x /\ x < max_sint64
+
+ lemma is_bool0 : is_bool 0
+
+ lemma is_bool1 : is_bool 1
(** * C-Integer Conversion * **)
@@ -80,12 +100,6 @@ theory Cint
function to_sint64 int : int
function two_power_abs int : int
- lemma two_power_abs_is_positive : forall n:int [ two_power_abs n ]. 0 < two_power_abs n
- lemma two_power_abs_plus_pos : forall n m:int . 0 <= n -> 0 <= m -> two_power_abs (n+m) = (two_power_abs n) * (two_power_abs m)
- lemma two_power_abs_plus_one : forall n:int . 0 <= n -> two_power_abs (n+1) = 2 * (two_power_abs n)
- meta "remove_for_" lemma two_power_abs_is_positive
- meta "remove_for_" lemma two_power_abs_plus_pos
- meta "remove_for_" lemma two_power_abs_plus_one
predicate is_uint (n:int) (x:int) = 0 <= x < two_power_abs n
@@ -97,11 +111,6 @@ theory Cint
(** * C-Integer Conversions are in-range * **)
- lemma is_to_uint : forall n x:int [ is_uint n (to_uint n x) ]. is_uint n (to_uint n x)
- lemma is_to_sint : forall n x:int [ is_sint n (to_sint n x) ]. is_sint n (to_sint n x)
- meta "remove_for_" lemma is_to_uint
- meta "remove_for_" lemma is_to_sint
-
axiom is_to_uint8 : forall x:int. is_uint8 (to_uint8 x)
axiom is_to_sint8 : forall x:int. is_sint8 (to_sint8 x)
axiom is_to_uint16 : forall x:int. is_uint16 (to_uint16 x)
@@ -113,84 +122,20 @@ theory Cint
(** * C-Integer Conversions are identity when in-range * **)
- lemma id_uint : forall n x:int [ to_uint n x ]. is_uint n x <-> (to_uint n x) = x
- lemma id_sint : forall n x:int [ to_sint n x ]. is_sint n x <-> (to_sint n x) = x
- meta "remove_for_" lemma id_uint
- meta "remove_for_" lemma id_sint
-
- axiom id_uint8 : forall x:int [ to_uint8 x ]. is_uint8 x -> (to_uint8 x) = x
- axiom id_sint8 : forall x:int [ to_sint8 x ]. is_sint8 x -> (to_sint8 x) = x
- axiom id_uint16 : forall x:int [ to_uint16 x ]. is_uint16 x -> (to_uint16 x) = x
- axiom id_sint16 : forall x:int [ to_sint16 x ]. is_sint16 x -> (to_sint16 x) = x
- axiom id_uint32 : forall x:int [ to_uint32 x ]. is_uint32 x -> (to_uint32 x) = x
- axiom id_sint32 : forall x:int [ to_sint32 x ]. is_sint32 x -> (to_sint32 x) = x
- axiom id_uint64 : forall x:int [ to_uint64 x ]. is_uint64 x -> (to_uint64 x) = x
- axiom id_sint64 : forall x:int [ to_sint64 x ]. is_sint64 x -> (to_sint64 x) = x
-
- meta "inline_in" predicate is_uint8, axiom id_uint8
- meta "inline_in" predicate is_sint8, axiom id_sint8
- meta "inline_in" predicate is_uint16, axiom id_uint16
- meta "inline_in" predicate is_sint16, axiom id_sint16
- meta "inline_in" predicate is_uint32, axiom id_uint32
- meta "inline_in" predicate is_sint32, axiom id_sint32
- meta "inline_in" predicate is_uint64, axiom id_uint64
- meta "inline_in" predicate is_sint64, axiom id_sint64
-
- (** * C-Integer Conversions are projections * **)
-
- lemma proj_uint : forall n x:int . to_uint n (to_uint n x)= to_uint n x
- lemma proj_sint : forall n x:int . to_sint n (to_sint n x)= to_sint n x
- meta "remove_for_" lemma proj_uint
- meta "remove_for_" lemma proj_sint
-
- axiom proj_uint8 : forall x:int [ to_uint8(to_uint8 x) ]. to_uint8(to_uint8 x)=to_uint8 x
- axiom proj_sint8 : forall x:int [ to_sint8(to_sint8 x) ]. to_sint8(to_sint8 x)=to_sint8 x
- axiom proj_uint16 : forall x:int [ to_uint16(to_uint16 x) ]. to_uint16(to_uint16 x)=to_uint16 x
- axiom proj_sint16 : forall x:int [ to_sint16(to_sint16 x) ]. to_sint16(to_sint16 x)=to_sint16 x
- axiom proj_uint32 : forall x:int [ to_uint32(to_uint32 x) ]. to_uint32(to_uint32 x)=to_uint32 x
- axiom proj_sint32 : forall x:int [ to_sint32(to_sint32 x) ]. to_sint32(to_sint32 x)=to_sint32 x
- axiom proj_uint64 : forall x:int [ to_uint64(to_uint64 x) ]. to_uint64(to_uint64 x)=to_uint64 x
- axiom proj_sint64 : forall x:int [ to_sint64(to_sint64 x) ]. to_sint64(to_sint64 x)=to_sint64 x
-
- meta "remove_for_" axiom proj_uint8
- meta "remove_for_" axiom proj_sint8
- meta "remove_for_" axiom proj_uint16
- meta "remove_for_" axiom proj_sint16
- meta "remove_for_" axiom proj_uint32
- meta "remove_for_" axiom proj_sint32
- meta "remove_for_" axiom proj_uint64
- meta "remove_for_" axiom proj_sint64
+ axiom id_uint8 : forall x:int [ to_uint8 x ]. 0 <= x < max_uint8 -> (to_uint8 x) = x
+ axiom id_sint8 : forall x:int [ to_sint8 x ]. -max_sint8 <= x < max_sint8 -> (to_sint8 x) = x
+ axiom id_uint16 : forall x:int [ to_uint16 x ]. 0 <= x < max_uint16 -> (to_uint16 x) = x
+ axiom id_sint16 : forall x:int [ to_sint16 x ]. -max_sint16 <= x < max_sint16 -> (to_sint16 x) = x
+ axiom id_uint32 : forall x:int [ to_uint32 x ]. 0 <= x < max_uint32 -> (to_uint32 x) = x
+ axiom id_sint32 : forall x:int [ to_sint32 x ]. -max_sint32 <= x < max_sint32 -> (to_sint32 x) = x
+ axiom id_uint64 : forall x:int [ to_uint64 x ]. 0 <= x < max_uint64 -> (to_uint64 x) = x
+ axiom id_sint64 : forall x:int [ to_sint64 x ]. -max_sint64 <= x < max_sint64 -> (to_sint64 x) = x
(** * Generalization for [to_sint _ (to_uint _ x)] * **)
- lemma proj_su: forall n x:int . to_sint n (to_uint n x) = to_uint n x
- lemma incl_su: forall n x:int . is_uint n x -> is_sint n x
- meta "remove_for_" lemma proj_su
- meta "remove_for_" lemma incl_su
-
- lemma proj_su_uint: forall n m x:int . 0 <= n -> 0 <= m -> to_sint (m+n) (to_uint n x) = to_uint n x
- lemma proj_su_sint: forall n m x:int . 0 <= n -> 0 <= m -> to_sint n (to_uint (m+(n+1)) x) = to_sint n x
- meta "remove_for_" lemma proj_su_uint
- meta "remove_for_" lemma proj_su_sint
-
axiom proj_int8 : forall x:int [ to_sint8(to_uint8 x) ]. to_sint8(to_uint8 x) =to_sint8 x
axiom proj_int16 : forall x:int [ to_sint16(to_uint16 x) ]. to_sint16(to_uint16 x)=to_sint16 x
axiom proj_int32 : forall x:int [ to_sint32(to_uint32 x) ]. to_sint32(to_uint32 x)=to_sint32 x
axiom proj_int64 : forall x:int [ to_sint64(to_uint64 x) ]. to_sint64(to_uint64 x)=to_sint64 x
- (** * Generalization for [to_uint _ (to_sint _ x)] * **)
-
- lemma proj_us_uint: forall n m x:int . 0 <= n -> 0 <= m -> to_uint (n+1) (to_sint (m+n) x) = to_uint (n+1) x
- meta "remove_for_" lemma proj_us_uint
-
- (** * C-Integer range inclusion * **)
-
- lemma incl_uint : forall n x i:int . 0 <= n -> 0 <= i -> is_uint n x -> is_uint (n+i) x
- lemma incl_sint : forall n x i:int . 0 <= n -> 0 <= i -> is_sint n x -> is_sint (n+i) x
- lemma incl_int : forall n x i:int . 0 <= n -> 0 <= i -> is_uint n x -> is_sint (n+i) x
- meta "remove_for_" lemma incl_uint
- meta "remove_for_" lemma incl_sint
- meta "remove_for_" lemma incl_int
-
-
end
diff --git a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
index b9429ed30474464bea60bc1ae8827c87beb65f13..1404e517aad7cfb0063e578ea088761890f7debf 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
@@ -34,9 +34,6 @@ theory Qed
function eqb (x y : 'a) : bool (*= if x = y then True else False*)
axiom eqb : forall x:'a, y:'a. eqb x y = True <-> x = y
- axiom eqb_false : forall x:'a, y:'a. eqb x y = False <-> x <> y
- meta "remove_for_" axiom eqb_false
-
function neqb (x y : 'a) : bool(* = if x <> y then True else False*)
axiom neqb : forall x:'a, y:'a. neqb x y = True <-> x <> y
diff --git a/src/plugins/wp/wp.ml b/src/plugins/wp/wp.ml
index abeb0a7931bed7a557bac4234534ecc5a5447fdf..c10ae35f5359dc4847111b07da904c402c24fefd 100644
--- a/src/plugins/wp/wp.ml
+++ b/src/plugins/wp/wp.ml
@@ -170,7 +170,6 @@ module Filtering = Filtering
(** {2 Prover Interface} *)
module Why3Provers = Why3Provers
-module Filter_axioms = Filter_axioms
module Prover = Prover
module ProverTask = ProverTask
module ProverWhy3 = ProverWhy3