diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 3a878d27a67b268b3886b99e2547754294f9fbf8..d61e7eec939bc5495e058724901f21d606f8bf2e 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -20,6 +20,10 @@
(* *)
(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
+(* --- Property Type --- *)
+(* -------------------------------------------------------------------------- *)
+
open Cil_types
open Cil_datatype
@@ -145,6 +149,10 @@ and identified_property =
| IPGlobalInvariant of identified_global_invariant
| IPOther of string * other_loc
+(* -------------------------------------------------------------------------- *)
+(* --- Getters --- *)
+(* -------------------------------------------------------------------------- *)
+
let ki_of_e_loc = function
| ELContract _ | ELGlob -> Kglobal
| ELStmt (_,s) -> Kstmt s
@@ -291,6 +299,40 @@ let get_behavior = function
| IPGlobalInvariant _
| IPOther _ -> None
+(* -------------------------------------------------------------------------- *)
+(* --- Property Status --- *)
+(* -------------------------------------------------------------------------- *)
+
+let has_status_ext ((_,_,_,status,_) : Cil_types.acsl_extension) = status
+
+let has_status_ca = function
+ | AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAllocation _
+ | AAssigns _ -> true
+ | AExtended(_,_,e) -> has_status_ext e
+ | APragma _ -> false
+
+let has_status_pkind = function
+ | PKAssumes _ -> false
+ | PKEnsures _ | PKRequires _ | PKTerminates
+ -> true
+
+let rec has_status = function
+ | IPPredicate(pkind, _, _, _) -> has_status_pkind pkind
+ | IPExtended(_,e) -> has_status_ext e
+ | IPCodeAnnot(_,_, { annot_content = ca }) -> has_status_ca ca
+ | IPPropertyInstance(_,_,_,ip) -> has_status ip
+ | IPOther _ | IPReachable _
+ | IPAxiom _ | IPAxiomatic _ | IPBehavior _
+ | IPDisjoint _ | IPComplete _
+ | IPAssigns _ | IPFrom _
+ | IPAllocation _ | IPDecrease _ | IPLemma _
+ | IPTypeInvariant _ | IPGlobalInvariant _
+ -> true
+
+(* -------------------------------------------------------------------------- *)
+(* --- Datatype --- *)
+(* -------------------------------------------------------------------------- *)
+
include Datatype.Make_with_collections
(struct
@@ -1153,12 +1195,6 @@ end
(* --- Smart Constructors --- *)
(* -------------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Smart Constructors --- *)
-(* -------------------------------------------------------------------------- *)
-
-
let ip_other s le = IPOther(s,le)
let ip_reachable_stmt kf ki = IPReachable(Some kf, Kstmt ki, Before)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 61f401c12a113f0abec2eebf75176897db61c6cb..d951fa1afb61b2990baece699c57ff35cc83b462 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -93,7 +93,7 @@ type identified_predicate =
type program_point = Before | After
type identified_reachable = kernel_function option * kinstr * program_point
-(** [None, Kglobal] --> global property
+(** [None, Kglobal] --> global property
[None, Some ki] --> impossible
[Some kf, Kglobal] --> property of a function without code
[Some kf, Kstmt stmt] --> reachability of the given stmt (and the attached
@@ -113,7 +113,7 @@ type identified_extended = extended_loc * Cil_types.acsl_extension
and identified_axiomatic = string * identified_property list
-and identified_lemma =
+and identified_lemma =
string * logic_label list * string list * predicate * location
and identified_axiom = identified_lemma
@@ -156,7 +156,7 @@ val short_pretty: Format.formatter -> t -> unit
corresponding identified predicate when available)
reverting back to the full ACSL formula if it can't find one.
The name is not meant to uniquely identify the property.
- @since Neon-20140301
+ @since Neon-20140301
*)
(** @since Oxygen-20120901 *)
@@ -245,7 +245,7 @@ val ip_of_allocation:
@modify Aluminium-20160501 added active argument
*)
val ip_allocation_of_behavior:
- kernel_function -> kinstr -> active:string list ->
+ kernel_function -> kinstr -> active:string list ->
funbehavior -> identified_property option
(** Builds the corresponding IPAssigns.
@@ -403,13 +403,13 @@ val ip_property_instance:
identified_property -> identified_property
(** Builds an IPAxiom.
- @since Carbon-20110201
+ @since Carbon-20110201
@modify Oxygen-20120901 takes an identified_axiom instead of a string
*)
val ip_axiom: identified_axiom -> identified_property
(** Build an IPLemma.
- @since Nitrogen-20111001
+ @since Nitrogen-20111001
@modify Oxygen-20120901 takes an identified_lemma instead of a string
*)
val ip_lemma: identified_lemma -> identified_property
@@ -437,7 +437,7 @@ val ip_of_code_annot_single:
val ip_of_global_annotation: global_annotation -> identified_property list
(** @since Nitrogen-20111001 *)
-val ip_of_global_annotation_single:
+val ip_of_global_annotation_single:
global_annotation -> identified_property option
(** @since Nitrogen-20111001 *)
@@ -445,6 +445,11 @@ val ip_of_global_annotation_single:
(** {2 getters} *)
(**************************************************************************)
+val has_status: identified_property -> bool
+(** Does the property has a logical status (which may be Never_tried)?
+ False for pragma, assumes clauses and some ACSL extensions.
+ @since Frama-C+dev *)
+
val get_kinstr: identified_property -> kinstr
val get_kf: identified_property -> kernel_function option
val get_behavior: identified_property -> funbehavior option
@@ -462,7 +467,7 @@ val source: identified_property -> Filepath.position option
(**************************************************************************)
-(** @since Frama-C+dev deprecated old naming scheeme,
+(** @since Frama-C+dev deprecated old naming scheme,
to be removed in future versions. *)
module LegacyNames :
sig
@@ -479,12 +484,12 @@ sig
val get_prop_name_id: identified_property -> string
(** returns a unique name identifying the property.
- This name is built from the basename of the property.
+ This name is built from the basename of the property.
@modify Frama-C+dev new naming scheme, Cf. LegacyNames
*)
-
+
val get_prop_basename: ?truncate:int -> identified_property -> string
- (** returns the basename of the property.
+ (** returns the basename of the property.
@modify Frama-C+dev additional truncation parameter
*)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index f9e63b4bf3105741bb0bc4a65094994708e6930d..f74d088be78e5ef2a0162a07066e06fb9962a167 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -271,8 +271,9 @@ let filetree_selector
end
let pretty_predicate_status fmt p =
- let s = Property_status.get p in
- Format.fprintf fmt "Status: %a@." Property_status.pretty s
+ if Property.has_status p then
+ let s = Property_status.get p in
+ Format.fprintf fmt "Status: %a@." Property_status.pretty s
(* This is called when a localizable is selected in the pretty-printed source
buffer *)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 2fd3a11560a87d427867089367902ff83a3d26b3..a859ed50bd7e119fa26cbd6f9f7983e7400d82ef 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -752,13 +752,10 @@ let make_panel (main_ui:main_window_extension_points) =
Aka. "bullets" in left margin *)
let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
match localizable with
- | Pretty_source.PIP (Property.IPPredicate (Property.PKAssumes _,_,_,_)) ->
- (* Assumes clause do not get a bullet: there is nothing
- to prove about them.*)
- ()
| Pretty_source.PIP ppt ->
- Design.Feedback.mark
- buffer#buffer ~offset:start (Property_status.Feedback.get ppt)
+ if Property.has_status ppt then
+ Design.Feedback.mark
+ buffer#buffer ~offset:start (Property_status.Feedback.get ppt)
| Pretty_source.PStmt(_,({ skind=Instr(Call _| Local_init (_, ConsInit _, _)) } as stmt)) ->
let kfs = Statuses_by_call.all_functions_with_preconditions stmt in
(* We separate the consolidated statuses of the preconditions inside