From 14dbc6931093aaece23b3748b7d58d3b19b101a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 8 Jan 2025 16:46:21 +0100
Subject: [PATCH] [server] Adds a libc column to the synchronized array of
properties.
---
src/plugins/server/kernel_properties.ml | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index bba21be7666..5dc5f899bcf 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))
--
GitLab