From 54ca5b81d5dd6907f3a3254f6cf2753b2bdf7918 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 26 Jul 2019 11:40:59 +0200
Subject: [PATCH] [Inout] Fixes the location computed for \exit_status in
assigns clauses.
Handles \exit_status exactly as \result.
---
src/plugins/inout/operational_inputs.ml | 7 ++++---
tests/spec/oracle/assigns_result.res.oracle | 2 --
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 3df4c008632..ea48d5ad04b 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -115,20 +115,21 @@ let eval_assigns kf state assigns =
not (Kernel_function.is_formal v kf)
| Base.CLogic_Var _ | Base.Null | Base.String _ -> true)
in
+ let out_term = out.it_content in
let outputs_under, outputs_over, deps =
try
- if Logic_utils.is_result out.it_content
+ if Logic_const.(is_result out_term || is_exit_status out_term)
then (Zone.bottom, Zone.bottom, Zone.bottom)
else
let loc_out_under, loc_out_over, deps =
- !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out.it_content
+ !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out_term
in
(enumerate_valid_bits_under Write loc_out_under,
enumerate_valid_bits Write loc_out_over,
clean_deps deps)
with Db.Properties.Interp.No_conversion ->
Inout_parameters.warning ~current:true ~once:true
- "failed to interpret assigns clause '%a'" Printer.pp_term out.it_content;
+ "failed to interpret assigns clause '%a'" Printer.pp_term out_term;
(Zone.bottom, Zone.top, Zone.top)
in
(* Compute all inputs as a zone *)
diff --git a/tests/spec/oracle/assigns_result.res.oracle b/tests/spec/oracle/assigns_result.res.oracle
index be625108d0c..f492644ff77 100644
--- a/tests/spec/oracle/assigns_result.res.oracle
+++ b/tests/spec/oracle/assigns_result.res.oracle
@@ -11,8 +11,6 @@
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/spec/assigns_result.i:16.
-[inout] tests/spec/assigns_result.i:16: Warning:
- failed to interpret assigns clause '\exit_status'
[eva] using specification for function g
[eva] tests/spec/assigns_result.i:16: Warning:
cannot interpret assigns clause \exit_status
--
GitLab