From fbee244377688cb82c3c6e18e152dd0efddc836c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 25 Jan 2023 17:47:57 +0100
Subject: [PATCH] [server] introduce default values
---
ivette/src/frama-c/kernel/api/ast/index.ts | 131 ++++++++++-------
ivette/src/frama-c/kernel/api/data/index.ts | 10 ++
.../src/frama-c/kernel/api/project/index.ts | 8 ++
.../frama-c/kernel/api/properties/index.ts | 41 +++++-
.../src/frama-c/kernel/api/services/index.ts | 36 ++++-
ivette/src/frama-c/plugins/dive/api/index.ts | 42 ++++++
.../frama-c/plugins/eva/api/general/index.ts | 136 ++++++++++++------
.../frama-c/plugins/eva/api/values/index.ts | 35 +++--
.../plugins/pivot/api/general/index.ts | 3 +
.../plugins/studia/api/studia/index.ts | 28 ++--
ivette/src/frama-c/states.ts | 16 +--
src/plugins/api-generator/api_generator.ml | 61 +++++++-
src/plugins/server/data.ml | 10 +-
src/plugins/server/package.ml | 17 ++-
src/plugins/server/package.mli | 6 +-
src/plugins/server/server_doc.ml | 4 +-
16 files changed, 421 insertions(+), 163 deletions(-)
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 7cbd4af0072..56a4cf5c77d 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -43,6 +43,8 @@ import { byText } from 'frama-c/kernel/api/data';
import { jText } from 'frama-c/kernel/api/data';
//@ts-ignore
import { text } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { textDefault } from 'frama-c/kernel/api/data';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
@@ -82,6 +84,22 @@ export const bySource: Compare.Order<source> =
line: Compare.number,
});
+/** Default value for `source` */
+export const sourceDefault: source =
+ { dir: '', base: '', file: '', line: 0 };
+
+/** Function names */
+export type fct = Json.key<'#fct'>;
+
+/** Decoder for `fct` */
+export const jFct: Json.Decoder<fct> = Json.jKey<'#fct'>('#fct');
+
+/** Natural order for `fct` */
+export const byFct: Compare.Order<fct> = Compare.string;
+
+/** Default value for `fct` */
+export const fctDefault: fct = Json.jKey<'#fct'>('#fct')('');
+
/** Localizable AST markers */
export type marker = Json.key<'#marker'>;
@@ -91,44 +109,46 @@ export const jMarker: Json.Decoder<marker> = Json.jKey<'#marker'>('#marker');
/** Natural order for `marker` */
export const byMarker: Compare.Order<marker> = Compare.string;
+/** Default value for `marker` */
+export const markerDefault: marker = Json.jKey<'#marker'>('#marker')('');
+
/** Location: function and marker */
-export interface location {
- /** Function */
- fct: Json.key<'#fct'>;
- /** Marker */
- marker: marker;
-}
+export type location = { fct: fct, marker: marker };
/** Decoder for `location` */
export const jLocation: Json.Decoder<location> =
- Json.jObject({ fct: Json.jKey<'#fct'>('#fct'), marker: jMarker,});
+ Json.jObject({ fct: jFct, marker: jMarker,});
/** Natural order for `location` */
export const byLocation: Compare.Order<location> =
Compare.byFields
- <{ fct: Json.key<'#fct'>, marker: marker }>({
- fct: Compare.string,
+ <{ fct: fct, marker: marker }>({
+ fct: byFct,
marker: byMarker,
});
+/** Default value for `location` */
+export const locationDefault: location =
+ { fct: fctDefault, marker: markerDefault };
+
/** Data for array rows [`markerAttributes`](#markerattributes) */
export interface markerAttributesData {
/** Entry identifier. */
- key: string;
+ marker: marker;
/** Marker kind (short) */
labelKind: string;
/** Marker kind (long) */
titleKind: string;
- /** Marker short name */
+ /** Marker short name or identifier when relevant. */
name: string;
/** Marker declaration or description */
descr: string;
/** Whether it is an l-value */
isLval: boolean;
- /** Whether it is a function declaration or definition */
- isFunDecl: boolean;
/** Whether it is a function symbol */
- isFun: boolean;
+ isFunction: boolean;
+ /** Whether it is a function declaration */
+ isFunDecl: boolean;
/** Function scope of the marker, if applicable */
scope?: string;
/** Source location */
@@ -138,14 +158,14 @@ export interface markerAttributesData {
/** Decoder for `markerAttributesData` */
export const jMarkerAttributesData: Json.Decoder<markerAttributesData> =
Json.jObject({
- key: Json.jString,
+ marker: jMarker,
labelKind: Json.jString,
titleKind: Json.jString,
name: Json.jString,
descr: Json.jString,
isLval: Json.jBoolean,
+ isFunction: Json.jBoolean,
isFunDecl: Json.jBoolean,
- isFun: Json.jBoolean,
scope: Json.jOption(Json.jString),
sloc: jSource,
});
@@ -153,17 +173,17 @@ export const jMarkerAttributesData: Json.Decoder<markerAttributesData> =
/** Natural order for `markerAttributesData` */
export const byMarkerAttributesData: Compare.Order<markerAttributesData> =
Compare.byFields
- <{ key: string, labelKind: string, titleKind: string, name: string,
- descr: string, isLval: boolean, isFunDecl: boolean, isFun: boolean,
- scope?: string, sloc: source }>({
- key: Compare.string,
+ <{ marker: marker, labelKind: string, titleKind: string, name: string,
+ descr: string, isLval: boolean, isFunction: boolean,
+ isFunDecl: boolean, scope?: string, sloc: source }>({
+ marker: byMarker,
labelKind: Compare.alpha,
titleKind: Compare.alpha,
name: Compare.alpha,
descr: Compare.string,
isLval: Compare.boolean,
+ isFunction: Compare.boolean,
isFunDecl: Compare.boolean,
- isFun: Compare.boolean,
scope: Compare.defined(Compare.string),
sloc: bySource,
});
@@ -185,7 +205,7 @@ export const reloadMarkerAttributes: Server.GetRequest<null,null>= reloadMarkerA
const fetchMarkerAttributes_internal: Server.GetRequest<
number,
- { pending: number, updated: markerAttributesData[], removed: string[],
+ { pending: number, updated: markerAttributesData[], removed: marker[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
@@ -194,7 +214,7 @@ const fetchMarkerAttributes_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jNumber,
updated: Json.jArray(jMarkerAttributesData),
- removed: Json.jArray(Json.jString),
+ removed: Json.jArray(jMarker),
reload: Json.jBoolean,
}),
signals: [],
@@ -202,58 +222,56 @@ const fetchMarkerAttributes_internal: Server.GetRequest<
/** Data fetcher for array [`markerAttributes`](#markerattributes) */
export const fetchMarkerAttributes: Server.GetRequest<
number,
- { pending: number, updated: markerAttributesData[], removed: string[],
+ { pending: number, updated: markerAttributesData[], removed: marker[],
reload: boolean }
>= fetchMarkerAttributes_internal;
-const markerAttributes_internal: State.Array<string,markerAttributesData> = {
+const markerAttributes_internal: State.Array<marker,markerAttributesData> = {
name: 'kernel.ast.markerAttributes',
- getkey: ((d:markerAttributesData) => d.key),
+ getkey: ((d:markerAttributesData) => d.marker),
signal: signalMarkerAttributes,
fetch: fetchMarkerAttributes,
reload: reloadMarkerAttributes,
order: byMarkerAttributesData,
};
/** Marker attributes */
-export const markerAttributes: State.Array<string,markerAttributesData> = markerAttributes_internal;
+export const markerAttributes: State.Array<marker,markerAttributesData> = markerAttributes_internal;
-const getMainFunction_internal: Server.GetRequest<
- null,
- Json.key<'#fct'> |
- undefined
- > = {
+/** Default value for `markerAttributesData` */
+export const markerAttributesDataDefault: markerAttributesData =
+ { marker: markerDefault, labelKind: '', titleKind: '', name: '', descr: '',
+ isLval: false, isFunction: false, isFunDecl: false, scope: undefined,
+ sloc: sourceDefault };
+
+const getMainFunction_internal: Server.GetRequest<null,fct | undefined> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getMainFunction',
input: Json.jNull,
- output: Json.jOption(Json.jKey<'#fct'>('#fct')),
+ output: Json.jOption(jFct),
signals: [],
};
/** Get the current 'main' function. */
-export const getMainFunction: Server.GetRequest<
- null,
- Json.key<'#fct'> |
- undefined
- >= getMainFunction_internal;
+export const getMainFunction: Server.GetRequest<null,fct | undefined>= getMainFunction_internal;
-const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
+const getFunctions_internal: Server.GetRequest<null,fct[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
input: Json.jNull,
- output: Json.jArray(Json.jKey<'#fct'>('#fct')),
+ output: Json.jArray(jFct),
signals: [],
};
/** Collect all functions in the AST */
-export const getFunctions: Server.GetRequest<null,Json.key<'#fct'>[]>= getFunctions_internal;
+export const getFunctions: Server.GetRequest<null,fct[]>= getFunctions_internal;
-const printFunction_internal: Server.GetRequest<Json.key<'#fct'>,text> = {
+const printFunction_internal: Server.GetRequest<fct,text> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.printFunction',
- input: Json.jKey<'#fct'>('#fct'),
+ input: jFct,
output: jText,
signals: [],
};
/** Print the AST of a function */
-export const printFunction: Server.GetRequest<Json.key<'#fct'>,text>= printFunction_internal;
+export const printFunction: Server.GetRequest<fct,text>= printFunction_internal;
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
@@ -353,6 +371,12 @@ const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
/** AST Functions */
export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
+/** Default value for `functionsData` */
+export const functionsDataDefault: functionsData =
+ { key: Json.jKey<'#functions'>('#functions')(''), name: '', signature: '',
+ main: undefined, defined: undefined, stdlib: undefined,
+ builtin: undefined, sloc: sourceDefault };
+
/** Updated AST information */
export const getInformationUpdate: Server.Signal = {
name: 'kernel.ast.getInformationUpdate',
@@ -385,21 +409,18 @@ export const getInformation: Server.GetRequest<
const getMarkerAt_internal: Server.GetRequest<
[ string, number, number ],
- [ Json.key<'#fct'> | undefined, marker | undefined ]
+ [ fct | undefined, marker | undefined ]
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getMarkerAt',
input: Json.jTriple( Json.jString, Json.jNumber, Json.jNumber,),
- output: Json.jPair(
- Json.jOption(Json.jKey<'#fct'>('#fct')),
- Json.jOption(jMarker),
- ),
+ output: Json.jPair( Json.jOption(jFct), Json.jOption(jMarker),),
signals: [],
};
/** Returns the marker and function at a source file position, if any. Input: file path, line and column. */
export const getMarkerAt: Server.GetRequest<
[ string, number, number ],
- [ Json.key<'#fct'> | undefined, marker | undefined ]
+ [ fct | undefined, marker | undefined ]
>= getMarkerAt_internal;
const getFiles_internal: Server.GetRequest<null,string[]> = {
@@ -422,22 +443,22 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
-const parseTerm_internal: Server.GetRequest<
+const parseExpr_internal: Server.GetRequest<
{ term: string, stmt: marker },
marker |
undefined
> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.parseTerm',
+ name: 'kernel.ast.parseExpr',
input: Json.jObject({ term: Json.jString, stmt: jMarker,}),
output: Json.jOption(jMarker),
signals: [],
};
-/** Parse an ACSL Term and returns the associated marker */
-export const parseTerm: Server.GetRequest<
+/** Parse a C expression and returns the associated marker */
+export const parseExpr: Server.GetRequest<
{ term: string, stmt: marker },
marker |
undefined
- >= parseTerm_internal;
+ >= parseExpr_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/api/data/index.ts b/ivette/src/frama-c/kernel/api/data/index.ts
index 8cd515d9dd5..6cd1ba463a9 100644
--- a/ivette/src/frama-c/kernel/api/data/index.ts
+++ b/ivette/src/frama-c/kernel/api/data/index.ts
@@ -47,6 +47,9 @@ export const jMarkdown: Json.Decoder<markdown> = Json.jString;
/** Natural order for `markdown` */
export const byMarkdown: Compare.Order<markdown> = Compare.string;
+/** Default value for `markdown` */
+export const markdownDefault: markdown = '';
+
/** Rich text format uses `[tag; …text ]` to apply the tag `tag` to the enclosed text. Empty tag `""` can also used to simply group text together. */
export type text = null | string | text[];
@@ -62,6 +65,9 @@ export const jText: Json.Decoder<text> =
export const byText: Compare.Order<text> =
(_x: any, _y: any) => Compare.structural(_x,_y);
+/** Default value for `text` */
+export const textDefault: text = null;
+
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
@@ -78,4 +84,8 @@ export const byTag: Compare.Order<tag> =
descr: byMarkdown,
});
+/** Default value for `tag` */
+export const tagDefault: tag =
+ { name: '', label: markdownDefault, descr: markdownDefault };
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/api/project/index.ts b/ivette/src/frama-c/kernel/api/project/index.ts
index fdb80fc3c0c..3d8ce768c21 100644
--- a/ivette/src/frama-c/kernel/api/project/index.ts
+++ b/ivette/src/frama-c/kernel/api/project/index.ts
@@ -59,6 +59,10 @@ export const byProjectInfo: Compare.Order<projectInfo> =
current: Compare.boolean,
});
+/** Default value for `projectInfo` */
+export const projectInfoDefault: projectInfo =
+ { id: Json.jKey<'#project'>('#project')(''), name: '', current: false };
+
/** Request to be executed on the specified project. */
export type projectRequest =
{ project: Json.key<'#project'>, request: string, data: Json.json };
@@ -80,6 +84,10 @@ export const byProjectRequest: Compare.Order<projectRequest> =
data: Compare.structural,
});
+/** Default value for `projectRequest` */
+export const projectRequestDefault: projectRequest =
+ { project: Json.jKey<'#project'>('#project')(''), request: '', data: null };
+
const getCurrent_internal: Server.GetRequest<null,projectInfo> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getCurrent',
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index ab774d1f222..bb314b1d26b 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -37,24 +37,38 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { bySource } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jSource } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { source } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { sourceDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { jTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { tag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { tagDefault } from 'frama-c/kernel/api/data';
/** Property Kinds */
export enum propKind {
@@ -134,6 +148,9 @@ export const jPropKind: Json.Decoder<propKind> = Json.jEnum(propKind);
/** Natural order for `propKind` */
export const byPropKind: Compare.Order<propKind> = Compare.byEnum(propKind);
+/** Default value for `propKind` */
+export const propKindDefault: propKind = propKind.behavior;
+
const propKindTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.properties.propKindTags',
@@ -177,6 +194,9 @@ export const jPropStatus: Json.Decoder<propStatus> = Json.jEnum(propStatus);
export const byPropStatus: Compare.Order<propStatus> =
Compare.byEnum(propStatus);
+/** Default value for `propStatus` */
+export const propStatusDefault: propStatus = propStatus.unknown;
+
const propStatusTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.properties.propStatusTags',
@@ -231,6 +251,9 @@ export const jAlarms: Json.Decoder<alarms> = Json.jEnum(alarms);
/** Natural order for `alarms` */
export const byAlarms: Compare.Order<alarms> = Compare.byEnum(alarms);
+/** Default value for `alarms` */
+export const alarmsDefault: alarms = alarms.division_by_zero;
+
const alarmsTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.properties.alarmsTags',
@@ -254,7 +277,7 @@ export interface statusData {
/** Status */
status: propStatus;
/** Function */
- fct?: Json.key<'#fct'>;
+ fct?: fct;
/** Instruction */
kinstr?: marker;
/** Position */
@@ -275,7 +298,7 @@ export const jStatusData: Json.Decoder<statusData> =
kind: jPropKind,
names: Json.jArray(Json.jString),
status: jPropStatus,
- fct: Json.jOption(Json.jKey<'#fct'>('#fct')),
+ fct: Json.jOption(jFct),
kinstr: Json.jOption(jMarker),
source: jSource,
alarm: Json.jOption(Json.jString),
@@ -287,15 +310,14 @@ export const jStatusData: Json.Decoder<statusData> =
export const byStatusData: Compare.Order<statusData> =
Compare.byFields
<{ key: marker, descr: string, kind: propKind, names: string[],
- status: propStatus, fct?: Json.key<'#fct'>, kinstr?: marker,
- source: source, alarm?: string, alarm_descr?: string,
- predicate?: string }>({
+ status: propStatus, fct?: fct, kinstr?: marker, source: source,
+ alarm?: string, alarm_descr?: string, predicate?: string }>({
key: byMarker,
descr: Compare.string,
kind: byPropKind,
names: Compare.array(Compare.string),
status: byPropStatus,
- fct: Compare.defined(Compare.string),
+ fct: Compare.defined(byFct),
kinstr: Compare.defined(byMarker),
source: bySource,
alarm: Compare.defined(Compare.string),
@@ -352,4 +374,11 @@ const status_internal: State.Array<marker,statusData> = {
/** Status of Registered Properties */
export const status: State.Array<marker,statusData> = status_internal;
+/** Default value for `statusData` */
+export const statusDataDefault: statusData =
+ { key: markerDefault, descr: '', kind: propKindDefault, names: [],
+ status: propStatusDefault, fct: undefined, kinstr: undefined,
+ source: sourceDefault, alarm: undefined, alarm_descr: undefined,
+ predicate: undefined };
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/api/services/index.ts b/ivette/src/frama-c/kernel/api/services/index.ts
index 21df34a7a89..e2db53a9dc3 100644
--- a/ivette/src/frama-c/kernel/api/services/index.ts
+++ b/ivette/src/frama-c/kernel/api/services/index.ts
@@ -37,24 +37,38 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { bySource } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jSource } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { source } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { sourceDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { jTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { tag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { tagDefault } from 'frama-c/kernel/api/data';
const getConfig_internal: Server.GetRequest<
null,
@@ -118,6 +132,9 @@ export const jLogkind: Json.Decoder<logkind> = Json.jEnum(logkind);
/** Natural order for `logkind` */
export const byLogkind: Compare.Order<logkind> = Compare.byEnum(logkind);
+/** Default value for `logkind` */
+export const logkindDefault: logkind = logkind.ERROR;
+
const logkindTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.services.logkindTags',
@@ -145,7 +162,7 @@ export interface messageData {
/** Marker at the message position (if any) */
marker?: marker;
/** Function containing the message position (if any) */
- fct?: Json.key<'#fct'>;
+ fct?: fct;
}
/** Decoder for `messageData` */
@@ -158,7 +175,7 @@ export const jMessageData: Json.Decoder<messageData> =
category: Json.jOption(Json.jString),
source: Json.jOption(jSource),
marker: Json.jOption(jMarker),
- fct: Json.jOption(Json.jKey<'#fct'>('#fct')),
+ fct: Json.jOption(jFct),
});
/** Natural order for `messageData` */
@@ -166,7 +183,7 @@ export const byMessageData: Compare.Order<messageData> =
Compare.byFields
<{ key: Json.key<'#message'>, kind: logkind, plugin: string,
message: string, category?: string, source?: source, marker?: marker,
- fct?: Json.key<'#fct'> }>({
+ fct?: fct }>({
key: Compare.string,
kind: byLogkind,
plugin: Compare.alpha,
@@ -174,7 +191,7 @@ export const byMessageData: Compare.Order<messageData> =
category: Compare.defined(Compare.string),
source: Compare.defined(bySource),
marker: Compare.defined(byMarker),
- fct: Compare.defined(Compare.string),
+ fct: Compare.defined(byFct),
});
/** Signal for array [`message`](#message) */
@@ -226,6 +243,12 @@ const message_internal: State.Array<Json.key<'#message'>,messageData> = {
/** Log messages */
export const message: State.Array<Json.key<'#message'>,messageData> = message_internal;
+/** Default value for `messageData` */
+export const messageDataDefault: messageData =
+ { key: Json.jKey<'#message'>('#message')(''), kind: logkindDefault,
+ plugin: '', message: '', category: undefined, source: undefined,
+ marker: undefined, fct: undefined };
+
/** Message event record. */
export interface log {
/** Message kind */
@@ -262,6 +285,11 @@ export const byLog: Compare.Order<log> =
source: Compare.defined(bySource),
});
+/** Default value for `log` */
+export const logDefault: log =
+ { kind: logkindDefault, plugin: '', message: '', category: undefined,
+ source: undefined };
+
const setLogs_internal: Server.SetRequest<boolean,null> = {
kind: Server.RqKind.SET,
name: 'kernel.services.setLogs',
diff --git a/ivette/src/frama-c/plugins/dive/api/index.ts b/ivette/src/frama-c/plugins/dive/api/index.ts
index 0d585f8009a..cd47a1579e0 100644
--- a/ivette/src/frama-c/plugins/dive/api/index.ts
+++ b/ivette/src/frama-c/plugins/dive/api/index.ts
@@ -48,7 +48,11 @@ import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { location } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { locationDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
/** Parametrization of the exploration range. */
export interface range {
@@ -73,6 +77,10 @@ export const byRange: Compare.Order<range> =
forward: Compare.defined(Compare.number),
});
+/** Default value for `range` */
+export const rangeDefault: range =
+ { backward: undefined, forward: undefined };
+
/** Global parametrization of the exploration. */
export interface explorationWindow {
/** how far dive will explore from root nodes ; must be a finite range */
@@ -93,6 +101,10 @@ export const byExplorationWindow: Compare.Order<explorationWindow> =
horizon: byRange,
});
+/** Default value for `explorationWindow` */
+export const explorationWindowDefault: explorationWindow =
+ { perception: rangeDefault, horizon: rangeDefault };
+
/** A node identifier in the graph */
export type nodeId = number;
@@ -102,6 +114,9 @@ export const jNodeId: Json.Decoder<nodeId> = Json.jNumber;
/** Natural order for `nodeId` */
export const byNodeId: Compare.Order<nodeId> = Compare.number;
+/** Default value for `nodeId` */
+export const nodeIdDefault: nodeId = 0;
+
/** A callsite */
export type callsite = { fun: string, instr: number | string };
@@ -120,6 +135,9 @@ export const byCallsite: Compare.Order<callsite> =
instr: Compare.structural,
});
+/** Default value for `callsite` */
+export const callsiteDefault: callsite = { fun: '', instr: 0 };
+
/** The callstack context for a node */
export type callstack = callsite[];
@@ -130,6 +148,9 @@ export const jCallstack: Json.Decoder<callstack> = Json.jArray(jCallsite);
export const byCallstack: Compare.Order<callstack> =
Compare.array(byCallsite);
+/** Default value for `callstack` */
+export const callstackDefault: callstack = [];
+
/** The description of a node locality */
export type nodeLocality = { file: string, callstack?: callstack };
@@ -145,6 +166,10 @@ export const byNodeLocality: Compare.Order<nodeLocality> =
callstack: Compare.defined(byCallstack),
});
+/** Default value for `nodeLocality` */
+export const nodeLocalityDefault: nodeLocality =
+ { file: '', callstack: undefined };
+
/** A graph node */
export type node =
{ id: nodeId, label: string, kind: string, locality: nodeLocality,
@@ -195,6 +220,12 @@ export const byNode: Compare.Order<node> =
taint: Compare.defined(Compare.structural),
});
+/** Default value for `node` */
+export const nodeDefault: node =
+ { id: nodeIdDefault, label: '', kind: '', locality: nodeLocalityDefault,
+ is_root: false, backward_explored: '', forward_explored: '', writes: [],
+ values: undefined, range: 0, type: undefined, taint: undefined };
+
/** The dependency between two nodes */
export type dependency =
{ id: number, src: nodeId, dst: nodeId, kind: string, origins: location[] };
@@ -221,6 +252,10 @@ export const byDependency: Compare.Order<dependency> =
origins: Compare.array(byLocation),
});
+/** Default value for `dependency` */
+export const dependencyDefault: dependency =
+ { id: 0, src: nodeIdDefault, dst: nodeIdDefault, kind: '', origins: [] };
+
/** The whole graph being built */
export type graphData = { nodes: node[], deps: dependency[] };
@@ -236,6 +271,9 @@ export const byGraphData: Compare.Order<graphData> =
deps: Compare.array(byDependency),
});
+/** Default value for `graphData` */
+export const graphDataDefault: graphData = { nodes: [], deps: [] };
+
/** Graph differences from the last action. */
export type diffData =
{ root?: nodeId, add: { nodes: node[], deps: dependency[] }, sub: nodeId[]
@@ -266,6 +304,10 @@ export const byDiffData: Compare.Order<diffData> =
sub: Compare.array(byNodeId),
});
+/** Default value for `diffData` */
+export const diffDataDefault: diffData =
+ { root: undefined, add: { nodes: [], deps: [] }, sub: [] };
+
const window_internal: Server.SetRequest<explorationWindow,null> = {
kind: Server.RqKind.SET,
name: 'plugins.dive.window',
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 1ccceb03887..b5914a0f5c9 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -37,18 +37,30 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { jTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { tag } from 'frama-c/kernel/api/data';
+//@ts-ignore
+import { tagDefault } from 'frama-c/kernel/api/data';
/** State of the computation of Eva Analysis. */
export type computationStateType = "not_computed" | "computing" | "computed";
@@ -65,6 +77,10 @@ export const jComputationStateType: Json.Decoder<computationStateType> =
export const byComputationStateType: Compare.Order<computationStateType> =
Compare.structural;
+/** Default value for `computationStateType` */
+export const computationStateTypeDefault: computationStateType =
+ "not_computed";
+
/** Signal for state [`computationState`](#computationstate) */
export const signalComputationState: Server.Signal = {
name: 'plugins.eva.general.signalComputationState',
@@ -94,35 +110,30 @@ const computationState_internal: State.Value<computationStateType> = {
/** The current computation state of the analysis. */
export const computationState: State.Value<computationStateType> = computationState_internal;
-/** CallSite */
-export interface CallSite {
- /** Function */
- kf: Json.key<'#fct'>;
- /** Statement */
- stmt: marker;
-}
+/** Call site, combining function and stmt */
+export type CallSite = { kf: fct, stmt: marker };
/** Decoder for `CallSite` */
export const jCallSite: Json.Decoder<CallSite> =
- Json.jObject({ kf: Json.jKey<'#fct'>('#fct'), stmt: jMarker,});
+ Json.jObject({ kf: jFct, stmt: jMarker,});
/** Natural order for `CallSite` */
export const byCallSite: Compare.Order<CallSite> =
- Compare.byFields
- <{ kf: Json.key<'#fct'>, stmt: marker }>({
- kf: Compare.string,
- stmt: byMarker,
- });
+ Compare.byFields<{ kf: fct, stmt: marker }>({ kf: byFct, stmt: byMarker, });
-const getCallers_internal: Server.GetRequest<Json.key<'#fct'>,CallSite[]> = {
+/** Default value for `CallSite` */
+export const CallSiteDefault: CallSite =
+ { kf: fctDefault, stmt: markerDefault };
+
+const getCallers_internal: Server.GetRequest<fct,CallSite[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.getCallers',
- input: Json.jKey<'#fct'>('#fct'),
+ input: jFct,
output: Json.jArray(jCallSite),
signals: [],
};
/** Get the list of call site of a function */
-export const getCallers: Server.GetRequest<Json.key<'#fct'>,CallSite[]>= getCallers_internal;
+export const getCallers: Server.GetRequest<fct,CallSite[]>= getCallers_internal;
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
@@ -196,6 +207,10 @@ const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
/** AST Functions */
export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
+/** Default value for `functionsData` */
+export const functionsDataDefault: functionsData =
+ { key: Json.jKey<'#functions'>('#functions')(''), eva_analyzed: undefined };
+
/** Unreachable and non terminating statements. */
export interface deadCode {
/** List of unreachable statements. */
@@ -219,15 +234,19 @@ export const byDeadCode: Compare.Order<deadCode> =
nonTerminating: Compare.array(byMarker),
});
-const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
+/** Default value for `deadCode` */
+export const deadCodeDefault: deadCode =
+ { unreachable: [], nonTerminating: [] };
+
+const getDeadCode_internal: Server.GetRequest<fct,deadCode> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.getDeadCode',
- input: Json.jKey<'#fct'>('#fct'),
+ input: jFct,
output: jDeadCode,
signals: [],
};
/** Get the lists of unreachable and of non terminating statements in a function */
-export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
+export const getDeadCode: Server.GetRequest<fct,deadCode>= getDeadCode_internal;
/** Taint status of logical properties */
export enum taintStatus {
@@ -257,6 +276,9 @@ export const jTaintStatus: Json.Decoder<taintStatus> =
export const byTaintStatus: Compare.Order<taintStatus> =
Compare.byEnum(taintStatus);
+/** Default value for `taintStatus` */
+export const taintStatusDefault: taintStatus = taintStatus.not_computed;
+
const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.taintStatusTags',
@@ -287,21 +309,19 @@ export const byLvalueTaints: Compare.Order<LvalueTaints> =
taint: byTaintStatus,
});
-const taintedLvalues_internal: Server.GetRequest<
- Json.key<'#fundec'>,
- LvalueTaints[]
- > = {
+/** Default value for `LvalueTaints` */
+export const LvalueTaintsDefault: LvalueTaints =
+ { lval: markerDefault, taint: taintStatusDefault };
+
+const taintedLvalues_internal: Server.GetRequest<fct,LvalueTaints[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.taintedLvalues',
- input: Json.jKey<'#fundec'>('#fundec'),
+ input: jFct,
output: Json.jArray(jLvalueTaints),
signals: [],
};
/** Get the tainted lvalues of a given function */
-export const taintedLvalues: Server.GetRequest<
- Json.key<'#fundec'>,
- LvalueTaints[]
- >= taintedLvalues_internal;
+export const taintedLvalues: Server.GetRequest<fct,LvalueTaints[]>= taintedLvalues_internal;
/** Data for array rows [`properties`](#properties) */
export interface propertiesData {
@@ -376,6 +396,10 @@ const properties_internal: State.Array<marker,propertiesData> = {
/** Status of Registered Properties */
export const properties: State.Array<marker,propertiesData> = properties_internal;
+/** Default value for `propertiesData` */
+export const propertiesDataDefault: propertiesData =
+ { key: markerDefault, priority: false, taint: taintStatusDefault };
+
/** The alarms are counted after being grouped by these categories */
export enum alarmCategory {
/** Integer division by zero */
@@ -408,6 +432,10 @@ export const jAlarmCategory: Json.Decoder<alarmCategory> =
export const byAlarmCategory: Compare.Order<alarmCategory> =
Compare.byEnum(alarmCategory);
+/** Default value for `alarmCategory` */
+export const alarmCategoryDefault: alarmCategory =
+ alarmCategory.division_by_zero;
+
const alarmCategoryTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.alarmCategoryTags',
@@ -439,6 +467,10 @@ export const byStatusesEntry: Compare.Order<statusesEntry> =
invalid: Compare.number,
});
+/** Default value for `statusesEntry` */
+export const statusesEntryDefault: statusesEntry =
+ { valid: 0, unknown: 0, invalid: 0 };
+
/** Alarm count for each alarm category. */
export type alarmEntry = { category: alarmCategory, count: number };
@@ -454,6 +486,10 @@ export const byAlarmEntry: Compare.Order<alarmEntry> =
count: Compare.number,
});
+/** Default value for `alarmEntry` */
+export const alarmEntryDefault: alarmEntry =
+ { category: alarmCategoryDefault, count: 0 };
+
/** Statistics about an Eva analysis. */
export type programStatsType =
{ progFunCoverage: { reachable: number, dead: number },
@@ -522,6 +558,16 @@ export const byProgramStatsType: Compare.Order<programStatsType> =
precondsStatuses: byStatusesEntry,
});
+/** Default value for `programStatsType` */
+export const programStatsTypeDefault: programStatsType =
+ { progFunCoverage: { reachable: 0, dead: 0 },
+ progStmtCoverage: { reachable: 0, dead: 0 }, progAlarms: [],
+ evaEvents: { errors: 0, warnings: 0 },
+ kernelEvents: { errors: 0, warnings: 0 },
+ alarmsStatuses: statusesEntryDefault,
+ assertionsStatuses: statusesEntryDefault,
+ precondsStatuses: statusesEntryDefault };
+
/** Signal for state [`programStats`](#programstats) */
export const signalProgramStats: Server.Signal = {
name: 'plugins.eva.general.signalProgramStats',
@@ -548,7 +594,7 @@ export const programStats: State.Value<programStatsType> = programStats_internal
/** Data for array rows [`functionStats`](#functionstats) */
export interface functionStatsData {
/** Entry identifier. */
- key: Json.key<'#fundec'>;
+ key: fct;
/** Coverage of the Eva analysis */
coverage: { reachable: number, dead: number };
/** Alarms raised by the Eva analysis by category */
@@ -560,7 +606,7 @@ export interface functionStatsData {
/** Decoder for `functionStatsData` */
export const jFunctionStatsData: Json.Decoder<functionStatsData> =
Json.jObject({
- key: Json.jKey<'#fundec'>('#fundec'),
+ key: jFct,
coverage: Json.jObject({ reachable: Json.jNumber, dead: Json.jNumber,}),
alarmCount: Json.jArray(jAlarmEntry),
alarmStatuses: jStatusesEntry,
@@ -569,10 +615,9 @@ export const jFunctionStatsData: Json.Decoder<functionStatsData> =
/** Natural order for `functionStatsData` */
export const byFunctionStatsData: Compare.Order<functionStatsData> =
Compare.byFields
- <{ key: Json.key<'#fundec'>,
- coverage: { reachable: number, dead: number },
+ <{ key: fct, coverage: { reachable: number, dead: number },
alarmCount: alarmEntry[], alarmStatuses: statusesEntry }>({
- key: Compare.string,
+ key: byFct,
coverage: Compare.byFields
<{ reachable: number, dead: number }>({
reachable: Compare.number,
@@ -599,8 +644,8 @@ export const reloadFunctionStats: Server.GetRequest<null,null>= reloadFunctionSt
const fetchFunctionStats_internal: Server.GetRequest<
number,
- { pending: number, updated: functionStatsData[],
- removed: Json.key<'#fundec'>[], reload: boolean }
+ { pending: number, updated: functionStatsData[], removed: fct[],
+ reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.fetchFunctionStats',
@@ -608,7 +653,7 @@ const fetchFunctionStats_internal: Server.GetRequest<
output: Json.jObject({
pending: Json.jNumber,
updated: Json.jArray(jFunctionStatsData),
- removed: Json.jArray(Json.jKey<'#fundec'>('#fundec')),
+ removed: Json.jArray(jFct),
reload: Json.jBoolean,
}),
signals: [],
@@ -616,14 +661,11 @@ const fetchFunctionStats_internal: Server.GetRequest<
/** Data fetcher for array [`functionStats`](#functionstats) */
export const fetchFunctionStats: Server.GetRequest<
number,
- { pending: number, updated: functionStatsData[],
- removed: Json.key<'#fundec'>[], reload: boolean }
+ { pending: number, updated: functionStatsData[], removed: fct[],
+ reload: boolean }
>= fetchFunctionStats_internal;
-const functionStats_internal: State.Array<
- Json.key<'#fundec'>,
- functionStatsData
- > = {
+const functionStats_internal: State.Array<fct,functionStatsData> = {
name: 'plugins.eva.general.functionStats',
getkey: ((d:functionStatsData) => d.key),
signal: signalFunctionStats,
@@ -632,10 +674,12 @@ const functionStats_internal: State.Array<
order: byFunctionStatsData,
};
/** Statistics about the last Eva analysis for each function */
-export const functionStats: State.Array<
- Json.key<'#fundec'>,
- functionStatsData
- > = functionStats_internal;
+export const functionStats: State.Array<fct,functionStatsData> = functionStats_internal;
+
+/** Default value for `functionStatsData` */
+export const functionStatsDataDefault: functionStatsData =
+ { key: fctDefault, coverage: { reachable: 0, dead: 0 }, alarmCount: [],
+ alarmStatuses: statusesEntryDefault };
const getStates_internal: Server.GetRequest<
[ marker, boolean ],
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index fdb7cf5397b..5ca5cfd1828 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -37,12 +37,22 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
/** Emitted when EVA results has changed */
export const changed: Server.Signal = {
@@ -58,6 +68,10 @@ export const jCallstack: Json.Decoder<callstack> =
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> = Compare.number;
+/** Default value for `callstack` */
+export const callstackDefault: callstack =
+ Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id')(-1);
+
const getCallstacks_internal: Server.GetRequest<marker[],callstack[]> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstacks',
@@ -70,16 +84,15 @@ export const getCallstacks: Server.GetRequest<marker[],callstack[]>= getCallstac
const getCallstackInfo_internal: Server.GetRequest<
callstack,
- { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>, stmt?: marker,
- rank?: number }[]
+ { callee: fct, caller?: fct, stmt?: marker, rank?: number }[]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getCallstackInfo',
input: jCallstack,
output: Json.jArray(
Json.jObject({
- callee: Json.jKey<'#fct'>('#fct'),
- caller: Json.jOption(Json.jKey<'#fct'>('#fct')),
+ callee: jFct,
+ caller: Json.jOption(jFct),
stmt: Json.jOption(jMarker),
rank: Json.jOption(Json.jNumber),
})),
@@ -88,25 +101,23 @@ const getCallstackInfo_internal: Server.GetRequest<
/** Callstack Description */
export const getCallstackInfo: Server.GetRequest<
callstack,
- { callee: Json.key<'#fct'>, caller?: Json.key<'#fct'>, stmt?: marker,
- rank?: number }[]
+ { callee: fct, caller?: fct, stmt?: marker, rank?: number }[]
>= getCallstackInfo_internal;
const getStmtInfo_internal: Server.GetRequest<
marker,
- { rank: number, fct: Json.key<'#fct'> }
+ { rank: number, fct: fct }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getStmtInfo',
input: jMarker,
- output: Json.jObject({ rank: Json.jNumber, fct: Json.jKey<'#fct'>('#fct'),
- }),
+ output: Json.jObject({ rank: Json.jNumber, fct: jFct,}),
signals: [],
};
/** Stmt Information */
export const getStmtInfo: Server.GetRequest<
marker,
- { rank: number, fct: Json.key<'#fct'> }
+ { rank: number, fct: fct }
>= getStmtInfo_internal;
const getProbeInfo_internal: Server.GetRequest<
@@ -170,6 +181,10 @@ export const byEvaluation: Compare.Order<evaluation> =
pointedVars: Compare.array(Compare.pair(Compare.string,byMarker,)),
});
+/** Default value for `evaluation` */
+export const evaluationDefault: evaluation =
+ { value: '', alarms: [], pointedVars: [] };
+
const getValues_internal: Server.GetRequest<
{ callstack?: callstack, target: marker },
{ vElse?: evaluation, vThen?: evaluation, vAfter?: evaluation,
diff --git a/ivette/src/frama-c/plugins/pivot/api/general/index.ts b/ivette/src/frama-c/plugins/pivot/api/general/index.ts
index 40745e002bd..208a49ada0e 100644
--- a/ivette/src/frama-c/plugins/pivot/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/pivot/api/general/index.ts
@@ -49,6 +49,9 @@ export const jTableStateType: Json.Decoder<tableStateType> =
export const byTableStateType: Compare.Order<tableStateType> =
Compare.array(Compare.array(Compare.string));
+/** Default value for `tableStateType` */
+export const tableStateTypeDefault: tableStateType = [];
+
/** Signal for state [`pivotState`](#pivotstate) */
export const signalPivotState: Server.Signal = {
name: 'plugins.pivot.general.signalPivotState',
diff --git a/ivette/src/frama-c/plugins/studia/api/studia/index.ts b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
index 4d55bfa8523..16e8a7b0043 100644
--- a/ivette/src/frama-c/plugins/studia/api/studia/index.ts
+++ b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
@@ -37,37 +37,49 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { fct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { fctDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jFct } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
/** Statements that read or write a location. */
export interface effects {
/** List of statements with direct effect. */
- direct: [ Json.key<'#fct'>, marker ][];
+ direct: [ fct, marker ][];
/** List of statements with indirect effect. */
- indirect: [ Json.key<'#fct'>, marker ][];
+ indirect: [ fct, marker ][];
}
/** Decoder for `effects` */
export const jEffects: Json.Decoder<effects> =
Json.jObject({
- direct: Json.jArray(Json.jPair( Json.jKey<'#fct'>('#fct'), jMarker,)),
- indirect: Json.jArray(Json.jPair( Json.jKey<'#fct'>('#fct'), jMarker,)),
+ direct: Json.jArray(Json.jPair( jFct, jMarker,)),
+ indirect: Json.jArray(Json.jPair( jFct, jMarker,)),
});
/** Natural order for `effects` */
export const byEffects: Compare.Order<effects> =
Compare.byFields
- <{ direct: [ Json.key<'#fct'>, marker ][],
- indirect: [ Json.key<'#fct'>, marker ][] }>({
- direct: Compare.array(Compare.pair(Compare.string,byMarker,)),
- indirect: Compare.array(Compare.pair(Compare.string,byMarker,)),
+ <{ direct: [ fct, marker ][], indirect: [ fct, marker ][] }>({
+ direct: Compare.array(Compare.pair(byFct,byMarker,)),
+ indirect: Compare.array(Compare.pair(byFct,byMarker,)),
});
+/** Default value for `effects` */
+export const effectsDefault: effects = { direct: [], indirect: [] };
+
const getReadsLval_internal: Server.GetRequest<marker,effects> = {
kind: Server.RqKind.GET,
name: 'plugins.studia.studia.getReadsLval',
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 6025b56eafc..486fa94666f 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -798,24 +798,12 @@ export async function resetSelection(): Promise<void> {
export type attributes = Ast.markerAttributesData;
-export const defaultMarker: attributes = {
- marker: Ast.jMarker(''),
- labelKind: '',
- titleKind: '',
- name: '',
- descr: '',
- isLval: false,
- isFunDecl: false,
- isFunction: false,
- sloc: { dir: '', base: '', file: '', line: 0 },
-};
-
/** Access the marker attributes from AST. */
export function useMarker(marker: Ast.marker | undefined): attributes {
const marks = useSyncArray(Ast.markerAttributes);
- if (marker === undefined) return defaultMarker;
+ if (marker === undefined) return Ast.markerAttributesDataDefault;
const attrs = marks.getData(marker);
- if (attrs === undefined) return defaultMarker;
+ if (attrs === undefined) return Ast.markerAttributesDataDefault;
return attrs;
}
diff --git a/src/plugins/api-generator/api_generator.ml b/src/plugins/api-generator/api_generator.ml
index f271f73dbfe..b35d7410118 100644
--- a/src/plugins/api-generator/api_generator.ml
+++ b/src/plugins/api-generator/api_generator.ml
@@ -100,7 +100,7 @@ let makeJtype ?self ~names =
| Jkey kd -> Format.fprintf fmt "Json.key<'#%s'>" kd
| Jindex kd -> Format.fprintf fmt "Json.index<'#%s'>" kd
| Jdict js -> Format.fprintf fmt "@[<hov 2>Json.dict<@,%a>@]" pp js
- | Jdata(id,_) | Jenum id -> pp_ident fmt id
+ | Jdata(id,_) | Jenum(id,_) -> pp_ident fmt id
| Joption js -> Format.fprintf fmt "%a |@ undefined" pp js
| Jtuple js ->
Pretty_utils.pp_list ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]" pp fmt js
@@ -180,7 +180,7 @@ let rec makeDecoder ?self ~names fmt js =
| Jkey kd -> jkey fmt kd
| Jindex kd -> jindex fmt kd
| Jdata(id,_) -> jcall names fmt (Pkg.Derived.decode id)
- | Jenum id -> jenum names fmt id
+ | Jenum(id,_) -> jenum names fmt id
| Jself -> jcall names fmt (Pkg.Derived.decode (getSelf self))
| Joption js ->
Format.fprintf fmt "@[<hov 2>Json.jOption(@,%a)@]" make js
@@ -219,7 +219,7 @@ let makeOrder ~self ~names fmt js =
| Jdata(id,_) -> jcall names fmt (Pkg.Derived.order id)
| Joption js ->
Format.fprintf fmt "@[<hov 2>Compare.defined(@,%a)@]" pp js
- | Jenum id ->
+ | Jenum(id,_) ->
Format.fprintf fmt "@[<hov 2>Compare.byEnum(@,%a)@]" (jcall names) id
| Jarray js ->
Format.fprintf fmt "@[<hov 2>Compare.array(@,%a)@]" pp js
@@ -248,6 +248,49 @@ let makeOrder ~self ~names fmt js =
Format.fprintf fmt "Compare.structural"
in pp fmt js
+(* -------------------------------------------------------------------------- *)
+(* --- Jtype Order --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec atomic js =
+ let open Pkg in
+ match js with
+ | Junion js -> List.exists atomic js
+ | Jany | Jnull | Jnumber | Jboolean | Jstring | Jalpha
+ | Jtag _ | Jkey _ | Jindex _ | Jdict _ | Joption _ | Jarray _ | Jenum _
+ -> true
+ | Jself | Jtuple _ | Jrecord _ | Jdata _
+ -> false
+
+let makeDefault ~names fmt js =
+ let open Pkg in
+ let rec pp fmt = function
+ | Junion [] -> failwith "empty union type"
+ | Jenum(_,[]) -> failwith "empty enum type"
+ | Jself -> failwith "recursive default value"
+ | Jany | Jnull -> Format.pp_print_string fmt "null"
+ | Jnumber -> Format.pp_print_string fmt "0"
+ | Jboolean -> Format.pp_print_string fmt "false"
+ | Jstring | Jalpha -> Format.pp_print_string fmt "''"
+ | Jtag a -> Format.fprintf fmt "\"%s\"" a
+ | Jkey kd -> Format.fprintf fmt "%a('')" jkey kd
+ | Jindex kd -> Format.fprintf fmt "%a(-1)" jindex kd
+ | Jdict _ -> Format.fprintf fmt "{}"
+ | Jarray _ -> Format.fprintf fmt "[]"
+ | Joption _ -> Format.fprintf fmt "undefined"
+ | Jtuple js ->
+ Pretty_utils.pp_list ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
+ pp fmt js
+ | Jrecord js ->
+ Pretty_utils.pp_list ~pre:"@[<hov 2>{ " ~sep:",@ " ~suf:"@ }@]"
+ pp_field fmt js
+ | Junion js ->
+ (try pp fmt (List.find atomic js) with Not_found -> pp fmt (List.hd js))
+ | Jdata(id,_) -> jcall names fmt (Pkg.Derived.default id)
+ | Jenum(id,tag::_) -> Format.fprintf fmt "%a.%s" (jcall names) id tag
+ and pp_field fmt (fd,js) = Format.fprintf fmt "%s: %a" fd pp js
+ in pp fmt js
+
(* -------------------------------------------------------------------------- *)
(* --- Declaration Generator --- *)
(* -------------------------------------------------------------------------- *)
@@ -271,7 +314,7 @@ let makeDeclaration fmt names d =
| D_type js ->
makeDescr fmt d.d_descr ;
- Format.fprintf fmt "@[<hv 2>export type %s =@ %a;@]@\n" self.name jtype js
+ Format.fprintf fmt "@[<hv 2>export type %s =@ %a;@]@\n" self.name jtype js ;
| D_record fjs ->
makeDescr fmt d.d_descr ;
@@ -396,6 +439,12 @@ let makeDeclaration fmt names d =
self.name (jcall names) id
(makeRecursive2 (makeOrder ~self:id ~names)) js
+ | D_default(id,js) ->
+ makeDescr fmt d.d_descr ;
+ Format.fprintf fmt
+ "@[<hov 2>@[<hv 0>export const %s:@ %a@] =@ %a;@]\n"
+ self.name (jcall names) id (makeDefault ~names) js
+
(* -------------------------------------------------------------------------- *)
(* --- Declaration Ranking --- *)
(* -------------------------------------------------------------------------- *)
@@ -412,14 +461,14 @@ let depends d =
let id = d.d_ident in
[
Pkg.Derived.signal id;
- Pkg.Derived.getter id
+ Pkg.Derived.getter id;
]
| D_state _ ->
let id = d.d_ident in
[
Pkg.Derived.signal id;
Pkg.Derived.getter id;
- Pkg.Derived.setter id
+ Pkg.Derived.setter id;
]
| D_array _ ->
let id = d.d_ident in
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 1a9d8446318..1d9511b2eb7 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -70,6 +70,9 @@ let derived ~package ~id jtype =
declare ~package ~name:(Derived.order id).name
~descr:(Md.plain "Natural order for" @ Md.code id.name)
(D_order(id,jtype)) ;
+ declare ~package ~name:(Derived.default id).name
+ ~descr:(Md.plain "Default value for" @ Md.code id.name)
+ (D_default(id,jtype)) ;
Jdata(id,jtype)
end
@@ -550,9 +553,10 @@ struct
struct
type t = a
let jtype =
- let enums = D_enum (List.rev d.tags) in
- let id = Package.declare_id ~package ~name ~descr enums in
- derived ~package ~id (Jenum id)
+ let tags = List.rev d.tags in
+ let tagNames = List.map (fun { tg_name } -> tg_name) tags in
+ let id = Package.declare_id ~package ~name ~descr (D_enum tags) in
+ derived ~package ~id (Jenum(id,tagNames))
let of_json = of_json name d.values
let to_json = to_json name d.lookup d.vindex
end in
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index a9031f4bd28..7ff0db41405 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -175,8 +175,8 @@ type jtype =
| Jtuple of jtype list
| Junion of jtype list
| Jrecord of (string * jtype) list
- | Jenum of ident (* enum type declaration *)
- | Jdata of ident * jtype (* underlying definition *)
+ | Jenum of ident * string list (* type and tags *)
+ | Jdata of ident * jtype (* type and definition *)
| Jself (* for (simply) recursive types *)
(* -------------------------------------------------------------------------- *)
@@ -223,6 +223,7 @@ type declKindInfo =
| D_array of arrayInfo (* key kind *)
| D_decoder of ident * jtype
| D_order of ident * jtype (* natural ordering *)
+ | D_default of ident * jtype (* default value *)
type declInfo = {
d_ident : ident;
@@ -274,6 +275,7 @@ struct
let getter id = derived ~prefix:"get" id
let setter id = derived ~prefix:"set" id
let data id = derived ~suffix:"Data" id
+ let default id = derived ~suffix:"Default" id
let fetch id = derived ~prefix:"fetch" id
let reload id = derived ~prefix:"reload" id
let order id = derived ~prefix:"by" id
@@ -299,9 +301,10 @@ let rec visit_jtype fn = function
| Joption js | Jdict js | Jarray js -> visit_jtype fn js
| Jtuple js | Junion js -> List.iter (visit_jtype fn) js
| Jrecord fjs -> List.iter (fun (_,js) -> visit_jtype fn js) fjs
- | Jdata(id,_) | Jenum id ->
+ | Jdata(id,_) | Jenum(id,_) ->
begin
fn id ;
+ fn (Derived.default id) ;
fn (Derived.decode id) ;
fn (Derived.order id) ;
end
@@ -318,7 +321,8 @@ let visit_request f { rq_input ; rq_output } =
let visit_dkind f = function
| D_signal | D_enum _ | D_array _ -> ()
| D_type js | D_state js | D_value js -> visit_jtype f js
- | D_decoder (id,js) | D_order(id,js) -> f id ; visit_jtype f js
+ | D_decoder (id,js) | D_order(id,js) | D_default(id,js)
+ -> f id ; visit_jtype f js
| D_record fds -> List.iter (visit_field f) fds
| D_request rq -> visit_request f rq
@@ -462,14 +466,13 @@ let rec md_jtype pp = function
| Jtag a -> litteral a
| Jkey kd -> key kd
| Jindex kd -> index kd
- | Jdata(id,_) | Jenum id -> pp.ident id
+ | Jdata(id,_) | Jenum(id,_) -> pp.ident id
| Joption js -> protect pp js @ Md.code "?"
| Jtuple js -> Md.code "[" @ md_jlist pp "," js @ Md.code "]"
| Junion js -> md_jlist pp "|" js
| Jarray js -> protect pp js @ Md.code "[]"
| Jrecord fjs -> Md.code "{" @ fields pp fjs @ Md.code "}"
- | Jdict js ->
- Md.code "{[key]:" @ md_jtype pp js @ Md.code "}"
+ | Jdict js -> Md.code "{[key]:" @ md_jtype pp js @ Md.code "}"
and md_jlist pp sep js =
Md.glue ~sep:(Md.plain sep) (List.map (md_jtype pp) js)
diff --git a/src/plugins/server/package.mli b/src/plugins/server/package.mli
index 8a120b5af10..30368138955 100644
--- a/src/plugins/server/package.mli
+++ b/src/plugins/server/package.mli
@@ -43,8 +43,8 @@ type jtype =
| Jtuple of jtype list
| Junion of jtype list
| Jrecord of (string * jtype) list
- | Jenum of ident (* enum type declaration *)
- | Jdata of ident * jtype (* underlying definition *)
+ | Jenum of ident * string list (* type and tags *)
+ | Jdata of ident * jtype (* type and definition *)
| Jself (* for (simply) recursive types *)
type fieldInfo = {
@@ -87,6 +87,7 @@ type declKindInfo =
| D_array of arrayInfo
| D_decoder of ident * jtype
| D_order of ident * jtype (* natural ordering *)
+ | D_default of ident * jtype (* default value *)
type declInfo = {
d_ident : ident;
@@ -124,6 +125,7 @@ sig
val getter : ident -> ident
val setter : ident -> ident
val data : ident -> ident
+ val default : ident -> ident
val fetch : ident -> ident
val reload : ident -> ident
val order : ident -> ident
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 55fa5dc178a..3209946010d 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -138,7 +138,7 @@ let kind_of_decl = function
| D_request { rq_kind=`GET } -> "GET"
| D_request { rq_kind=`SET } -> "SET"
| D_request { rq_kind=`EXEC } -> "EXEC"
- | D_decoder _ | D_order _ -> assert false
+ | D_decoder _ | D_order _ | D_default _ -> assert false
let pp_for ?decl names =
let self =
@@ -169,7 +169,7 @@ let md_signals signals =
let descr_of_decl names decl =
match decl.d_kind with
- | D_decoder _ | D_order _ -> assert false
+ | D_decoder _ | D_order _ | D_default _ -> assert false
| D_signal -> []
| D_state _ -> [] (* TBC *)
| D_value _ -> [] (* TBC *)
--
GitLab