From c40c026f14b228f5e3e5b6f70c34422bc4858798 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 16 Sep 2020 17:53:20 +0200
Subject: [PATCH] [report] allows updating property status
---
src/plugins/report/tests/report/no_hyp.ml | 42 ++++++++++-------
.../tests/report/oracle/single.1.res.oracle | 46 ++++++++++++++++---
2 files changed, 65 insertions(+), 23 deletions(-)
diff --git a/src/plugins/report/tests/report/no_hyp.ml b/src/plugins/report/tests/report/no_hyp.ml
index cb651465511..a145963f447 100644
--- a/src/plugins/report/tests/report/no_hyp.ml
+++ b/src/plugins/report/tests/report/no_hyp.ml
@@ -1,4 +1,4 @@
-let emitter =
+let emitter =
Emitter.create "Test" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
let set_status s =
@@ -11,7 +11,7 @@ let set_status s =
let print_status =
Dynamic.get
~plugin:"Report"
- "print"
+ "print"
(Datatype.func Datatype.unit Datatype.unit)
let clear () =
@@ -20,26 +20,36 @@ let clear () =
()
let main () =
- Ast.compute ();
- Kernel.feedback "SETTING STATUS TO dont_know";
- set_status Property_status.Dont_know;
- print_status ();
- Kernel.feedback "SETTING STATUS TO true";
- set_status Property_status.True;
- print_status ();
+ begin
+ Ast.compute ();
+ Kernel.feedback "SETTING STATUS TO dont_know";
+ set_status Property_status.Dont_know;
+ print_status ();
+ Kernel.feedback "SETTING STATUS TO true";
+ set_status Property_status.True;
+ print_status ();
+ Kernel.feedback "SETTING STATUS TO false_if_reachable";
+ set_status Property_status.False_if_reachable;
+ print_status ();
+ Kernel.feedback "SETTING STATUS TO dont_know";
+ set_status Property_status.Dont_know;
+ print_status ();
+ Kernel.feedback "SETTING STATUS TO true";
+ set_status Property_status.True;
+ print_status ();
+ Kernel.feedback "SETTING STATUS TO false_if_reachable";
+ set_status Property_status.False_if_reachable;
+ print_status ();
+ (*
Kernel.feedback "SETTING STATUS TO false_if_reachable";
(try set_status Property_status.False_if_reachable
with Property_status.Inconsistent_emitted_status(s1, s2) ->
- Kernel.result "inconsistency between %a and %a"
+ Kernel.result "inconsistency between %a and %a"
Property_status.Emitted_status.pretty s1
Property_status.Emitted_status.pretty s2);
Kernel.feedback "CLEARING";
clear ();
- Kernel.feedback "SETTING STATUS TO false_if_reachable";
- set_status Property_status.False_if_reachable;
- print_status ();
- Kernel.feedback "SETTING STATUS TO false_and_reachable";
- set_status Property_status.False_and_reachable;
- print_status ()
+ *)
+ end
let () = Db.Main.extend main
diff --git a/src/plugins/report/tests/report/oracle/single.1.res.oracle b/src/plugins/report/tests/report/oracle/single.1.res.oracle
index a47026150e0..088835a7a67 100644
--- a/src/plugins/report/tests/report/oracle/single.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/single.1.res.oracle
@@ -32,9 +32,6 @@
1 Total
--------------------------------------------------------------------------------
[kernel] SETTING STATUS TO false_if_reachable
-[kernel] inconsistency between **NOT** VALID and VALID
-[kernel] CLEARING
-[kernel] SETTING STATUS TO false_if_reachable
[report] Computing properties status...
--------------------------------------------------------------------------------
@@ -51,19 +48,54 @@
1 Alarm emitted
1 Total
--------------------------------------------------------------------------------
-[kernel] SETTING STATUS TO false_and_reachable
+[kernel] SETTING STATUS TO dont_know
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
-[ Bug ] Assertion (file tests/report/single.i, line 9)
- by Test.
+[ Alarm ] Assertion (file tests/report/single.i, line 9)
+ By Test, with pending:
+ - Unreachable program point (file tests/report/single.i, line 9)
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 1 Bugs found
+ 1 Alarm emitted
+ 1 Total
+--------------------------------------------------------------------------------
+[kernel] SETTING STATUS TO true
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ Alarm ] Assertion (file tests/report/single.i, line 9)
+ By Test, with pending:
+ - Unreachable program point (file tests/report/single.i, line 9)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Alarm emitted
+ 1 Total
+--------------------------------------------------------------------------------
+[kernel] SETTING STATUS TO false_if_reachable
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ Alarm ] Assertion (file tests/report/single.i, line 9)
+ By Test, with pending:
+ - Unreachable program point (file tests/report/single.i, line 9)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Alarm emitted
1 Total
--------------------------------------------------------------------------------
--
GitLab