diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx index 78d4ed4189b20acb235ceade6a25abcee4018bdd..10b3715ec196d3cfe7f5544bde0ea9e19316f2b9 100644 --- a/ivette/src/frama-c/kernel/Globals.tsx +++ b/ivette/src/frama-c/kernel/Globals.tsx @@ -136,12 +136,20 @@ export default function Globals(): JSX.Element { useFlipSettings('ivette.globals.stdlib', false); const [builtin, flipBuiltin] = useFlipSettings('ivette.globals.builtin', false); + const [def, flipDef] = + useFlipSettings('ivette.globals.def', true); 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 [intern, flipIntern] = + useFlipSettings('ivette.globals.intern', true); + const [extern, flipExtern] = + useFlipSettings('ivette.globals.extern', true); + const [evaAnalyzed, flipEvaAnalyzed] = + useFlipSettings('ivette.globals.eva-analyzed', true); + const [evaUnreached, flipEvaUnreached] = + useFlipSettings('ivette.globals.eva-unreached', true); + const [selected, flipSelected] = + useFlipSettings('ivette.globals.selected', false); const multipleSelection = selection?.multiple; const multipleSelectionActive = multipleSelection?.allSelections.length > 0; const evaComputed = States.useSyncValue(computationState) === 'computed'; @@ -159,11 +167,16 @@ export default function Globals(): JSX.Element { const visible = (stdlib || !fct.stdlib) && (builtin || !fct.builtin) + && (def || !fct.defined) && (undef || fct.defined) - && (!evaOnly || !evaComputed || + && (intern || fct.extern) + && (extern || !fct.extern) + && (evaAnalyzed || !evaComputed || + !('eva_analyzed' in fct && fct.eva_analyzed === true)) + && (evaUnreached || !evaComputed || ('eva_analyzed' in fct && fct.eva_analyzed === true)) && (!selected || !multipleSelectionActive || isSelected(fct)); - return visible || (!!current && fct.name === current); + return !!visible; } function onSelection(name: string): void { @@ -182,24 +195,48 @@ export default function Globals(): JSX.Element { checked: stdlib, onClick: flipStdlib, }, + 'separator', + { + label: 'Show defined functions', + checked: def, + onClick: flipDef, + }, { label: 'Show undefined functions', checked: undef, onClick: flipUndef, }, 'separator', + { + label: 'Show intern functions', + checked: intern, + onClick: flipIntern, + }, + { + label: 'Show extern functions', + checked: extern, + onClick: flipExtern, + }, + 'separator', + { + label: 'Show functions analyzed by Eva', + enabled: evaComputed, + checked: evaAnalyzed, + onClick: flipEvaAnalyzed, + }, + { + label: 'Show functions unreached by Eva', + enabled: evaComputed, + checked: evaUnreached, + onClick: flipEvaUnreached, + }, + 'separator', { label: 'Selected only', enabled: multipleSelectionActive, checked: selected, onClick: flipSelected, }, - { - label: 'Analyzed by Eva only', - enabled: evaComputed, - checked: evaOnly, - onClick: flipEvaOnly, - }, ]; Dome.popupMenu(items); } diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts index 2a94f41e5e4262b9223d28e2ba1529d11b693ea1..aec33c528c5ef518269f3fdf08a594bd42732169 100644 --- a/ivette/src/frama-c/kernel/api/ast/index.ts +++ b/ivette/src/frama-c/kernel/api/ast/index.ts @@ -289,6 +289,8 @@ export interface functionsData { stdlib?: boolean; /** Is the function a Frama-C builtin? */ builtin?: boolean; + /** Is the function extern? */ + extern?: boolean; /** Source location */ sloc: source; } @@ -303,6 +305,7 @@ export const jFunctionsData: Json.Decoder<functionsData> = defined: Json.jOption(Json.jBoolean), stdlib: Json.jOption(Json.jBoolean), builtin: Json.jOption(Json.jBoolean), + extern: Json.jOption(Json.jBoolean), sloc: jSource, }); @@ -311,7 +314,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, sloc: source }>({ + builtin?: boolean, extern?: boolean, sloc: source }>({ key: Compare.string, name: Compare.alpha, signature: Compare.string, @@ -319,6 +322,7 @@ export const byFunctionsData: Compare.Order<functionsData> = defined: Compare.defined(Compare.boolean), stdlib: Compare.defined(Compare.boolean), builtin: Compare.defined(Compare.boolean), + extern: Compare.defined(Compare.boolean), sloc: bySource, }); @@ -375,7 +379,7 @@ export const functions: State.Array<Json.key<'#functions'>,functionsData> = func export const functionsDataDefault: functionsData = { key: Json.jKey<'#functions'>('#functions')(''), name: '', signature: '', main: undefined, defined: undefined, stdlib: undefined, - builtin: undefined, sloc: sourceDefault }; + builtin: undefined, extern: undefined, sloc: sourceDefault }; /** Updated AST information */ export const getInformationUpdate: Server.Signal = { diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 0cfafb80824a07954033b64b754e8bc9cab341e2..e9caac0d72f77c0f06729ee541c2b56bfaeffd18 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -474,9 +474,9 @@ struct let is_builtin kf = Cil_builtins.is_builtin (Kernel_function.get_vi kf) - let is_stdlib kf = + let is_extern kf = let vi = Kernel_function.get_vi kf in - Cil.is_in_libc vi.vattr + vi.vstorage = Extern let iter f = Globals.Functions.iter @@ -514,13 +514,19 @@ struct ~descr:(Md.plain "Is the function from the Frama-C stdlib?") ~data:(module Data.Jbool) ~default:false - ~get:is_stdlib; + ~get:Kernel_function.is_in_libc; 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:"extern" + ~descr:(Md.plain "Is the function extern?") + ~data:(module Data.Jbool) + ~default:false + ~get:is_extern; States.column model ~name:"sloc" ~descr:(Md.plain "Source location")