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")