From 27bf243d54b524a3d19ec35692593a4b62315ce1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 26 Feb 2019 11:03:12 +0100
Subject: [PATCH] [Gui] In the property filter, separates user assertions and
user checks.
---
src/plugins/gui/property_navigator.ml | 17 +++++++++++++----
1 file changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index a859ed50bd7..8ada692acfd 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -112,6 +112,7 @@ module Refreshers: sig
val assigns: check
val from: check
val user_assertions: check
+ val user_checks: check
val rte: check
val invariant: check
val variant: check
@@ -239,6 +240,8 @@ struct
~hint:"Show functional dependencies in function assigns"
let user_assertions =
add ~name:"User assertions" ~hint:"Show user assertions" ()
+ let user_checks =
+ add ~name:"User checks" ~hint:"Show user checks" ()
(* Function called when RTEs are enabled or disabled. *)
let set_rte = ref (fun _b -> ())
let rte = add ~set:(fun b -> !set_rte b) ~name:"RTEs"
@@ -360,6 +363,7 @@ struct
assigns.add hb;
from.add hb;
user_assertions.add hb;
+ user_checks.add hb;
rte.add hb;
invariant.add hb;
variant.add hb;
@@ -630,10 +634,15 @@ let make_panel (main_ui:main_window_extension_points) =
| Property.IPLemma _ -> lemmas.get ()
| Property.IPComplete _ -> complete_disjoint.get ()
| Property.IPDisjoint _ -> complete_disjoint.get ()
- | Property.IPCodeAnnot(_,_,({annot_content = AAssert _} as ca)) ->
- (match Alarms.find ca with
- | None -> user_assertions.get ()
- | Some a -> rte.get () && active_alarm a)
+ | Property.IPCodeAnnot(_,_,({annot_content = AAssert (_, kind, _)} as ca)) ->
+ begin
+ match Alarms.find ca with
+ | Some a -> rte.get () && active_alarm a
+ | None ->
+ match kind with
+ | Assert -> user_assertions.get ()
+ | Check -> user_checks.get ()
+ end
| Property.IPCodeAnnot(_,_,{annot_content = AInvariant _}) ->
invariant.get ()
| Property.IPCodeAnnot(_,_,{annot_content = APragma p}) ->
--
GitLab