From 5b3b29865f40ab9f96d7a343ba8fb92608fcc64b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 19 Jan 2021 08:38:42 +0100
Subject: [PATCH] [wp] remove unused code
---
src/plugins/wp/wpAnnot.ml | 38 --------------------------------------
src/plugins/wp/wpAnnot.mli | 9 ---------
2 files changed, 47 deletions(-)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index b99158d3cd2..84ab16c03be 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -127,41 +127,6 @@ let is_proved pf =
let is_invalid pf =
pf.invalid && not (is_proved pf)
-(* -------------------------------------------------------------------------- *)
-(* --- Function Contracts --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Properties for kf-conditions of termination-kind 'tkind' *)
-let get_called_postconds (tkind:termination_kind) kf =
- let bhvs = Annotations.behaviors kf in
- List.fold_left
- (fun properties bhv ->
- List.fold_left
- (fun properties postcond ->
- if tkind = fst postcond then
- let pid_spec = Property.ip_of_ensures kf Kglobal bhv postcond in
- pid_spec :: properties
- else properties)
- properties bhv.b_post_cond)
- []
- bhvs
-
-let get_called_post_conditions = get_called_postconds Cil_types.Normal
-let get_called_exit_conditions = get_called_postconds Cil_types.Exits
-
-(** Properties for assigns of kf *)
-let get_called_assigns kf =
- let bhvs = Annotations.behaviors kf in
- List.fold_left
- (fun properties bhv ->
- if Cil.is_default_behavior bhv then
- match Property.ip_assigns_of_behavior kf Kglobal [] bhv with
- | None -> properties
- | Some ip -> ip :: properties
- else properties)
- []
- bhvs
-
(* -------------------------------------------------------------------------- *)
(* --- Preconditions at Callsites --- *)
(* -------------------------------------------------------------------------- *)
@@ -185,9 +150,6 @@ let preconditions_at_call s = function
List.map aux preconds
| Cil2cfg.Dynamic _ -> []
-let get_called_preconditions_at kf stmt =
- List.map snd (call_preconditions kf stmt)
-
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Behaviors --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 74f2c0d972d..aee06d48536 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -55,15 +55,6 @@ val dependencies : proof -> Property.t list
val filter_status : prop_id -> bool
-(* -------------------------------------------------------------------------- *)
-(* --- Property Accessors : Function Calls --- *)
-(* -------------------------------------------------------------------------- *)
-
-val get_called_preconditions_at : kernel_function -> stmt -> Property.t list
-val get_called_post_conditions : kernel_function -> Property.t list
-val get_called_exit_conditions : kernel_function -> Property.t list
-val get_called_assigns : kernel_function -> Property.t list
-
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Behaviors --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab