diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml index bba21be7666385e9fa90760540a5d5b2eccdf427..5dc5f899bcfdc55a67f67c194775fde36694d64b 100644 --- a/src/plugins/server/kernel_properties.ml +++ b/src/plugins/server/kernel_properties.ml @@ -248,6 +248,13 @@ let find_alarm = function | Property.IPCodeAnnot annot -> Alarms.find annot.ica_ca | _ -> None +let is_libc ip = + match Property.source ip with + | None -> false + | Some position -> + let libc_path = Kernel.Share.get_dir "libc" in + Filepath.is_relative ~base_name:libc_path position.pos_path + let model = States.model () let () = States.column model ~name:"descr" @@ -289,6 +296,11 @@ let () = States.column model ~name:"source" ~data:(module Kernel_ast.Position) ~get:(fun ip -> Property.location ip |> fst) +let () = States.column model ~name:"libc" + ~descr:(Md.plain "Is the property from the Frama-C libc?") + ~data:(module Jbool) + ~get:is_libc + let () = States.column model ~name:"alarm" ~descr:(Md.plain "Alarm name (if the property is an alarm)") ~data:(module Joption(Jstring))