[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

@@ -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,

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>;
 }

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