diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts index aec33c528c5ef518269f3fdf08a594bd42732169..e0b4ccbdead11fe6eacec4f4a7197d1c71bf1e5b 100644 --- a/ivette/src/frama-c/kernel/api/ast/index.ts +++ b/ivette/src/frama-c/kernel/api/ast/index.ts @@ -152,7 +152,7 @@ export interface markerAttributesData { /** Function scope of the marker, if applicable */ scope?: string; /** Source location */ - sloc: source; + sloc?: source; } /** Decoder for `markerAttributesData` */ @@ -167,7 +167,7 @@ export const jMarkerAttributesData: Json.Decoder<markerAttributesData> = isFunction: Json.jBoolean, isFunDecl: Json.jBoolean, scope: Json.jOption(Json.jString), - sloc: jSource, + sloc: Json.jOption(jSource), }); /** Natural order for `markerAttributesData` */ @@ -175,7 +175,7 @@ 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 }>({ + isFunDecl: boolean, scope?: string, sloc?: source }>({ marker: byMarker, labelKind: Compare.alpha, titleKind: Compare.alpha, @@ -185,7 +185,7 @@ export const byMarkerAttributesData: Compare.Order<markerAttributesData> = isFunction: Compare.boolean, isFunDecl: Compare.boolean, scope: Compare.defined(Compare.string), - sloc: bySource, + sloc: Compare.defined(bySource), }); /** Signal for array [`markerAttributes`](#markerattributes) */ @@ -241,7 +241,7 @@ export const markerAttributes: State.Array<marker,markerAttributesData> = marker export const markerAttributesDataDefault: markerAttributesData = { marker: markerDefault, labelKind: '', titleKind: '', name: '', descr: '', isLval: false, isFunction: false, isFunDecl: false, scope: undefined, - sloc: sourceDefault }; + sloc: undefined }; const getMainFunction_internal: Server.GetRequest<null,fct | undefined> = { kind: Server.RqKind.GET, diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx index 92da070f66b5096a41eff374af01f6dd8b8e829d..4588949ce59e5fb047bc8c76b742bedac915304a 100644 --- a/ivette/src/frama-c/plugins/eva/valuetable.tsx +++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx @@ -218,9 +218,10 @@ interface StmtProps { function Stmt(props: StmtProps): JSX.Element | null { const { stmt, marker, short } = props; - const { descr, sloc: { base, line } } = States.useMarker(marker); + const { descr, sloc } = States.useMarker(marker); if (!stmt || !marker) return null; - const label = short ? `@L${line}` : `@${base}:${line}`; + // Location sloc should always be defined for statements. + const label = short ? `@L${sloc?.line}` : `@${sloc?.base}:${sloc?.line}`; const className = 'dome-text-cell eva-stmt'; return <span className={className} title={descr}>{label}</span>; } diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index e9caac0d72f77c0f06729ee541c2b56bfaeffd18..02fc76f1bc0aba538c3b951c7d44b4ac7fa4de13 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -394,11 +394,15 @@ struct model let () = - States.column + let get (tag, _) = + let pos = fst (Printer_tag.loc_of_localizable tag) in + if Cil_datatype.Position.(equal unknown pos) then None else Some pos + in + States.option ~name:"sloc" ~descr:(Md.plain "Source location") ~data:(module Position) - ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag)) + ~get model let array = States.register_array