From e7125985673916056914b772d13e479f68e35caf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Nov 2023 19:12:40 +0100
Subject: [PATCH] [server] fixed ip-other kinds
---
.../frama-c/kernel/api/properties/index.ts | 2 ++
src/plugins/server/kernel_properties.ml | 20 ++-----------------
src/plugins/server/kernel_properties.mli | 8 --------
3 files changed, 4 insertions(+), 26 deletions(-)
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index 7103e001bbf..da82af1774b 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -140,6 +140,8 @@ export enum propKind {
check_lemma = 'check_lemma',
/** ACSL extension */
extension = 'extension',
+ /** Generic Property */
+ generic = 'generic',
}
/** Decoder for `propKind` */
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index dfcb841190c..78c179100d9 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -84,15 +84,7 @@ struct
let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
let t_ext = t_kind "extension" "ACSL extension"
-
- let p_ext = Enum.prefix kinds ~name:"ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL extension `<clause>`")
-
- let p_loop_ext = Enum.prefix kinds ~name:"loop_ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL loop extension `loop <clause>`")
-
- let p_other = Enum.prefix kinds ~name:"prop" ~var:"<prop>"
- ~descr:(Md.plain "Plugin Specific properties")
+ let t_other = t_kind "generic" "Generic Property"
open Property
@@ -138,7 +130,7 @@ struct
| IPPropertyInstance _ -> t_instance
| IPTypeInvariant _ -> t_type_invariant
| IPGlobalInvariant _ -> t_global_invariant
- | IPOther { io_name } -> Enum.instance p_other io_name
+ | IPOther _ -> t_other
let () = Enum.set_lookup kinds lookup
let data = Request.dictionary ~package
@@ -149,14 +141,6 @@ struct
include (val data : S with type t = Property.t)
end
-let register_propkind ~name ~kind ?label ~descr () =
- let open PropKind in
- let prefix = match kind with
- | `Clause -> p_ext
- | `Loop -> p_loop_ext
- | `Other -> p_other
- in ignore @@ Enum.extends prefix ~name ?label ~descr
-
(* -------------------------------------------------------------------------- *)
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.mli b/src/plugins/server/kernel_properties.mli
index 9d6a044eb61..3a828a88139 100644
--- a/src/plugins/server/kernel_properties.mli
+++ b/src/plugins/server/kernel_properties.mli
@@ -22,14 +22,6 @@
(** Kernel Property Status *)
-(** Documentation of ACSL extensions for [propkind] server data. *)
-val register_propkind :
- name:string ->
- kind:[`Clause | `Loop | `Other] ->
- ?label:Markdown.text ->
- descr:Markdown.text ->
- unit -> unit
-
(** Trigger a full reload for the table of property status. *)
val reload : unit -> unit
--
GitLab