diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts
index 319a69f78ed8167bb05221dfa84694d8be113315..dc1398e2ab95606276eb5ab92a4475f1ffbe3299 100644
--- a/ivette/api/generated/kernel/ast/index.ts
+++ b/ivette/api/generated/kernel/ast/index.ts
@@ -281,13 +281,13 @@ export interface functionsData {
/** Signature */
signature: string;
/** Is the function the main entry point */
- main: boolean;
+ main?: boolean;
/** Is the function defined? */
- defined: boolean;
+ defined?: boolean;
/** Is the function from the Frama-C stdlib? */
- stdlib: boolean;
+ stdlib?: boolean;
/** Is the function a Frama-C builtin? */
- builtin: boolean;
+ builtin?: boolean;
/** Has the function been analyzed by Eva */
eva_analyzed?: boolean;
}
@@ -299,10 +299,10 @@ export const jFunctionsData: Json.Loose<functionsData> =
'#functions expected'),
name: Json.jFail(Json.jString,'String expected'),
signature: Json.jFail(Json.jString,'String expected'),
- main: Json.jFail(Json.jBoolean,'Boolean expected'),
- defined: Json.jFail(Json.jBoolean,'Boolean expected'),
- stdlib: Json.jFail(Json.jBoolean,'Boolean expected'),
- builtin: Json.jFail(Json.jBoolean,'Boolean expected'),
+ main: Json.jBoolean,
+ defined: Json.jBoolean,
+ stdlib: Json.jBoolean,
+ builtin: Json.jBoolean,
eva_analyzed: Json.jBoolean,
});
@@ -314,15 +314,15 @@ export const jFunctionsDataSafe: Json.Safe<functionsData> =
export const byFunctionsData: Compare.Order<functionsData> =
Compare.byFields
<{ key: Json.key<'#functions'>, name: string, signature: string,
- main: boolean, defined: boolean, stdlib: boolean, builtin: boolean,
- eva_analyzed?: boolean }>({
+ main?: boolean, defined?: boolean, stdlib?: boolean,
+ builtin?: boolean, eva_analyzed?: boolean }>({
key: Compare.string,
name: Compare.alpha,
signature: Compare.string,
- main: Compare.boolean,
- defined: Compare.boolean,
- stdlib: Compare.boolean,
- builtin: Compare.boolean,
+ main: Compare.defined(Compare.boolean),
+ defined: Compare.defined(Compare.boolean),
+ stdlib: Compare.defined(Compare.boolean),
+ builtin: Compare.defined(Compare.boolean),
eva_analyzed: Compare.defined(Compare.boolean),
});
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index cb1c70324132e281a16cb32f20cf01fa9100fcb5..6dd76c134789afb91c5d3db8ef6eb3213da42721 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -371,8 +371,8 @@ struct
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 is_eva_analyzed kf =
+ if Db.Value.is_computed () then !Db.Value.is_called kf else false
let iter f =
Globals.Functions.iter
@@ -397,27 +397,32 @@ struct
~name:"main"
~descr:(Md.plain "Is the function the main entry point")
~data:(module Data.Jbool)
+ ~default:false
~get:Kernel_function.is_entry_point;
States.column model
~name:"defined"
~descr:(Md.plain "Is the function defined?")
~data:(module Data.Jbool)
+ ~default:false
~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)
+ ~default:false
~get:is_stdlib;
States.column model
~name:"builtin"
~descr:(Md.plain "Is the function a Frama-C builtin?")
~data:(module Data.Jbool)
+ ~default:false
~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;
+ ~data:(module Data.Jbool)
+ ~default:false
+ ~get:is_eva_analyzed;
States.register_array model
~package ~key
~name:"functions"
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index 5b172c2d4efdfc5e9a25b7839fa276761fb0766b..f9ae51a5b8acb166d074e7b2dc88b1624e90c1b1 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -92,23 +92,55 @@ let register_state (type a) ~package ~name ~descr
(* --- Model Signature --- *)
(* -------------------------------------------------------------------------- *)
-type 'a column = Package.fieldInfo * ('a -> json)
+type 'a column = Package.fieldInfo * ('a -> json option)
type 'a model = 'a column list ref
let model () = ref []
+let mkfield (model : 'a model) fd (js : 'a -> json option) =
+ let open Package in
+ let name = fd.fd_name in
+ if List.exists (fun (fd,_) -> fd.fd_name = name) !model then
+ raise (Invalid_argument "Server.States.column: duplicate name") ;
+ model := (fd , js) :: !model
+
let column (type a b) ~name ~descr
- ~(data: b Request.output) ~(get : a -> b) (model : a model) =
+ ~(data: b Request.output)
+ ~(get : a -> b)
+ ?(default: b option)
+ (model : a model) =
+ let module D = (val data) in
+ match default with
+ | None ->
+ let fd = Package.{
+ fd_name = name ;
+ fd_type = D.jtype ;
+ fd_descr = descr ;
+ } in
+ mkfield model fd (fun a -> Some (D.to_json (get a)))
+ | Some d ->
+ let fd = Package.{
+ fd_name = name ;
+ fd_type = Joption D.jtype ;
+ fd_descr = descr ;
+ } in
+ mkfield model fd (fun a ->
+ let v = get a in
+ if v = d then None else Some (D.to_json v)
+ )
+
+let option (type a b) ~name ~descr
+ ~(data: b Request.output) ~(get : a -> b option) (model : a model) =
let module D = (val data) in
- if List.exists (fun (fd,_) -> fd.Package.fd_name = name) !model then
- raise (Invalid_argument "Server.States.column: duplicate name") ;
let fd = Package.{
fd_name = name ;
- fd_type = D.jtype ;
+ fd_type = Joption D.jtype ;
fd_descr = descr ;
} in
- model := (fd , fun a -> D.to_json (get a)) :: !model
+ mkfield model fd (fun a -> match get a with
+ | None -> None
+ | Some b -> Some (D.to_json b))
module Kmap = Map.Make(String)
@@ -127,7 +159,7 @@ type 'a array = {
fkey : string ;
key : 'a -> string ;
iter : ('a -> unit) -> unit ;
- getter : (string * ('a -> json)) list ;
+ getter : (string * ('a -> json option)) list ;
(* [LC+JS]
The two following fields allow to keep an array in sync
with the current project and still have a polymorphic data type. *)
@@ -206,8 +238,9 @@ type buffer = {
let add_entry buffer cols fkey key v =
let fjs = List.fold_left (fun fjs (fd,to_json) ->
- try (fd , to_json v) :: fjs
- with Not_found -> fjs
+ match to_json v with
+ | Some js -> (fd , js) :: fjs
+ | None | exception Not_found -> fjs
) [] cols in
let row = (fkey, `String key) :: fjs in
buffer.updated <- `Assoc row :: buffer.updated ;
@@ -267,7 +300,7 @@ let register_array ~package ~name ~descr ~key
?(add_update_hook : 'a callback option)
?(add_remove_hook : 'a callback option)
?(add_reload_hook : unit callback option)
- model =
+ (model : 'a model) =
let open Markdown in
let href = link ~name () in
let columns = List.rev !model in
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
index 3e2c681cb406e8b08cf75a0e218871525f3a9967..a75c6c76c8776b067e39b4544c66198d3424fe89 100644
--- a/src/plugins/server/states.mli
+++ b/src/plugins/server/states.mli
@@ -76,12 +76,23 @@ type 'a model (** Columns array model *)
val model : unit -> 'a model
(** Populate an array model with a new field.
- Columns with name `"id"` and `"_index"` are reserved for internal use. *)
+ If a [~default] value is given, the field becomes optional and
+ the field is omitted when equal to the default value (compared with [=]).
+*)
val column :
name:string ->
descr:Markdown.text ->
data:('b Request.output) ->
get:('a -> 'b) ->
+ ?default:'b ->
+ 'a model -> unit
+
+(** Populate an array model with a new optional field. *)
+val option :
+ name:string ->
+ descr:Markdown.text ->
+ data:('b Request.output) ->
+ get:('a -> 'b option) ->
'a model -> unit
(** Synchronized array state. *)
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 2738c8e311a532572d29fa115ddb9228aa04998f..3dc3730f8f4b2707777bde129a6916dcb1f94d84 100644
--- a/src/plugins/server/tests/batch/oracle/ast_services.out.json
+++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json
@@ -7,19 +7,13 @@
"key": "kf#24",
"name": "g",
"signature": "int g(int y);",
- "defined": true,
- "stdlib": false,
- "builtin": false,
- "eva_analyzed": null
+ "defined": true
},
{
"key": "kf#20",
"name": "f",
"signature": "int f(int x);",
- "defined": true,
- "stdlib": false,
- "builtin": false,
- "eva_analyzed": null
+ "defined": true
}
],
"removed": [],