From 1a7d7665dd2eb27b95b2066e1c881803f33b8ec3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Oct 2020 12:23:38 +0200
Subject: [PATCH] [kernel] Admitted properties always have the Considered_valid
status.
Plugins cannot emit a status for admitted properties.
---
.../ast_data/property_status.ml | 21 +++++++++++++++++--
1 file changed, 19 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index e70cdf7f9f8..dc912390898 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -338,6 +338,19 @@ let merge_distinct_emitted x y = match x, y with
| False_if_reachable, True | True, False_if_reachable ->
raise Unmergeable
+let is_admitted_code_annot = function
+ | Cil_types.AAssert (_, tp)
+ | Cil_types.AInvariant (_, _, tp) -> tp.tp_kind = Admit
+ | _ -> false
+
+let rec is_admitted = function
+ | Property.IPPredicate ip -> ip.ip_pred.ip_content.tp_kind = Admit
+ | IPAxiom _ -> true
+ | IPLemma lemma -> lemma.il_pred.tp_kind = Admit
+ | IPCodeAnnot ca -> is_admitted_code_annot ca.ica_ca.annot_content
+ | IPPropertyInstance instance -> is_admitted instance.ii_ip
+ | _ -> false
+
module Register_hook = Hook.Build (struct type t = Property.t end)
let register_property_add_hook = Register_hook.extend
@@ -557,7 +570,9 @@ let emit_and_get e ~hyps ppt ?distinct s =
| IPExtended _
| IPTypeInvariant _ | IPGlobalInvariant _ -> ()
end;
- unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
+ if is_admitted ppt
+ then True (* TODO: fail here? *)
+ else unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
let emit e ~hyps ppt ?distinct s = ignore (emit_and_get e ~hyps ppt ?distinct s)
@@ -644,7 +659,9 @@ let conjunction s1 s2 = match s1, s2 with
| Dont_know, _ | _, Dont_know -> Dont_know
| True, True -> True
-let is_not_verifiable_but_valid ppt status = match status with
+let is_not_verifiable_but_valid ppt status =
+ is_admitted ppt ||
+ match status with
| Never_tried ->
(match ppt with
| Property.IPOther _ ->
--
GitLab