From 35f09eaf23b205d9aed5eddb7af98db3031263ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Mar 2023 10:39:26 +0100
Subject: [PATCH] [server] Marker attributes: the position is an option, as it
can be unknown.
Fixes a bug of the SourceCode component where the view is empty on markers
with unknown position, for instance on type markers.
Now, when selecting a type marker, the view displays the top of the current
function, which is not perfect, but better.
---
ivette/src/frama-c/kernel/api/ast/index.ts | 10 +++++-----
ivette/src/frama-c/plugins/eva/valuetable.tsx | 5 +++--
src/plugins/server/kernel_ast.ml | 8 ++++++--
3 files changed, 14 insertions(+), 9 deletions(-)
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index aec33c528c5..e0b4ccbdead 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 92da070f66b..4588949ce59 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 e9caac0d72f..02fc76f1bc0 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
--
GitLab