From 51960af6234a8d94435aced593a5aef16e08a22b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Oct 2020 15:54:57 +0200
Subject: [PATCH] [Eva] Do not record the logical status of "admit" predicates.
---
src/plugins/value/engine/transfer_logic.ml | 40 ++++++++++++++--------
1 file changed, 25 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 9308063e3e2..2293ed64aef 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -220,8 +220,8 @@ let ip_from_precondition kf call_ki b pre =
let process_inactive_behavior kf call_ki behavior =
let emitted = ref false in
(* We emit a valid status for every requires and ensures of the behavior. *)
- List.iter (fun (tk, _ as post) ->
- if tk = Normal then begin
+ List.iter (fun (tk, pred as post) ->
+ if tk = Normal && pred.ip_content.tp_kind <> Admit then begin
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal behavior post in
@@ -229,9 +229,11 @@ let process_inactive_behavior kf call_ki behavior =
end
) behavior.b_post_cond;
List.iter (fun pre ->
- emitted := true;
- let ip = ip_from_precondition kf call_ki behavior pre in
- emit_status ip Property_status.True;
+ if pre.ip_content.tp_kind <> Admit then begin
+ emitted := true;
+ let ip = ip_from_precondition kf call_ki behavior pre in
+ emit_status ip Property_status.True;
+ end
) behavior.b_requires;
if !emitted then
Value_parameters.result ~once:true ~current:true ~level:2
@@ -247,8 +249,8 @@ let process_inactive_postconds kf inactive_bhvs =
List.iter
(fun b ->
let emitted = ref false in
- List.iter (fun (tk, _ as post) ->
- if tk = Normal then begin
+ List.iter (fun (tk, pred as post) ->
+ if tk = Normal && pred.ip_content.tp_kind <> Admit then begin
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal b post in
@@ -387,7 +389,7 @@ module Make
let eval_split_and_reduce limit ~reduce pred build_env state =
let env = build_env state in
let status = Domain.evaluate_predicate env state pred in
- let reduced_states =
+ let reduced_states =
if reduce then
match status with
| Alarmset.False -> States.empty
@@ -453,12 +455,13 @@ module Make
let emit = emit_message_and_status kind kf behavior ~active in
let aux_pred states pred =
let pr = Logic_const.pred_of_id_pred pred in
+ let record = pred.ip_content.tp_kind <> Admit in
let reduce = active && pred.ip_content.tp_kind <> Check in
let ip = build_prop pred in
if ignore_predicate pr then
states
else if States.is_empty states then begin
- emit ~empty:true ip pr Alarmset.True;
+ if record then emit ~empty:true ip pr Alarmset.True;
states
end
else
@@ -472,8 +475,12 @@ module Make
fst (States.merge ~into:acc_states reduced_states)))
states ([], States.empty)
in
- List.iter (fun status -> emit ~empty:false ip pr status) statuses;
- check_ensures_false kf behavior active pr kind statuses;
+ if record
+ then
+ begin
+ List.iter (fun status -> emit ~empty:false ip pr status) statuses;
+ check_ensures_false kf behavior active pr kind statuses;
+ end;
States.reorder reduced_states
in
List.fold_left aux_pred states ips
@@ -596,13 +603,14 @@ module Make
| Some loc when not (Cil_datatype.Location.(equal loc unknown)) -> loc
| _ -> Cil_datatype.Stmt.loc stmt
+
(* Reduce the given states according to the given code annotations.
If [record] is true, update the proof state of the code annotation.
DO NOT PASS record=false unless you know what your are doing *)
let interp_annot ~limit ~record kf ab stmt code_annot ~initial_state states =
let ips = Property.ip_of_code_annot kf stmt code_annot in
let source, _ = code_annotation_loc code_annot stmt in
- let aux_interp ~reduce code_annot behav p =
+ let aux_interp ~record ~reduce code_annot behav p =
let text = code_annotation_text code_annot in
let in_behavior =
match behav with
@@ -673,7 +681,7 @@ module Make
'nice' ordering *)
if reduce then States.reorder reduced_states else states
in
- let aux code_annot ~reduce behav p =
+ let aux code_annot ~record ~reduce behav p =
if ignore_predicate p then
states
else if States.is_empty states then (
@@ -686,12 +694,14 @@ module Make
end;
states
) else
- aux_interp ~reduce code_annot behav p
+ aux_interp ~record ~reduce code_annot behav p
in
match code_annot.annot_content with
| AAssert (behav, p)
| AInvariant (behav, true, p) ->
- aux ~reduce:(p.tp_kind <> Check) code_annot behav p.tp_statement
+ let record = record && p.tp_kind <> Admit in
+ let reduce = p.tp_kind <> Check in
+ aux ~record ~reduce code_annot behav p.tp_statement
| APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _ | AExtended _
--
GitLab