diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index d40b73e253e2c67e5d6008b605c902d0f13504b1..7fb10e1ae010fcb0ff9a99303d517545366841b2 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -31,10 +31,12 @@ import { alpha } from 'dome/data/compare';
import { Section, Item } from 'dome/frame/sidebars';
import { Button } from 'dome/controls/buttons';
import * as Toolbars from 'dome/frame/toolbars';
+import * as ArrayUtils from 'dome/data/arrays';
import * as States from 'frama-c/states';
-import { functions, functionsData } from 'frama-c/kernel/api/ast';
+import * as Kernel from 'frama-c/kernel/api/ast';
import { computationState } from 'frama-c/plugins/eva/api/general';
+import * as Eva from 'frama-c/plugins/eva/api/general';
// --------------------------------------------------------------------------
// --- Global Search Hints
@@ -51,7 +53,7 @@ function makeFunctionHint(fct: functionsData): Toolbars.Hint {
async function lookupGlobals(pattern: string): Promise<Toolbars.Hint[]> {
const lookup = pattern.toLowerCase();
- const fcts = States.getSyncArray(functions).getArray();
+ const fcts = States.getSyncArray(Kernel.functions).getArray();
return fcts.filter((fn) => (
0 <= fn.name.toLowerCase().indexOf(lookup)
)).map(makeFunctionHint);
@@ -96,13 +98,18 @@ function FctItem(props: FctItemProps): JSX.Element {
// --- Globals Section(s)
// --------------------------------------------------------------------------
+type functionsData =
+ Kernel.functionsData | (Kernel.functionsData & Eva.functionsData)
+
export default function Globals(): JSX.Element {
// Hooks
const [selection, updateSelection] = States.useSelection();
- const fcts = States.useSyncArray(functions).getArray().sort(
+ const kernelFcts = States.useSyncArray(Kernel.functions).getArray().sort(
(f, g) => alpha(f.name, g.name),
);
+ const evaFcts = States.useSyncArray(Eva.functions).getArray();
+ const fcts = ArrayUtils.mergeArraysByKey(kernelFcts, evaFcts);
const { useFlipSettings } = Dome;
const [stdlib, flipStdlib] =
useFlipSettings('ivette.globals.stdlib', false);
@@ -132,7 +139,8 @@ export default function Globals(): JSX.Element {
(stdlib || !fct.stdlib)
&& (builtin || !fct.builtin)
&& (undef || fct.defined)
- && (!evaOnly || !evaComputed || (fct.eva_analyzed === true))
+ && (!evaOnly || !evaComputed ||
+ ('eva_analyzed' in fct && fct.eva_analyzed === true))
&& (!selected || !multipleSelectionActive || isSelected(fct));
return visible || (!!current && fct.name === current);
}
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 70b14dd814e7cb57c693dff3a5a86b5515feed05..932488fecae57980244f4ec7f97e0d99a4db764a 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -367,8 +367,6 @@ export interface functionsData {
stdlib?: boolean;
/** Is the function a Frama-C builtin? */
builtin?: boolean;
- /** Has the function been analyzed by Eva */
- eva_analyzed?: boolean;
/** Source location */
sloc: source;
}
@@ -384,7 +382,6 @@ export const jFunctionsData: Json.Loose<functionsData> =
defined: Json.jBoolean,
stdlib: Json.jBoolean,
builtin: Json.jBoolean,
- eva_analyzed: Json.jBoolean,
sloc: jSourceSafe,
});
@@ -397,7 +394,7 @@ 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, sloc: source }>({
+ builtin?: boolean, sloc: source }>({
key: Compare.string,
name: Compare.alpha,
signature: Compare.string,
@@ -405,7 +402,6 @@ export const byFunctionsData: Compare.Order<functionsData> =
defined: Compare.defined(Compare.boolean),
stdlib: Compare.defined(Compare.boolean),
builtin: Compare.defined(Compare.boolean),
- eva_analyzed: Compare.defined(Compare.boolean),
sloc: bySource,
});
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 3ed2ea6b595d436fd82035130a5f13647d828103..0cc4595adf33d3b1fd1d4afe1a6329010a34775d 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -123,6 +123,83 @@ export const getCallers: Server.GetRequest<
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
>= getCallers_internal;
+/** Data for array rows [`functions`](#functions) */
+export interface functionsData {
+ /** Entry identifier. */
+ key: Json.key<'#functions'>;
+ /** Has the function been analyzed by Eva */
+ eva_analyzed?: boolean;
+}
+
+/** Loose decoder for `functionsData` */
+export const jFunctionsData: Json.Loose<functionsData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey<'#functions'>('#functions'),
+ '#functions expected'),
+ eva_analyzed: Json.jBoolean,
+ });
+
+/** Safe decoder for `functionsData` */
+export const jFunctionsDataSafe: Json.Safe<functionsData> =
+ Json.jFail(jFunctionsData,'FunctionsData expected');
+
+/** Natural order for `functionsData` */
+export const byFunctionsData: Compare.Order<functionsData> =
+ Compare.byFields
+ <{ key: Json.key<'#functions'>, eva_analyzed?: boolean }>({
+ key: Compare.string,
+ eva_analyzed: Compare.defined(Compare.boolean),
+ });
+
+/** Signal for array [`functions`](#functions) */
+export const signalFunctions: Server.Signal = {
+ name: 'plugins.eva.general.signalFunctions',
+};
+
+const reloadFunctions_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.reloadFunctions',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Force full reload for array [`functions`](#functions) */
+export const reloadFunctions: Server.GetRequest<null,null>= reloadFunctions_internal;
+
+const fetchFunctions_internal: Server.GetRequest<
+ number,
+ { pending: number, updated: functionsData[],
+ removed: Json.key<'#functions'>[], reload: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.fetchFunctions',
+ input: Json.jNumber,
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jFunctionsData),
+ removed: Json.jList(Json.jKey<'#functions'>('#functions')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
+ signals: [],
+};
+/** Data fetcher for array [`functions`](#functions) */
+export const fetchFunctions: Server.GetRequest<
+ number,
+ { pending: number, updated: functionsData[],
+ removed: Json.key<'#functions'>[], reload: boolean }
+ >= fetchFunctions_internal;
+
+const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
+ name: 'plugins.eva.general.functions',
+ getkey: ((d:functionsData) => d.key),
+ signal: signalFunctions,
+ fetch: fetchFunctions,
+ reload: reloadFunctions,
+ order: byFunctionsData,
+};
+/** AST Functions */
+export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
+
/** Unreachable and non terminating statements. */
export interface deadCode {
/** List of unreachable statements. */
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index eb76164294fca8a88a3e39f3c1937a952a9308e1..09b052ace96ce3190cad0681fae8243a912b5787 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -71,10 +71,34 @@ let () = Request.register ~package
(* ----- Functions ---------------------------------------------------------- *)
-let () =
- Analysis.register_computation_hook
- (fun _ -> States.reload Kernel_ast.Functions.array)
-
+module Functions =
+struct
+ let key kf = Printf.sprintf "kf#%d" (Kernel_function.get_id kf)
+
+ 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 =
+ let model = States.model () in
+
+ States.column model
+ ~name:"eva_analyzed"
+ ~descr:(Markdown.plain "Has the function been analyzed by Eva")
+ ~data:(module Data.Jbool)
+ ~default:false
+ ~get:Results.is_called;
+
+ States.register_array model
+ ~package ~key
+ ~name:"functions"
+ ~descr:(Markdown.plain "AST Functions")
+ ~iter
+ ~add_reload_hook:(fun f ->
+ Analysis.register_computation_hook (fun _ -> f () ))
+end
(* ----- Dead code: unreachable and non-terminating statements -------------- *)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 9b0ee6e61e2565b834785548bda0bec8c4e89dd2..a50aeb4f09d790b283cb68bf813a6ca8b6b7ae71 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -508,9 +508,6 @@ struct
let vi = Kernel_function.get_vi kf in
Cil.is_in_libc vi.vattr
- let is_eva_analyzed kf =
- if Db.Value.is_computed () then !Db.Value.is_called kf else false
-
let iter f =
Globals.Functions.iter
(fun kf ->
@@ -554,12 +551,6 @@ struct
~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.Jbool)
- ~default:false
- ~get:is_eva_analyzed;
States.column model
~name:"sloc"
~descr:(Md.plain "Source location")