From e762f5a659fe0a6905b9ef07fde81ba81051a04c Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 18 Nov 2021 11:32:50 +0100
Subject: [PATCH] [eacsl] Remove hypotheses when reemitting invalid properties
during AST preparation
---
.../src/project_initializer/prepare_ast.ml | 35 ++++++++++++++++---
1 file changed, 31 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index f6b87213875..ff197b64c36 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -203,7 +203,34 @@ let dup_global loc spec sound_verdict_vi kf vi new_vi =
let e = Emitter.Usable_emitter.get ep.emitter in
if ep.logical_consequence
then logical_consequence e new_ip ep.properties
- else emit e new_ip ~hyps:ep.properties status
+ else
+ let status, hyps =
+ match status, ep.properties with
+ | True, _ | Dont_know, _
+ | False_and_reachable, [] | False_if_reachable, [] ->
+ (* Valid emission: either [true] status with arbitrary hypotheses or
+ [false] status with empty hypotheses. *)
+ status, ep.properties
+ | False_and_reachable, [ IPReachable _ ]
+ | False_if_reachable, [ IPReachable _ ] ->
+ (* [False] status with a reachability hypothesis: remove the
+ hypothesis and set the status to [False_if_reachable]. *)
+ False_if_reachable, []
+ | False_and_reachable, hyps | False_if_reachable, hyps ->
+ (* Invalid emission: [false]Â status with arbitrary hypotheses. *)
+ Options.fatal
+ "Property with status '%s' and non-empty hypotheses:\n\
+ * Property: %a\n\
+ * Hypotheses:\n- %a"
+ (match status with
+ | True -> "True"
+ | Dont_know -> "Dont_know"
+ | False_if_reachable -> "False_if_reachable"
+ | False_and_reachable -> "False_and_reachable")
+ Property.short_pretty new_ip
+ (Pretty_utils.pp_list ~sep:"\n- " Property.short_pretty) hyps
+ in
+ emit e new_ip ~hyps status
in
match get old_ip with
| Never_tried ->
@@ -212,9 +239,9 @@ let dup_global loc spec sound_verdict_vi kf vi new_vi =
List.iter (cp s) epl
| Inconsistent icst ->
List.iter (cp True) icst.valid;
- (* either the program is reachable and [False_and_reachable] is
- fine, or the program point is not reachable and it does not
- matter for E-ACSL that checks it at runtime. *)
+ (* Copy invalid properties with [False_and_reachable], if a reachability
+ hypothesis is present then the [cp] function will convert it to
+ [False_if_reachable]. *)
List.iter (cp False_and_reachable) icst.invalid
in
let ips kf s = Property.ip_of_spec kf Kglobal ~active:[] s in
--
GitLab