diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts index e0b4ccbdead11fe6eacec4f4a7197d1c71bf1e5b..a02d403f09a8950ca65dd1ef150851b3eb60356a 100644 --- a/ivette/src/frama-c/kernel/api/ast/index.ts +++ b/ivette/src/frama-c/kernel/api/ast/index.ts @@ -147,6 +147,8 @@ export interface markerAttributesData { isLval: boolean; /** Whether it is a function symbol */ isFunction: boolean; + /** Whether it is a function pointer */ + isFunctionPointer: boolean; /** Whether it is a function declaration */ isFunDecl: boolean; /** Function scope of the marker, if applicable */ @@ -165,6 +167,7 @@ export const jMarkerAttributesData: Json.Decoder<markerAttributesData> = descr: Json.jString, isLval: Json.jBoolean, isFunction: Json.jBoolean, + isFunctionPointer: Json.jBoolean, isFunDecl: Json.jBoolean, scope: Json.jOption(Json.jString), sloc: Json.jOption(jSource), @@ -175,7 +178,8 @@ export const byMarkerAttributesData: Compare.Order<markerAttributesData> = Compare.byFields <{ marker: marker, labelKind: string, titleKind: string, name: string, descr: string, isLval: boolean, isFunction: boolean, - isFunDecl: boolean, scope?: string, sloc?: source }>({ + isFunctionPointer: boolean, isFunDecl: boolean, scope?: string, + sloc?: source }>({ marker: byMarker, labelKind: Compare.alpha, titleKind: Compare.alpha, @@ -183,6 +187,7 @@ export const byMarkerAttributesData: Compare.Order<markerAttributesData> = descr: Compare.string, isLval: Compare.boolean, isFunction: Compare.boolean, + isFunctionPointer: Compare.boolean, isFunDecl: Compare.boolean, scope: Compare.defined(Compare.string), sloc: Compare.defined(bySource), @@ -240,8 +245,8 @@ export const markerAttributes: State.Array<marker,markerAttributesData> = marker /** Default value for `markerAttributesData` */ export const markerAttributesDataDefault: markerAttributesData = { marker: markerDefault, labelKind: '', titleKind: '', name: '', descr: '', - isLval: false, isFunction: false, isFunDecl: false, scope: undefined, - sloc: undefined }; + isLval: false, isFunction: false, isFunctionPointer: false, + isFunDecl: false, scope: undefined, sloc: undefined }; const getMainFunction_internal: Server.GetRequest<null,fct | undefined> = { kind: Server.RqKind.GET, diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 02fc76f1bc0aba538c3b951c7d44b4ac7fa4de13..f8c00bd913afce64be30134efa71558302ec8837 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -320,6 +320,13 @@ struct | Some vi -> Globals.Functions.mem vi | None -> false + let is_function_pointer = function + | PLval (_, _, (Mem _, NoOffset as lval)) + when Cil.(isFunctionType (typeOfLval lval)) -> true + | PLval (_, _, lval) + when Cil.(isFunPtrType (Cil.typeOfLval lval)) -> true + | _ -> false + let is_fundecl = function | PVDecl(Some _,Kglobal,vi) -> vi.vglob && Globals.Functions.mem vi | _ -> false @@ -377,6 +384,14 @@ struct ~get:(fun (tag, _) -> is_function tag) model + let () = + States.column + ~name:"isFunctionPointer" + ~descr:(Md.plain "Whether it is a function pointer") + ~data:(module Jbool) + ~get:(fun (tag, _) -> is_function_pointer tag) + model + let () = States.column ~name:"isFunDecl"