From 938be45146acaf739e8086d9f0918dc4169c7fe7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 25 Nov 2020 11:07:51 +0100
Subject: [PATCH] [server] Kernel AST: adds new columns to the synchronized
arrays of functions.
Do not include builtins Frama_C_show_each & cie in the array.
---
src/plugins/server/kernel_ast.ml | 38 ++++++++++++++++++-
.../tests/batch/oracle/ast_services.out.json | 20 +++++++++-
2 files changed, 55 insertions(+), 3 deletions(-)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 832c1adce2b..2a5692d2dc7 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -354,6 +354,22 @@ struct
let global = Kernel_function.get_global kf in
Rich_text.to_string Printer_tag.pretty (PGlobal global)
+ let is_builtin kf = Cil.is_builtin (Kernel_function.get_vi kf)
+
+ let is_stdlib kf =
+ let vi = Kernel_function.get_vi kf in
+ Cil.hasAttribute "fc_stdlib" vi.vattr ||
+ Cil.hasAttribute "fc_stdlib_generated" vi.vattr
+
+ let is_analyzed kf =
+ if Db.Value.is_computed () then Some (!Db.Value.is_called kf) else None
+
+ let iter f =
+ Globals.Functions.iter
+ (fun kf ->
+ let name = Kernel_function.get_name kf in
+ if not (Ast_info.is_frama_c_builtin name) then f kf)
+
let array : kernel_function States.array =
begin
let model = States.model () in
@@ -367,11 +383,31 @@ struct
~descr:(Md.plain "Signature")
~data:(module Data.Jstring)
~get:signature ;
+ States.column model
+ ~name:"defined"
+ ~descr:(Md.plain "Is the function defined?")
+ ~data:(module Data.Jbool)
+ ~get:Kernel_function.is_definition;
+ States.column model
+ ~name:"stdlib"
+ ~descr:(Md.plain "Is the function from the Frama-C stdlib?")
+ ~data:(module Data.Jbool)
+ ~get:is_stdlib;
+ States.column model
+ ~name:"builtin"
+ ~descr:(Md.plain "Is the function a Frama-C builtin?")
+ ~data:(module Data.Jbool)
+ ~get:is_builtin;
+ States.column model
+ ~name:"eva_analyzed"
+ ~descr:(Md.plain "Has the function been analyzed by Eva")
+ ~data:(module Data.Joption (Data.Jbool))
+ ~get:is_analyzed;
States.register_array model
~package ~key
~name:"functions"
~descr:(Md.plain "AST Functions")
- ~iter:Globals.Functions.iter
+ ~iter
~add_reload_hook:Ast.add_hook_on_update ;
end
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json
index 865d7d9f0c0..2738c8e311a 100644
--- a/src/plugins/server/tests/batch/oracle/ast_services.out.json
+++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json
@@ -3,8 +3,24 @@
"id": "GET-1",
"data": {
"updated": [
- { "key": "kf#24", "name": "g", "signature": "int g(int y);" },
- { "key": "kf#20", "name": "f", "signature": "int f(int x);" }
+ {
+ "key": "kf#24",
+ "name": "g",
+ "signature": "int g(int y);",
+ "defined": true,
+ "stdlib": false,
+ "builtin": false,
+ "eva_analyzed": null
+ },
+ {
+ "key": "kf#20",
+ "name": "f",
+ "signature": "int f(int x);",
+ "defined": true,
+ "stdlib": false,
+ "builtin": false,
+ "eva_analyzed": null
+ }
],
"removed": [],
"reload": true,
--
GitLab