diff --git a/Makefile b/Makefile
index 70092c7cb3418f552d685b555464635837b4c83a..c3c3ecb3c413faad978858ca4b1b5bf5c9eeb0ce 100644
--- a/Makefile
+++ b/Makefile
@@ -427,6 +427,7 @@ LIB_CMO =\
src/libraries/datatype/type \
src/libraries/datatype/descr \
src/libraries/utils/filepath \
+ src/libraries/utils/sanitizer \
src/libraries/utils/pretty_utils \
src/libraries/utils/hook \
src/libraries/utils/bag \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 509d0627ae8b5724d772b34288850461b48a0cf7..5a010a2dce7f7db95e4f793f254d6f959aa9862c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -672,6 +672,8 @@ src/libraries/utils/rgmap.ml: CEA_LGPL
src/libraries/utils/rgmap.mli: CEA_LGPL
src/libraries/utils/rich_text.ml: CEA_LGPL
src/libraries/utils/rich_text.mli: CEA_LGPL
+src/libraries/utils/sanitizer.ml: CEA_LGPL
+src/libraries/utils/sanitizer.mli: CEA_LGPL
src/libraries/utils/task.ml: CEA_LGPL
src/libraries/utils/task.mli: CEA_LGPL
src/libraries/utils/unicode.ml: CEA_LGPL
@@ -989,8 +991,6 @@ src/plugins/report/csv.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/csv.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/dump.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/dump.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/property_names.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/report/property_names.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/report_parameters.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index c1b6a0334b9cb81cd722393f7c152557537f3801..d56b9d6d1a3bb895f7b9c4df880a01599e82a7b9 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -764,7 +764,14 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string s
pp_other_loc ol
-module Names = struct
+(* -------------------------------------------------------------------------- *)
+(* --- Legacy Property Names --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Shall be deprecated *)
+module LegacyNames =
+struct
+
module NamesTbl =
State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
@@ -949,19 +956,200 @@ module Names = struct
IndexTbl.add ip unique_name ;
unique_name
-(*
- (** force computation of the unique name identifying the property *)
- let make_prop_name_id ip =
- ignore (get_prop_name_id ip)
+end
- let remove_prop_name_id ip =
+(* -------------------------------------------------------------------------- *)
+(* --- Property Names --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Names =
+struct
+
+ open Cil_types
+
+ type part =
+ | B of behavior
+ | K of kernel_function
+ | A of string
+ | I of identified_predicate
+ | P of predicate
+ | T of term
+ | S of stmt
+
+ let add_part buffer = function
+ | B bhv ->
+ if not (Cil.is_default_behavior bhv)
+ then Sanitizer.add_string buffer bhv.b_name
+ | K kf -> Sanitizer.add_string buffer (Kernel_function.get_name kf)
+ | A msg -> Sanitizer.add_string buffer msg
+ | S stmt -> Sanitizer.add_string buffer (Printf.sprintf "s%d" stmt.sid)
+ | I { ip_content = { pred_name = a } }
+ | P { pred_name = a } | T { term_name = a } -> Sanitizer.add_list buffer a
+
+ let rec add_parts buffer = function
+ | [] -> ()
+ | p::ps ->
+ let open Sanitizer in
+ add_part buffer p ; add_sep buffer ; add_parts buffer ps
+
+ let rec parts_of_property ip : part list =
+ match ip with
+ | IPBehavior(kf,Kglobal,_,bhv) ->
+ [ K kf ; B bhv ]
+ | IPBehavior(kf,Kstmt s,_,bhv) ->
+ [ K kf ; B bhv ; S s ]
+
+ | IPPredicate (PKAssumes bhv,kf,_,ip) ->
+ [ K kf ; B bhv ; A "assumes" ; I ip ]
+ | IPPredicate (PKRequires bhv,kf,_,ip) ->
+ [ K kf ; B bhv ; A "requires" ; I ip ]
+ | IPPredicate (PKEnsures(bhv,Normal),kf,_,ip) ->
+ [ K kf ; B bhv ; A "ensures" ; I ip ]
+ | IPPredicate (PKEnsures(bhv,Exits),kf,_,ip) ->
+ [ K kf ; B bhv ; A "exits" ; I ip ]
+ | IPPredicate (PKEnsures(bhv,Breaks),kf,_,ip) ->
+ [ K kf ; B bhv ; A "breaks" ; I ip ]
+ | IPPredicate (PKEnsures(bhv,Continues),kf,_,ip) ->
+ [ K kf ; B bhv ; A "continues" ; I ip ]
+ | IPPredicate (PKEnsures(bhv,Returns),kf,_,ip) ->
+ [ K kf ; B bhv ; A "returns" ; I ip ]
+ | IPPredicate (PKTerminates,kf,_,ip) ->
+ [ K kf ; A "terminates" ; I ip ]
+
+ | IPAllocation(kf,_,Id_contract(_,bhv),_) ->
+ [ K kf ; B bhv ; A "allocates" ]
+ | IPAllocation(kf,_,Id_loop _,_) ->
+ [ K kf ; A "loop_allocates" ]
+
+ | IPAssigns(kf,_,Id_contract(_,bhv),_) ->
+ [ K kf ; B bhv ; A "assigns" ]
+
+ | IPAssigns(kf,_,Id_loop _,_) ->
+ [ K kf ; A "loop_assigns" ]
+
+ | IPFrom(kf,_,Id_contract(_,bhv),_) ->
+ [ K kf ; B bhv ; A "assigns_from" ]
+
+ | IPFrom(kf,_,Id_loop _,_) ->
+ [ K kf ; A "loop_assigns_from" ]
+
+ | IPDecrease (kf,_,None,_) ->
+ [ K kf ; A "variant" ]
+
+ | IPDecrease (kf,_,Some _,_) ->
+ [ K kf ; A "loop_variant" ]
+
+ | IPCodeAnnot (kf,stmt, { annot_content = AStmtSpec _ } ) ->
+ [ K kf ; A "contract" ; S stmt ]
+
+ | IPCodeAnnot (kf,stmt, { annot_content = APragma _ } ) ->
+ [ K kf ; A "pragma" ; S stmt ]
+
+ | IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_)) } )
+ -> [ K kf ; A clause ; S stmt ]
+
+ | IPCodeAnnot (kf,_, { annot_content = AAssert(_,p) } ) ->
+ [K kf ; A "assert" ; P p ]
+ | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,true,p) } ) ->
+ [K kf ; A "loop_invariant" ; P p ]
+ | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,false,p) } ) ->
+ [K kf ; A "invariant" ; P p ]
+ | IPCodeAnnot (kf,_, { annot_content = AVariant(e,_) } ) ->
+ [K kf ; A "loop_variant" ; T e ]
+ | IPCodeAnnot (kf,_, { annot_content = AAssigns _ } ) ->
+ [K kf ; A "loop_assigns" ]
+ | IPCodeAnnot (kf,_, { annot_content = AAllocation _ } ) ->
+ [K kf ; A "loop_allocates" ]
+
+ | IPComplete (kf,_,_,cs) ->
+ (K kf :: A "complete" :: List.map (fun a -> A a) cs)
+ | IPDisjoint(kf,_,_,cs) ->
+ (K kf :: A "disjoint" :: List.map (fun a -> A a) cs)
+
+ | IPReachable (None, _, _) -> []
+ | IPReachable (Some kf,Kglobal,Before) ->
+ [ K kf ; A "reachable" ]
+ | IPReachable (Some kf,Kglobal,After) ->
+ [ K kf ; A "reachable_post" ]
+ | IPReachable (Some kf,Kstmt s,Before) ->
+ [ K kf ; S s ; A "reachable" ]
+ | IPReachable (Some kf,Kstmt s,After) ->
+ [ K kf ; S s ; A "reachable_after" ]
+
+ | IPAxiomatic _
+ | IPAxiom _ -> []
+ | IPLemma(name,_,_,p,_) ->
+ [ A "lemma" ; A name ; P p ]
+
+ | IPTypeInvariant(name,_,_,_)
+ | IPGlobalInvariant(name,_,_) ->
+ [ A "invariant" ; A name ]
+
+ | IPOther(name,OLGlob _) -> [ A name ]
+ | IPOther(name,OLContract kf) -> [ K kf ; A name ]
+ | IPOther(name,OLStmt(kf,s)) -> [ K kf ; S s ; A name ]
+
+ | IPExtended(ELGlob,(_,name,_,_)) -> [ A name ]
+ | IPExtended(ELContract(kf),(_,name,_,_)) -> [ K kf ; A name ]
+ | IPExtended(ELStmt(kf,s),(_,name,_,_)) -> [ K kf ; S s ; A name ]
+
+ | IPPropertyInstance (_, _, _, ip) -> parts_of_property ip
+
+ let get_prop_basename ?truncate ip =
+ let buffer =
+ match truncate with
+ | None -> Sanitizer.create ~truncate:false 20
+ | Some n -> Sanitizer.create ~truncate:true n
+ in
+ add_parts buffer (parts_of_property ip) ;
+ Sanitizer.contents buffer
+
+ (* Numerotation of properties with same basename *)
+ module NamesTbl =
+ State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
+ (struct
+ let name = "Property.Names.NamesTbl"
+ let dependencies = [ ]
+ let size = 97
+ end)
+
+ (* Computed name of properties *)
+ module IndexTbl = (* indexed by Property *)
+ State_builder.Hashtbl(Hashtbl)(Datatype.String)
+ (struct
+ let name = "Property.Names.IndexTbl"
+ let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
+ let size = 97
+ end)
+
+ let self = IndexTbl.self
+
+ let compute_name_id basename =
try
- ignore (IndexTbl.find ip);
- IndexTbl.remove ip
- with Not_found -> ()
-*)
+ let speed_up_start = NamesTbl.find basename in
+ (* this basename is already reserved *)
+ let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
+ in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
+ unique_name
+ with Not_found -> (* first time that basename is reserved *)
+ NamesTbl.add basename 2 ;
+ basename
+
+ let get_prop_name_id ip =
+ try IndexTbl.find ip
+ with Not_found -> (* first time we are asking for a name for that [ip] *)
+ let basename = get_prop_basename ip in
+ let unique_name = compute_name_id basename in
+ IndexTbl.add ip unique_name ;
+ unique_name
+
end
+(* -------------------------------------------------------------------------- *)
+(* --- 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 254ef04db0c75f395bc00644ebbbd356e9bc2910..3cd66eeffdc9209e1215f21ae0367899b8ddf383 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -461,23 +461,32 @@ val source: identified_property -> Filepath.position option
(** {2 names} *)
(**************************************************************************)
+
+(** @since Frama-C+dev deprecated old naming scheeme,
+ to be removed in future versions. *)
+module LegacyNames :
+sig
+ val self: State.t
+ val get_prop_basename: identified_property -> string
+ val get_prop_name_id: identified_property -> string
+end
+
(** @since Oxygen-20120901 *)
-module Names: sig
+module Names :
+sig
val self: State.t
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. *)
-
- val get_prop_basename: identified_property -> string
- (** returns 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 reserve_name_id: string -> string
-(** returns the name that should be returned by the function
- [get_prop_name_id] if the given property has [name] as basename. That name
- is reserved so that [get_prop_name_id prop] can never return an identical
- name. *)
+ val get_prop_basename: ?truncate:int -> identified_property -> string
+ (** returns the basename of the property.
+ @modify Frama-C+dev additional truncation parameter
+ *)
end
diff --git a/src/libraries/utils/sanitizer.ml b/src/libraries/utils/sanitizer.ml
new file mode 100644
index 0000000000000000000000000000000000000000..25c9bb0ec739a7baf9311413007bc47bb694a95f
--- /dev/null
+++ b/src/libraries/utils/sanitizer.ml
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Sanitizer --- *)
+(* -------------------------------------------------------------------------- *)
+
+(*
+ Keeps only alphanumerical characters,
+ remove consecutive, trailing and leading `_`
+*)
+
+type state = START | SEP | CHAR | TRUNCATE
+
+type buffer = {
+ content : Buffer.t ;
+ truncate : int ;
+ mutable lastsep : int ;
+ mutable state : state ;
+}
+
+let create ?(truncate=false) n = {
+ content = Buffer.create n ;
+ truncate = if truncate then n else max_int ;
+ lastsep = 0 ;
+ state = START ;
+}
+
+let clear buffer =
+ begin
+ Buffer.clear buffer.content ;
+ buffer.state <- START ;
+ buffer.lastsep <- 0 ;
+ end
+
+let add_sep buffer =
+ if buffer.state = CHAR then
+ let offset = Buffer.length buffer.content in
+ if offset < buffer.truncate then
+ begin
+ buffer.state <- SEP ;
+ buffer.lastsep <- offset ;
+ end
+ else
+ begin
+ buffer.state <- TRUNCATE ;
+ (* TODO [OCaml 4.05] Buffer.truncate buffer.content buffer.lastsep ; *)
+ end
+
+let add_char buffer = function
+ | ('a'..'z' | 'A'..'Z' | '0'..'9') as c ->
+ begin
+ match buffer.state with
+ | START ->
+ Buffer.add_char buffer.content c ;
+ buffer.state <- CHAR
+ | SEP ->
+ Buffer.add_char buffer.content '_' ;
+ Buffer.add_char buffer.content c ;
+ buffer.state <- CHAR
+ | CHAR ->
+ Buffer.add_char buffer.content c
+ | TRUNCATE -> ()
+ end
+ | '_' -> add_sep buffer
+ | _ -> ()
+
+let add_string buffer s = String.iter (add_char buffer) s
+
+let rec add_list buffer = function
+ | [] -> ()
+ | p::ps -> add_string buffer p ; add_sep buffer ; add_list buffer ps
+
+let contents buffer =
+ (* TODO [OCaml 4.05] simply buffer contents if using Buffer.truncate *)
+ let s = Buffer.contents buffer.content in
+ if buffer.state = TRUNCATE then
+ String.sub s 0 buffer.lastsep
+ else s
diff --git a/src/plugins/report/property_names.mli b/src/libraries/utils/sanitizer.mli
similarity index 76%
rename from src/plugins/report/property_names.mli
rename to src/libraries/utils/sanitizer.mli
index 23a5f2ea7261f6c6f6c52f618a6cb48b4d963f7b..ea850a8587f0950630d3ad7d7d6838073de4f8f3 100644
--- a/src/plugins/report/property_names.mli
+++ b/src/libraries/utils/sanitizer.mli
@@ -20,20 +20,21 @@
(* *)
(**************************************************************************)
-open Cil_types
+(** {2 Sanitizer}
-type part =
- | B of behavior
- | K of kernel_function
- | A of string
- | I of identified_predicate
- | P of predicate
- | T of term
- | S of stmt
+ Keeps only alpha-numerical characters.
+ Separator ['_'] is allowed, but leading, trailing and consecutive
+ separators are removed.
+*)
-val is_name : string -> bool
-val join : string list -> string
+type buffer
-val string_of_part : part -> string
-val string_of_parts : part list -> string
-val parts_of_property : Property.t -> part list
+val create : ?truncate:bool -> int -> buffer
+val clear : buffer -> unit
+
+val add_sep : buffer -> unit (** Adds ['_'] character *)
+val add_char : buffer -> char -> unit
+val add_string : buffer -> string -> unit
+val add_list : buffer -> string list -> unit (** Separated with ['_'] *)
+
+val contents : buffer -> string
diff --git a/src/plugins/report/Makefile.in b/src/plugins/report/Makefile.in
index 6c6d41d7b0577e1a0fcbff0dea2f61e5745af3a7..c3464e1ebdd7c85ce5b42b63e9e562d102323439 100644
--- a/src/plugins/report/Makefile.in
+++ b/src/plugins/report/Makefile.in
@@ -36,7 +36,7 @@ endif
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_REPORT@
PLUGIN_NAME:=Report
-PLUGIN_CMO:= report_parameters scan dump csv property_names classify register
+PLUGIN_CMO:= report_parameters scan dump csv classify register
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
#PLUGIN_NO_DEFAULT_TEST:=no
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index d7844aa7a51d29087ca33fe2802617c21bf7de2e..e92506e697f099b820ed2632f62330357d604657 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -74,7 +74,7 @@ let errors = {
type props = {
ps_name : string ;
ps_rules : rule Queue.t ;
- ps_action : (unit -> string) ;
+ ps_action : (unit -> string) ; (* plugin option getter *)
}
let props ps_name ps_action =
@@ -408,19 +408,50 @@ let pending f pending =
(fun _ ips -> Property.Set.iter f ips) m)
pending
+let rec monitored_property ip =
+ let open Cil_types in
+ let open Property in
+ match ip with
+ | IPBehavior _ -> false
+ | IPPredicate (PKAssumes _,_,_,_) -> false
+ | IPPredicate (PKRequires _,_,_,_) -> true
+ | IPPredicate (PKEnsures _,_,_,_) -> true
+ | IPPredicate (PKTerminates,_,_,_) -> true
+ | IPAllocation(_,_,_,_) -> true
+ | IPAssigns(_,_,_,_) -> true
+ | IPFrom(_,_,_,_) -> true
+ | IPDecrease (_,_,_,_) -> true
+ | IPCodeAnnot (_,_, { annot_content = AStmtSpec _ } ) -> false
+ | IPCodeAnnot (_,_, { annot_content = APragma _ } ) -> false
+ | IPCodeAnnot (_,_, { annot_content = AExtended _ } ) -> true
+ | IPCodeAnnot (_,_, { annot_content = AAssert _ } ) -> true
+ | IPCodeAnnot (_,_, { annot_content = AInvariant _ } ) -> true
+ | IPCodeAnnot (_,_, { annot_content = AVariant _ } ) -> true
+ | IPCodeAnnot (_,_, { annot_content = AAssigns _ } ) -> true
+ | IPCodeAnnot (_,_, { annot_content = AAllocation _ } ) -> true
+ | IPComplete (_,_,_,_) -> true
+ | IPDisjoint(_,_,_,_) -> true
+ | IPReachable (None,_,_) -> false
+ | IPReachable (Some _,_,_) -> true
+ | IPAxiomatic _ | IPAxiom _ -> false
+ | IPLemma(_,_,_,_,_) -> true
+ | IPTypeInvariant(_,_,_,_) | IPGlobalInvariant(_,_,_) -> true
+ | IPOther(_,_) -> true
+ | IPExtended _ -> true
+ | IPPropertyInstance (_, _, _, ip) -> monitored_property ip
+
let monitor_status properties ip =
- let ps = Property_names.parts_of_property ip in
- if ps = [] then () else
- let msg = Property_names.string_of_parts ps in
+ if monitored_property ip then
+ let name = Property.Names.get_prop_name_id ip in
let lookup = find properties.ps_rules in
let source = Property.source ip in
let unclassified () =
let e_id = "unclassified." ^ properties.ps_name in
- let e_title = msg in
+ let e_title = name in
let e_action = properties.ps_action () |> action in
let e_descr = T.String.capitalize_ascii properties.ps_name ^ " status" in
{ unclassified with e_id ; e_action ; e_title ; e_descr }
- in monitor ~lookup ~category:[] ~msg ~source unclassified
+ in monitor ~lookup ~category:[] ~msg:name ~source unclassified
let monitor_property pool push ip =
begin
diff --git a/src/plugins/report/property_names.ml b/src/plugins/report/property_names.ml
deleted file mode 100644
index dd0ffca34ea836e827e830b5a6c98ebe9277e260..0000000000000000000000000000000000000000
--- a/src/plugins/report/property_names.ml
+++ /dev/null
@@ -1,131 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2018 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-type part =
- | B of behavior
- | K of kernel_function
- | A of string
- | I of identified_predicate
- | P of predicate
- | T of term
- | S of stmt
-
-let is_name s = s <> "" && s <> "_"
-let join ps = String.concat "_" (List.filter is_name ps)
-
-let string_of_part = function
- | B bhv -> if Cil.is_default_behavior bhv then "" else bhv.b_name
- | K kf -> Kernel_function.get_name kf
- | A msg -> msg
- | S stmt -> Printf.sprintf "s%d" stmt.sid
- | I { ip_content = { pred_name = a } }
- | P { pred_name = a } | T { term_name = a } -> join a
-
-let string_of_parts ps = join (List.map string_of_part ps)
-
-let rec parts_of_property ip : part list =
- let open Property in
- match ip with
- | IPBehavior _ -> []
- | IPPredicate (PKAssumes _,_,_,_) -> []
- | IPPredicate (PKRequires bhv,kf,_,ip) ->
- [ K kf ; B bhv ; A "requires" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Normal),kf,_,ip) ->
- [ K kf ; B bhv ; A "ensures" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Exits),kf,_,ip) ->
- [ K kf ; B bhv ; A "exits" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Breaks),kf,_,ip) ->
- [ K kf ; B bhv ; A "breaks" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Continues),kf,_,ip) ->
- [ K kf ; B bhv ; A "continues" ; I ip ]
- | IPPredicate (PKEnsures(bhv,Returns),kf,_,ip) ->
- [ K kf ; B bhv ; A "returns" ; I ip ]
- | IPPredicate (PKTerminates,kf,_,ip) ->
- [ K kf ; A "terminates" ; I ip ]
-
- | IPAllocation(kf,_,Id_contract(_,bhv),_) ->
- [ K kf ; B bhv ; A "allocates" ]
- | IPAllocation(kf,_,Id_loop _,_) ->
- [ K kf ; A "loop_allocates" ]
-
- | IPAssigns(kf,_,Id_contract(_,bhv),_) ->
- [ K kf ; B bhv ; A "assigns" ]
-
- | IPAssigns(kf,_,Id_loop _,_) ->
- [ K kf ; A "loop_assigns" ]
-
- | IPFrom(kf,_,Id_contract(_,bhv),_) ->
- [ K kf ; B bhv ; A "assigns_from" ]
-
- | IPFrom(kf,_,Id_loop _,_) ->
- [ K kf ; A "loop_assigns_from" ]
-
- | IPDecrease (kf,_,None,_) ->
- [ K kf ; A "variant" ]
-
- | IPDecrease (kf,_,Some _,_) ->
- [ K kf ; A "loop_variant" ]
-
- | IPCodeAnnot (_,_, { annot_content = AStmtSpec _ } ) -> []
- | IPCodeAnnot (_,_, { annot_content = APragma _ | AExtended _ } ) -> []
- | IPCodeAnnot (kf,_, { annot_content = AAssert(_,p) } ) ->
- [K kf ; A "assert" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,true,p) } ) ->
- [K kf ; A "loop_invariant" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,false,p) } ) ->
- [K kf ; A "invariant" ; P p ]
- | IPCodeAnnot (kf,_, { annot_content = AVariant(e,_) } ) ->
- [K kf ; A "loop_variant" ; T e ]
- | IPCodeAnnot (kf,_, { annot_content = AAssigns _ } ) ->
- [K kf ; A "loop_assigns" ]
- | IPCodeAnnot (kf,_, { annot_content = AAllocation _ } ) ->
- [K kf ; A "loop_allocates" ]
-
- | IPComplete (kf,_,_,cs) ->
- (K kf :: A "complete" :: List.map (fun a -> A a) cs)
- | IPDisjoint(kf,_,_,cs) ->
- (K kf :: A "disjoint" :: List.map (fun a -> A a) cs)
-
- | IPReachable (None, _, _) -> []
- | IPReachable (Some kf,Kglobal,Before) ->
- [ K kf ; A "reachable" ]
- | IPReachable (Some kf,Kglobal,After) ->
- [ K kf ; A "reachable_post" ]
- | IPReachable (Some kf,Kstmt s,Before) ->
- [ K kf ; S s ; A "reachable" ]
- | IPReachable (Some kf,Kstmt s,After) ->
- [ K kf ; S s ; A "reachable_after" ]
- | IPAxiomatic _ | IPAxiom _ -> []
- | IPLemma(name,_,_,_,_) -> [ A "lemma" ; A name ]
- | IPTypeInvariant(name,_,_,_)
- | IPGlobalInvariant(name,_,_) -> [ A "invariant" ; A name]
- | IPOther(name, OLContract kf) -> [ K kf ; A name ]
- | IPOther(name, OLStmt (kf, s)) -> [K kf; S s; A name]
- | IPOther(name,OLGlob _) -> [ A name ]
- | IPPropertyInstance (_, _, _, ip) -> parts_of_property ip
- | IPExtended(ELContract kf,(_,name,_,_)) -> [ K kf ; A name ]
- | IPExtended(ELStmt (kf, s),(_,name,_,_)) -> [ K kf ; S s ; A name ]
- | IPExtended(ELGlob, (_,name,_,_)) -> [ A name ]
-
-(**************************************************************************)
diff --git a/src/plugins/report/tests/report/oracle/classify.0.res.oracle b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
index 08e3a2f22246d9b0ce10e23016c15f9413fe8218..2d9f271aea5752a9bbc3037c9c42b90aac05b38e 100644
--- a/src/plugins/report/tests/report/oracle/classify.0.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
@@ -4,8 +4,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assign : Valid
-[wp] [Qed] Goal typed_f_post : Valid
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
[wp] Proved goals: 2 / 2
Qed: 2
[report] Classification
diff --git a/src/plugins/report/tests/report/oracle/classify.1.res.oracle b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
index 5dc01f6e288d62097d7aeb8bcff5de4b9a758aeb..9266851bb999c61aaf138053b920459d475fb73d 100644
--- a/src/plugins/report/tests/report/oracle/classify.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
@@ -5,8 +5,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assign : Valid
-[wp] [Qed] Goal typed_f_post : Valid
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
[wp] Proved goals: 2 / 2
Qed: 2
[report] Classification
diff --git a/src/plugins/report/tests/report/oracle/classify.2.res.oracle b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
index 0d4bf582b12dcdfdfcd194cce2b00f461d03f48b..8e0f90163361e74984979077ddaa1a85702be12e 100644
--- a/src/plugins/report/tests/report/oracle/classify.2.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
@@ -5,8 +5,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assign : Valid
-[wp] [Qed] Goal typed_f_post : Valid
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
[wp] Proved goals: 2 / 2
Qed: 2
[report] Classification
diff --git a/src/plugins/report/tests/report/oracle/classify.3.res.oracle b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
index e41bd323df63f3913f41fe42d9e7ac2fdf50227b..5fab349a04e38664af8b21b15febbb573588c6c7 100644
--- a/src/plugins/report/tests/report/oracle/classify.3.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
@@ -6,8 +6,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assign : Valid
-[wp] [Qed] Goal typed_f_post : Valid
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
[wp] Proved goals: 2 / 2
Qed: 2
[report] Classification
diff --git a/src/plugins/report/tests/report/oracle/classify.4.res.oracle b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
index 70e846d1bf34b306e607d9579046c28735bb18d0..4fe970e76ac2d9a5d2c965d22a6f185ebaeb2f95 100644
--- a/src/plugins/report/tests/report/oracle/classify.4.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
@@ -6,8 +6,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_f_assign : Valid
-[wp] [Qed] Goal typed_f_post : Valid
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
[wp] Proved goals: 2 / 2
Qed: 2
[report] Classification
diff --git a/src/plugins/report/tests/report/oracle/classify.5.res.oracle b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
index da6f9a37f4f68fd31782b82428ff795cf9ea9ebc..fe7d84466c0e64effca171af82723994cecf7759 100644
--- a/src/plugins/report/tests/report/oracle/classify.5.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
@@ -5,8 +5,8 @@
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] Goal typed_f_post : not tried
-[wp] Goal typed_f_assign : trivial
+[wp] Goal typed_f_ensures : not tried
+[wp] Goal typed_f_assigns : trivial
[report] Classification
[report] Output tests/report/result/classified.5.json
[report] Reviews : 2