From 4f2fe8748b5b486dcdc90a3490fd1a3e34616fec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Jan 2021 18:20:39 +0100
Subject: [PATCH] [kernel] Property status: changes [automatically_proven] into
[automatically_computed].
---
.../ast_data/property_status.ml | 23 +++----------------
.../ast_data/property_status.mli | 4 ++--
src/plugins/value/legacy/eval_annots.ml | 2 +-
3 files changed, 6 insertions(+), 23 deletions(-)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index e6eae23d70b..0bec8e3b4c0 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -694,27 +694,10 @@ and get_status ?(must_register=true) ppt =
(* local alias: too much local definitions of get implies name clashes *)
let get ppt = get_status ppt
-let automatically_proven ppt =
+let automatically_computed ppt =
match property_kind ppt with
- | Hypothesis | Unverifiable | Ignored | Other -> false
- | Consequence _ | Tautology ->
- (* nobody else tried to prove it *)
- try
- let by_emitter = Status.find ppt in
- try
- Emitter_with_properties.Hashtbl.iter
- (fun e _ ->
- if not (Emitter.equal
- (Emitter.Usable_emitter.get e.emitter)
- Emitter.kernel)
- then raise Exit)
- by_emitter;
- true
- with Exit ->
- false
- with Not_found ->
- true
-
+ | Hypothesis | Unverifiable | Ignored | Consequence _ | Tautology -> true
+ | Other -> false
(**************************************************************************)
(** {3 Consolidated property status} *)
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 3cf7daca5c6..5656c38152b 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -261,8 +261,8 @@ val merge: old:Property.t list -> Property.t list -> unit
(** [merge old new] registers properties in [new] which are not in [old] and
removes properties in [old] which are not in [new]. *)
-val automatically_proven: Property.t -> bool
-(** Is the status of the given property only automatically handled by the
+val automatically_computed: Property.t -> bool
+(** Is the status of the given property only automatically handled by the
kernel? *)
(*
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index cffbd71e788..f9c730b433d 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -47,7 +47,7 @@ let code_annotation_loc ca stmt =
let mark_unreachable () =
let mark ppt =
- if not (Property_status.automatically_proven ppt) then begin
+ if not (Property_status.automatically_computed ppt) then begin
Value_parameters.debug "Marking property %a as dead"
Description.pp_property ppt;
let emit =
--
GitLab