diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts index 7103e001bbf796b192369a4bbc6a9177ee19445d..da82af1774b8290511d55975a7f7a57716b1abee 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 dfcb841190cb37d092abcd887af7f6cc8586f625..78c179100d96b421ab445e4db6b558164252f1c9 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 9d6a044eb6188993058ea6d97ed43fb28165a2f1..3a828a88139363c9351b09c5809aeac692420a97 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