diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts
index 83fe1a4fe381959d597e6ca6ac36a19cf56d2a29..dc1398e2ab95606276eb5ab92a4475f1ffbe3299 100644
--- a/ivette/api/generated/kernel/ast/index.ts
+++ b/ivette/api/generated/kernel/ast/index.ts
@@ -280,6 +280,16 @@ export interface functionsData {
name: string;
/** Signature */
signature: string;
+ /** Is the function the main entry point */
+ main?: boolean;
+ /** Is the function defined? */
+ defined?: boolean;
+ /** Is the function from the Frama-C stdlib? */
+ stdlib?: boolean;
+ /** Is the function a Frama-C builtin? */
+ builtin?: boolean;
+ /** Has the function been analyzed by Eva */
+ eva_analyzed?: boolean;
}
/** Loose decoder for `functionsData` */
@@ -289,6 +299,11 @@ export const jFunctionsData: Json.Loose<functionsData> =
'#functions expected'),
name: Json.jFail(Json.jString,'String expected'),
signature: Json.jFail(Json.jString,'String expected'),
+ main: Json.jBoolean,
+ defined: Json.jBoolean,
+ stdlib: Json.jBoolean,
+ builtin: Json.jBoolean,
+ eva_analyzed: Json.jBoolean,
});
/** Safe decoder for `functionsData` */
@@ -298,10 +313,17 @@ export const jFunctionsDataSafe: Json.Safe<functionsData> =
/** Natural order for `functionsData` */
export const byFunctionsData: Compare.Order<functionsData> =
Compare.byFields
- <{ key: Json.key<'#functions'>, name: string, signature: string }>({
+ <{ key: Json.key<'#functions'>, name: string, signature: string,
+ main?: boolean, defined?: boolean, stdlib?: boolean,
+ builtin?: boolean, eva_analyzed?: boolean }>({
key: Compare.string,
name: Compare.alpha,
signature: Compare.string,
+ 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),
});
/** Signal for array [`functions`](#functions) */
diff --git a/ivette/api/generated/plugins/eva/general/index.ts b/ivette/api/generated/plugins/eva/general/index.ts
index 008df7649b0abefc37880b90d6e771a8e6d49cc8..d16a45ad200fe7939ed2b1f81461ec0d78dce8e8 100644
--- a/ivette/api/generated/plugins/eva/general/index.ts
+++ b/ivette/api/generated/plugins/eva/general/index.ts
@@ -24,6 +24,15 @@ import { jMarkerSafe } from 'frama-c/api/kernel/ast';
//@ts-ignore
import { marker } from 'frama-c/api/kernel/ast';
+const isComputed_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.isComputed',
+ input: Json.jNull,
+ output: Json.jBoolean,
+};
+/** True if the Eva analysis has been done */
+export const isComputed: Server.GetRequest<null,boolean>= isComputed_internal;
+
const getCallers_internal: Server.GetRequest<
Json.key<'#fct'>,
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
diff --git a/ivette/src/dome/src/renderer/frame/sidebars.tsx b/ivette/src/dome/src/renderer/frame/sidebars.tsx
index 27fea8e0cc749bcda882d8e1176c8ea7358cded9..52dc2b2cd91bbb4d579259ed9318f8e31840ec25 100644
--- a/ivette/src/dome/src/renderer/frame/sidebars.tsx
+++ b/ivette/src/dome/src/renderer/frame/sidebars.tsx
@@ -99,6 +99,8 @@ export interface SectionProps {
disabled?: boolean;
/** Badge summary (only visible when folded). */
summary?: Badge;
+ /** Right-click callback. */
+ onContextMenu?: () => void;
/** Section contents. */
children?: React.ReactNode;
}
@@ -132,7 +134,8 @@ export function Section(props: SectionProps) {
<div className="dome-xSideBarSection">
<div
className="dome-xSideBarSection-title dome-color-frame"
- title={props.label}
+ title={props.title}
+ onContextMenu={props.onContextMenu}
>
<Label label={props.label} />
{!visible && makeBadge(props.summary)}
@@ -168,6 +171,10 @@ export interface ItemProps {
onSelection?: () => void;
/** Right-click callback. */
onContextMenu?: () => void;
+ /** Additional class. */
+ className?: string;
+ /** Additional styles. */
+ style?: React.CSSProperties;
/** Other item elements. */
children?: React.ReactNode;
}
@@ -182,10 +189,12 @@ export function Item(props: ItemProps) {
'dome-xSideBarItem',
selected ? 'dome-active' : 'dome-inactive',
isDisabled && 'dome-disabled',
+ props.className,
);
return (
<div
className={className}
+ style={props.style}
title={props.title}
onContextMenu={onContextMenu}
onClick={onClick}
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index 4b153c03dde17807d64943188e5a4667c6a0e063..ffd3959366776d3a1c9ed4ff9fba1a4932985645 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -5,9 +5,13 @@
import React from 'react';
import { Section, Item } from 'dome/frame/sidebars';
import type { Hint } from 'dome/frame/toolbars';
+import { classes } from 'dome/misc/utils';
import * as States from 'frama-c/states';
+import { useFlipSettings } from 'dome';
import { alpha } from 'dome/data/compare';
import { functions, functionsData } from 'frama-c/api/kernel/ast';
+import { isComputed } from 'frama-c/api/plugins/eva/general';
+import * as Dome from 'dome';
// --------------------------------------------------------------------------
// --- Global Search Hints
@@ -37,6 +41,39 @@ export function useHints(): [GlobalHint[], (pattern: string) => void] {
return [hints, onSearch];
}
+// --------------------------------------------------------------------------
+// --- Function Item
+// --------------------------------------------------------------------------
+
+interface FctItemProps {
+ fct: functionsData;
+ current: string | undefined;
+ onSelection: (name: string) => void;
+}
+
+function FctItem(props: FctItemProps) {
+ const { name, signature, main, stdlib, builtin, defined } = props.fct;
+ const className = classes(
+ main && 'globals-main',
+ (stdlib || builtin) && 'globals-stdlib',
+ );
+ const attributes = classes(
+ main && '(main)',
+ !stdlib && !builtin && !defined && '(ext)',
+ );
+ return (
+ <Item
+ className={className}
+ label={name}
+ title={signature}
+ selected={name === props.current}
+ onSelection={() => props.onSelection(name)}
+ >
+ {attributes && <span className="globals-attr">{attributes}</span>}
+ </Item>
+ );
+}
+
// --------------------------------------------------------------------------
// --- Globals Section(s)
// --------------------------------------------------------------------------
@@ -48,25 +85,98 @@ export default () => {
const fcts = States.useSyncArray(functions).getArray().sort(
(f, g) => alpha(f.name, g.name),
);
+ const [stdlib, flipStdlib] =
+ useFlipSettings('ivette.globals.stdlib', false);
+ const [builtin, flipBuiltin] =
+ useFlipSettings('ivette.globals.builtin', false);
+ const [undef, flipUndef] =
+ useFlipSettings('ivette.globals.undef', true);
+ const [selected, flipSelected] =
+ useFlipSettings('ivette.globals.selected', false);
+ const [evaOnly, flipEvaOnly] =
+ useFlipSettings('ivette.globals.evaonly', false);
+ const multipleSelection = selection?.multiple;
+ const multipleSelectionActive = multipleSelection?.allSelections.length > 0;
+ const evaComputed = States.useRequest(isComputed, null);
+
+ function isSelected(fct: functionsData) {
+ return multipleSelection?.allSelections.some(
+ (l) => fct.name === l?.function
+ );
+ }
+
+ function showFunction(fct: functionsData) {
+ const visible =
+ (stdlib || !fct.stdlib)
+ && (builtin || !fct.builtin)
+ && (undef || fct.defined)
+ && (!evaOnly || !evaComputed || (fct.eva_analyzed === true))
+ && (!selected || !multipleSelectionActive || isSelected(fct));
+ return visible;
+ }
+
+ function onSelection(name: string) {
+ updateSelection({ location: { function: name } });
+ }
+
+ async function onContextMenu() {
+ const items: Dome.PopupMenuItem[] = [
+ {
+ label: 'Show Frama-C builtins',
+ checked: builtin,
+ onClick: flipBuiltin,
+ },
+ {
+ label: 'Show stdlib functions',
+ checked: stdlib,
+ onClick: flipStdlib,
+ },
+ {
+ label: 'Show undefined functions',
+ checked: undef,
+ onClick: flipUndef,
+ },
+ 'separator',
+ {
+ label: 'Selected only',
+ enabled: multipleSelectionActive,
+ checked: selected,
+ onClick: flipSelected,
+ },
+ {
+ label: 'Analyzed by Eva only',
+ enabled: evaComputed,
+ checked: evaOnly,
+ onClick: flipEvaOnly,
+ },
+ ];
+ Dome.popupMenu(items);
+ }
// Items
const current: undefined | string = selection?.current?.function;
- const makeFctItem = (fct: functionsData) => {
- const kf = fct.name;
- return (
- <Item
- key={kf}
- label={kf}
- title={fct.signature}
- selected={kf === current}
- onSelection={() => updateSelection({ location: { function: kf } })}
- />
- );
- };
+ // Filtered
+
+ const filtered = fcts.filter(showFunction);
+ const nTotal = fcts.length;
+ const nFilter = filtered.length;
+ const title = `Functions ${nFilter} / ${nTotal}`;
return (
- <Section label="Functions" defaultUnfold>
- {fcts.map(makeFctItem)}
+ <Section
+ label="Functions"
+ title={title}
+ onContextMenu={onContextMenu}
+ defaultUnfold
+ >
+ {filtered.map((fct) => (
+ <FctItem
+ key={fct.name}
+ fct={fct}
+ current={current}
+ onSelection={onSelection}
+ />
+ ))}
</Section>
);
diff --git a/ivette/src/renderer/style.css b/ivette/src/renderer/style.css
index 09df391d8df39183598a6fa9d2636fc49ce2372b..f559cb1dfb3b9b7be75f2f70d3d1d33fef544430 100644
--- a/ivette/src/renderer/style.css
+++ b/ivette/src/renderer/style.css
@@ -36,4 +36,18 @@
border-bottom: solid 0.2em #BBB;
}
+.globals-main label {
+ text-decoration: underline;
+}
+
+.globals-stdlib label {
+ font-style: italic;
+}
+
+.globals-attr {
+ font-size: smaller;
+ font-weight: lighter;
+ color: #aaa;
+}
+
/* -------------------------------------------------------------------------- */
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index e428ec472cf0d420869f8a080b9d7e5dfa3a87e1..9d77d6ecb2d8a66cf7f851d2e658901dd79c14a6 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -578,12 +578,11 @@ let is_return_stmt kf stmt =
false
let is_entry_point kf =
- let main, _ = Globals.entry_point () in
- equal kf main
+ try equal kf (fst (Globals.entry_point ()))
+ with Globals.No_such_entry_point _ -> false
let is_main kf =
- let name = get_name kf in
- Datatype.String.equal name "main"
+ String.equal (get_name kf) "main"
let returns_void kf =
let result_type,_,_,_ = Cil.splitFunctionType (get_type kf) in
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 832c1adce2b70ba182a4549234391d18512c4f28..6dd76c134789afb91c5d3db8ef6eb3213da42721 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -338,11 +338,13 @@ let () = Request.register ~package
~input:(module Kf) ~output:(module Jtext)
begin fun kf ->
let libc = Kernel.PrintLibc.get () in
- if not libc then Kernel.PrintLibc.set true ;
- let global = Kernel_function.get_global kf in
- let ast = Jbuffer.to_json Printer.pp_global global in
- if not libc then Kernel.PrintLibc.set false ;
- ast
+ try
+ if not libc then Kernel.PrintLibc.set true ;
+ let global = Kernel_function.get_global kf in
+ let ast = Jbuffer.to_json Printer.pp_global global in
+ if not libc then Kernel.PrintLibc.set false ; ast
+ with err ->
+ if not libc then Kernel.PrintLibc.set false ; raise err
end
module Functions =
@@ -352,7 +354,31 @@ struct
let signature kf =
let global = Kernel_function.get_global kf in
- Rich_text.to_string Printer_tag.pretty (PGlobal global)
+ let libc = Kernel.PrintLibc.get () in
+ try
+ if not libc then Kernel.PrintLibc.set true ;
+ let txt = Rich_text.to_string Printer_tag.pretty (PGlobal global) in
+ if not libc then Kernel.PrintLibc.set false ;
+ if Kernel_function.is_entry_point kf then (txt ^ " /* main */") else txt
+ with err ->
+ if not libc then Kernel.PrintLibc.set false ; raise err
+
+ let is_builtin kf =
+ Cil_builtins.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_eva_analyzed kf =
+ if Db.Value.is_computed () then !Db.Value.is_called kf else false
+
+ 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
@@ -367,11 +393,41 @@ struct
~descr:(Md.plain "Signature")
~data:(module Data.Jstring)
~get:signature ;
+ States.column model
+ ~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.Jbool)
+ ~default:false
+ ~get:is_eva_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/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 865d7d9f0c0c0821b47b4dbfefd7ef66440c82c8..3dc3730f8f4b2707777bde129a6916dcb1f94d84 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,18 @@
"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
+ },
+ {
+ "key": "kf#20",
+ "name": "f",
+ "signature": "int f(int x);",
+ "defined": true
+ }
],
"removed": [],
"reload": true,
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index abf821d1d69063f79af1cc14354030b3920ae856..bbb5c95724375e6306e6e47c70497fcd2c28e9f5 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -31,6 +31,12 @@ let package =
~readme:"eva.md"
()
+let () = Request.register ~package
+ ~kind:`GET ~name:"isComputed"
+ ~descr:(Markdown.plain "True if the Eva analysis has been done")
+ ~input:(module Data.Junit) ~output:(module Data.Jbool)
+ Db.Value.is_computed
+
let is_computed kf =
Db.Value.is_computed () &&
match kf with