From 9db5655025e1ce36ceede19165026418d3555c4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 25 Jun 2020 01:00:10 +0200
Subject: [PATCH] [ivette] fix api generation
---
ivette/Makefile | 1 -
ivette/api/dive/index.ts | 23 +-
ivette/api/kernel/ast/index.ts | 163 ++++++++++-----
ivette/api/kernel/data/index.ts | 31 +--
ivette/api/kernel/project/index.ts | 32 +--
ivette/api/kernel/properties/index.ts | 209 +++++++++++--------
ivette/api/kernel/services/index.ts | 57 +++--
ivette/api/server_tsc.ml | 70 +++++--
ivette/src/dome/src/renderer/data/json.ts | 2 +-
ivette/src/dome/src/renderer/text/buffers.js | 6 +-
ivette/src/frama-c/states.ts | 41 ++--
ivette/src/renderer/ASTinfo.tsx | 12 +-
ivette/src/renderer/Properties.tsx | 78 +++----
ivette/tsconfig.json | 4 +-
ivette/webpack.renderer.js | 1 +
src/plugins/server/data.ml | 9 +-
src/plugins/server/kernel_ast.ml | 4 +-
src/plugins/server/kernel_properties.ml | 16 +-
src/plugins/server/package.ml | 11 +
src/plugins/server/package.mli | 2 +
src/plugins/server/states.ml | 2 +
21 files changed, 464 insertions(+), 310 deletions(-)
diff --git a/ivette/Makefile b/ivette/Makefile
index 1985240a256..a9ec5f1eaeb 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -41,7 +41,6 @@ api:
@find api -name "*.ts" -exec rm -f {} \;
../bin/frama-c.byte -load-module api/server_tsc.ml -server-tsc
@find api -name "*.ts" -exec chmod a-w {} \;
- @touch $@
# --------------------------------------------------------------------------
# --- Ivette Documentation
diff --git a/ivette/api/dive/index.ts b/ivette/api/dive/index.ts
index cb3badb52ff..13457b8a843 100644
--- a/ivette/api/dive/index.ts
+++ b/ivette/api/dive/index.ts
@@ -6,9 +6,13 @@
@module frama-c/dive
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
@@ -22,18 +26,19 @@ export interface variableName {
/** Safe decoder for `variableName` */
export const jVariableNameSafe: Json.Safe<variableName> =
+ Json.jFail(jVariableName,'VariableName expected');
+
+/** Loose decoder for `variableName` */
+export const jVariableName: Json.Loose<variableName> =
Json.jObject({
funName: Json.jString,
varName: Json.jFail(Json.jString,'String expected'),
});
-/** Loose decoder for `variableName` */
-export const jVariableName: Json.Loose<variableName> =
- Json.jTry(jVariableNameSafe);
-
/** Natural order for `variableName` */
export const byVariableName: Compare.Order<variableName> =
- Compare.byFields({
+ Compare.byFields
+ <{ funName?: string, varName: string }>({
funName: Compare.defined(Compare.alpha),
varName: Compare.alpha,
});
@@ -63,7 +68,7 @@ export const addVar: Server.ExecRequest<variableName,Json.json> = {
};
/** Add all alarms of the given function */
-export const addFunctionAlarms: Server.ExecRequest<Json.Key<'#fct'>,Json.json
+export const addFunctionAlarms: Server.ExecRequest<Json.key<'#fct'>,Json.json
> = {
kind: Server.RqKind.EXEC,
name: 'dive.addFunctionAlarms',
@@ -72,7 +77,7 @@ export const addFunctionAlarms: Server.ExecRequest<Json.Key<'#fct'>,Json.json
};
/** Explore the graph starting from an existing vertex */
-export const explore: Server.ExecRequest<Json.Index<'#dive-node'>,Json.json
+export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json
> = {
kind: Server.RqKind.EXEC,
name: 'dive.explore',
@@ -81,7 +86,7 @@ export const explore: Server.ExecRequest<Json.Index<'#dive-node'>,Json.json
};
/** Show the dependencies of an existing vertex */
-export const show: Server.ExecRequest<Json.Index<'#dive-node'>,Json.json> = {
+export const show: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
kind: Server.RqKind.EXEC,
name: 'dive.show',
input: Json.jIndex('#dive-node'),
@@ -89,7 +94,7 @@ export const show: Server.ExecRequest<Json.Index<'#dive-node'>,Json.json> = {
};
/** Hide the dependencies of an existing vertex */
-export const hide: Server.ExecRequest<Json.Index<'#dive-node'>,Json.json> = {
+export const hide: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
kind: Server.RqKind.EXEC,
name: 'dive.hide',
input: Json.jIndex('#dive-node'),
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index 731f28b341c..aea3d3f0bdb 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -6,18 +6,30 @@
@module frama-c/kernel/ast
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
import { byTag } from 'api/kernel/data';
+//@ts-ignore
import { byText } from 'api/kernel/data';
+//@ts-ignore
import { jTag } from 'api/kernel/data';
+//@ts-ignore
import { jTagSafe } from 'api/kernel/data';
+//@ts-ignore
import { jText } from 'api/kernel/data';
+//@ts-ignore
import { jTextSafe } from 'api/kernel/data';
+//@ts-ignore
import { tag } from 'api/kernel/data';
+//@ts-ignore
import { text } from 'api/kernel/data';
/** Ensures that AST is computed */
@@ -31,23 +43,23 @@ export const compute: Server.ExecRequest<null,null> = {
/** Marker kind */
export enum markerKind {
/** Expression */
- expression = 'expression';
+ expression = 'expression',
/** Lvalue */
- lvalue = 'lvalue';
+ lvalue = 'lvalue',
/** Variable */
- variable = 'variable';
+ variable = 'variable',
/** Function */
- function = 'function';
+ function = 'function',
/** Declaration */
- declaration = 'declaration';
+ declaration = 'declaration',
/** Statement */
- statement = 'statement';
+ statement = 'statement',
/** Global */
- global = 'global';
+ global = 'global',
/** Term */
- term = 'term';
+ term = 'term',
/** Property */
- property = 'property';
+ property = 'property',
}
/** Safe decoder for `markerKind` */
@@ -59,7 +71,7 @@ export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
/** Natural order for `markerKind` */
export const byMarkerKind: Compare.Order<markerKind> =
- Compare.byEnym(markerKind);
+ Compare.byEnum(markerKind);
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]> = {
@@ -69,24 +81,24 @@ export const markerKindTags: Server.GetRequest<null,tag[]> = {
output: Json.jList(jTag),
};
-/** Markers data */
-export const markerData: State.Array<'#markerData',markerDataData> = {
- name: 'kernel.ast.markerData',
+/** Marker informations */
+export const markerInfo: State.Array<'#markerInfo',markerInfoData> = {
+ name: 'kernel.ast.markerInfo',
key: 'key',
- signal: signalMarkerData,
- fetch: fetchMarkerData,
- reload: reloadMarkerData,
+ signal: signalMarkerInfo,
+ fetch: fetchMarkerInfo,
+ reload: reloadMarkerInfo,
};
-/** Signal for array [`markerData`](#markerdata) */
-export const signalMarkerData: Server.Signal = {
- name: 'kernel.ast.signalMarkerData',
+/** Signal for array [`markerInfo`](#markerinfo) */
+export const signalMarkerInfo: Server.Signal = {
+ name: 'kernel.ast.signalMarkerInfo',
};
-/** Data for array rows [`markerData`](#markerdata) */
-export interface markerDataData {
+/** Data for array rows [`markerInfo`](#markerinfo) */
+export interface markerInfoData {
/** Entry identifier. */
- key: Json.Key<'#markerData'>;
+ key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
/** Marker short name */
@@ -95,35 +107,58 @@ export interface markerDataData {
descr: string;
}
-/** Data fetcher for array [`markerData`](#markerdata) */
-export const fetchMarkerData: Server.GetRequest<number,
- { pending: number, updated: markerDataData[],
- removed: Json.Key<'#markerData'>[], reload: boolean }> = {
+/** Safe decoder for `markerInfoData` */
+export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
+ Json.jFail(jMarkerInfoData,'MarkerInfoData expected');
+
+/** Loose decoder for `markerInfoData` */
+export const jMarkerInfoData: Json.Loose<markerInfoData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey('#markerInfo'),'#markerInfo expected'),
+ kind: jMarkerKindSafe,
+ name: Json.jFail(Json.jString,'String expected'),
+ descr: Json.jFail(Json.jString,'String expected'),
+ });
+
+/** Natural order for `markerInfoData` */
+export const byMarkerInfoData: Compare.Order<markerInfoData> =
+ Compare.byFields
+ <{ key: Json.key<'#markerInfo'>, kind: markerKind, name: string,
+ descr: string }>({
+ key: Compare.primitive,
+ kind: byMarkerKind,
+ name: Compare.alpha,
+ descr: Compare.primitive,
+ });
+
+/** Data fetcher for array [`markerInfo`](#markerinfo) */
+export const fetchMarkerInfo: Server.GetRequest<number,
+ { pending: number, updated: markerInfoData[],
+ removed: Json.key<'#markerInfo'>[], reload: boolean }> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.fetchMarkerData',
+ name: 'kernel.ast.fetchMarkerInfo',
input: Json.jNumber,
- output: Json.jTry(
- Json.jObject({
- pending: Json.jFail(Json.jNumber,'Number expected'),
- updated: Json.jList(jMarkerDataData),
- removed: Json.jList(Json.jKey('#markerData')),
- reload: Json.jFail(Json.jBoolean,'Boolean expected'),
- })),
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jMarkerInfoData),
+ removed: Json.jList(Json.jKey('#markerInfo')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
};
-/** Force full reload for array [`markerData`](#markerdata) */
-export const reloadMarkerData: Server.GetRequest<null,null> = {
+/** Force full reload for array [`markerInfo`](#markerinfo) */
+export const reloadMarkerInfo: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.reloadMarkerData',
+ name: 'kernel.ast.reloadMarkerInfo',
input: Json.jNull,
output: Json.jNull,
};
/** Localizable AST markers */
export type marker =
- Json.Key<'#stmt'> | Json.Key<'#decl'> | Json.Key<'#lval'> |
- Json.Key<'#expr'> | Json.Key<'#term'> | Json.Key<'#global'> |
- Json.Key<'#property'>;
+ Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
+ Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
+ Json.key<'#property'>;
/** Safe decoder for `marker` */
export const jMarkerSafe: Json.Safe<marker> =
@@ -131,9 +166,9 @@ export const jMarkerSafe: Json.Safe<marker> =
/** Loose decoder for `marker` */
export const jMarker: Json.Loose<marker> =
- Json.jUnion<Json.Key<'#stmt'> | Json.Key<'#decl'> | Json.Key<'#lval'> |
- Json.Key<'#expr'> | Json.Key<'#term'> | Json.Key<'#global'> |
- Json.Key<'#property'>>(
+ Json.jUnion<Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
+ Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
+ Json.key<'#property'>>(
Json.jKey('#stmt'),
Json.jKey('#decl'),
Json.jKey('#lval'),
@@ -147,7 +182,7 @@ export const jMarker: Json.Loose<marker> =
export const byMarker: Compare.Order<marker> = Compare.structural;
/** Collect all functions in the AST */
-export const getFunctions: Server.GetRequest<null,Json.Key<'#fct'>[]> = {
+export const getFunctions: Server.GetRequest<null,Json.key<'#fct'>[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
input: Json.jNull,
@@ -155,7 +190,7 @@ export const getFunctions: Server.GetRequest<null,Json.Key<'#fct'>[]> = {
};
/** Print the AST of a function */
-export const printFunction: Server.GetRequest<Json.Key<'#fct'>,text> = {
+export const printFunction: Server.GetRequest<Json.key<'#fct'>,text> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.printFunction',
input: Json.jKey('#fct'),
@@ -179,27 +214,47 @@ export const signalFunctions: Server.Signal = {
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
/** Entry identifier. */
- key: Json.Key<'#functions'>;
+ key: Json.key<'#functions'>;
/** Name */
name: string;
/** Signature */
signature: string;
}
+/** Safe decoder for `functionsData` */
+export const jFunctionsDataSafe: Json.Safe<functionsData> =
+ Json.jFail(jFunctionsData,'FunctionsData expected');
+
+/** Loose decoder for `functionsData` */
+export const jFunctionsData: Json.Loose<functionsData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey('#functions'),'#functions expected'),
+ name: Json.jFail(Json.jString,'String expected'),
+ signature: Json.jFail(Json.jString,'String expected'),
+ });
+
+/** Natural order for `functionsData` */
+export const byFunctionsData: Compare.Order<functionsData> =
+ Compare.byFields
+ <{ key: Json.key<'#functions'>, name: string, signature: string }>({
+ key: Compare.primitive,
+ name: Compare.alpha,
+ signature: Compare.primitive,
+ });
+
/** Data fetcher for array [`functions`](#functions) */
export const fetchFunctions: Server.GetRequest<number,
{ pending: number, updated: functionsData[],
- removed: Json.Key<'#functions'>[], reload: boolean }> = {
+ removed: Json.key<'#functions'>[], reload: boolean }> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchFunctions',
input: Json.jNumber,
- output: Json.jTry(
- Json.jObject({
- pending: Json.jFail(Json.jNumber,'Number expected'),
- updated: Json.jList(jFunctionsData),
- removed: Json.jList(Json.jKey('#functions')),
- reload: Json.jFail(Json.jBoolean,'Boolean expected'),
- })),
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jFunctionsData),
+ removed: Json.jList(Json.jKey('#functions')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
};
/** Force full reload for array [`functions`](#functions) */
diff --git a/ivette/api/kernel/data/index.ts b/ivette/api/kernel/data/index.ts
index 721ec1fc1fa..5550b01e4f1 100644
--- a/ivette/api/kernel/data/index.ts
+++ b/ivette/api/kernel/data/index.ts
@@ -6,9 +6,13 @@
@module frama-c/kernel/data
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
@@ -29,36 +33,39 @@ export const byMarkdown: Compare.Order<markdown> = Compare.primitive;
export type text = null | string | text[];
/** Safe decoder for `text` */
-export const jTextSafe: Json.Safe<text> = Json.jFail(jText,'Text expected');
+export const jTextSafe: Json.Safe<text> =
+ (_x) => Json.jFail(jText,'Text expected')(_x);
/** Loose decoder for `text` */
export const jText: Json.Loose<text> =
- Json.jUnion<null | string | text[]>(
- Json.jNull,
- Json.jString,
- Json.jList(jText),
- );
+ (_x) => Json.jUnion<null | string | text[]>(
+ Json.jNull,
+ Json.jString,
+ Json.jList(jText),
+ )(_x);
/** Natural order for `text` */
-export const byText: Compare.Order<text> = Compare.structural;
+export const byText: Compare.Order<text> =
+ (_x,_y) => Compare.structural(_x,_y);
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
/** Safe decoder for `tag` */
-export const jTagSafe: Json.Safe<tag> =
+export const jTagSafe: Json.Safe<tag> = Json.jFail(jTag,'Tag expected');
+
+/** Loose decoder for `tag` */
+export const jTag: Json.Loose<tag> =
Json.jObject({
name: Json.jFail(Json.jString,'String expected'),
label: jMarkdownSafe,
descr: jMarkdownSafe,
});
-/** Loose decoder for `tag` */
-export const jTag: Json.Loose<tag> = Json.jTry(jTagSafe);
-
/** Natural order for `tag` */
export const byTag: Compare.Order<tag> =
- Compare.byFields({
+ Compare.byFields
+ <{ name: string, label: markdown, descr: markdown }>({
name: Compare.alpha,
label: byMarkdown,
descr: byMarkdown,
diff --git a/ivette/api/kernel/project/index.ts b/ivette/api/kernel/project/index.ts
index db4a28b8198..912ef274e80 100644
--- a/ivette/api/kernel/project/index.ts
+++ b/ivette/api/kernel/project/index.ts
@@ -6,31 +6,36 @@
@module frama-c/kernel/project
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
/** Project informations */
export type projectInfo =
- { id: Json.Key<'#project'>, name: string, current: boolean };
+ { id: Json.key<'#project'>, name: string, current: boolean };
/** Safe decoder for `projectInfo` */
export const jProjectInfoSafe: Json.Safe<projectInfo> =
+ Json.jFail(jProjectInfo,'ProjectInfo expected');
+
+/** Loose decoder for `projectInfo` */
+export const jProjectInfo: Json.Loose<projectInfo> =
Json.jObject({
id: Json.jFail(Json.jKey('#project'),'#project expected'),
name: Json.jFail(Json.jString,'String expected'),
current: Json.jFail(Json.jBoolean,'Boolean expected'),
});
-/** Loose decoder for `projectInfo` */
-export const jProjectInfo: Json.Loose<projectInfo> =
- Json.jTry(jProjectInfoSafe);
-
/** Natural order for `projectInfo` */
export const byProjectInfo: Compare.Order<projectInfo> =
- Compare.byFields({
+ Compare.byFields
+ <{ id: Json.key<'#project'>, name: string, current: boolean }>({
id: Compare.primitive,
name: Compare.alpha,
current: Compare.primitive,
@@ -38,23 +43,24 @@ export const byProjectInfo: Compare.Order<projectInfo> =
/** Request to be executed on the specified project. */
export type projectRequest =
- { project: Json.Key<'#project'>, request: string, data: Json.json };
+ { project: Json.key<'#project'>, request: string, data: Json.json };
/** Safe decoder for `projectRequest` */
export const jProjectRequestSafe: Json.Safe<projectRequest> =
+ Json.jFail(jProjectRequest,'ProjectRequest expected');
+
+/** Loose decoder for `projectRequest` */
+export const jProjectRequest: Json.Loose<projectRequest> =
Json.jObject({
project: Json.jFail(Json.jKey('#project'),'#project expected'),
request: Json.jFail(Json.jString,'String expected'),
data: Json.jAny,
});
-/** Loose decoder for `projectRequest` */
-export const jProjectRequest: Json.Loose<projectRequest> =
- Json.jTry(jProjectRequestSafe);
-
/** Natural order for `projectRequest` */
export const byProjectRequest: Compare.Order<projectRequest> =
- Compare.byFields({
+ Compare.byFields
+ <{ project: Json.key<'#project'>, request: string, data: Json.json }>({
project: Compare.primitive,
request: Compare.primitive,
data: Compare.structural,
@@ -69,7 +75,7 @@ export const getCurrent: Server.GetRequest<null,projectInfo> = {
};
/** Switches the current project */
-export const setCurrent: Server.SetRequest<Json.Key<'#project'>,null> = {
+export const setCurrent: Server.SetRequest<Json.key<'#project'>,null> = {
kind: Server.RqKind.SET,
name: 'kernel.project.setCurrent',
input: Json.jKey('#project'),
diff --git a/ivette/api/kernel/properties/index.ts b/ivette/api/kernel/properties/index.ts
index 7dc2b45c16c..4c6a826fe51 100644
--- a/ivette/api/kernel/properties/index.ts
+++ b/ivette/api/kernel/properties/index.ts
@@ -6,90 +6,96 @@
@module frama-c/kernel/properties
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
import { byTag } from 'api/kernel/data';
+//@ts-ignore
import { jTag } from 'api/kernel/data';
+//@ts-ignore
import { jTagSafe } from 'api/kernel/data';
+//@ts-ignore
import { tag } from 'api/kernel/data';
+//@ts-ignore
import { bySource } from 'api/kernel/services';
+//@ts-ignore
import { jSource } from 'api/kernel/services';
+//@ts-ignore
import { jSourceSafe } from 'api/kernel/services';
+//@ts-ignore
import { source } from 'api/kernel/services';
/** Property Kinds */
export enum propKind {
/** Contract behavior */
- behavior = 'behavior';
+ behavior = 'behavior',
/** Complete behaviors clause */
- complete = 'complete';
+ complete = 'complete',
/** Disjoint behaviors clause */
- disjoint = 'disjoint';
+ disjoint = 'disjoint',
/** Clause `@assumes` */
- assumes = 'assumes';
+ assumes = 'assumes',
/** Function precondition */
- requires = 'requires';
+ requires = 'requires',
/** Instance of a precondition at a call site */
- instance = 'instance';
+ instance = 'instance',
/** Clause `@breaks` */
- breaks = 'breaks';
+ breaks = 'breaks',
/** Clause `@continues` */
- continues = 'continues';
+ continues = 'continues',
/** Clause `@returns` */
- returns = 'returns';
+ returns = 'returns',
/** Clause `@exits` */
- exits = 'exits';
+ exits = 'exits',
/** Function postcondition */
- ensures = 'ensures';
+ ensures = 'ensures',
/** Function termination clause */
- terminates = 'terminates';
+ terminates = 'terminates',
/** Function allocation */
- allocates = 'allocates';
+ allocates = 'allocates',
/** Clause `@decreases` */
- decreases = 'decreases';
+ decreases = 'decreases',
/** Function assigns */
- assigns = 'assigns';
+ assigns = 'assigns',
/** Functional dependencies in function assigns */
- froms = 'froms';
+ froms = 'froms',
/** Assertion */
- assert = 'assert';
+ assert = 'assert',
/** Check */
- check = 'check';
- /** Loop invariant */
- invariant = 'invariant';
+ check = 'check',
+ /** Clause `@loop invariant` */
+ loop_invariant = 'loop_invariant',
/** Clause `@loop assigns` */
- loop-assigns = 'loop-assigns';
- /** Loop termination argument */
- variant = 'variant';
+ loop_assigns = 'loop_assigns',
+ /** Clause `@loop variant` */
+ loop_variant = 'loop_variant',
/** Clause `@loop allocates` */
- loop-allocates = 'loop-allocates';
+ loop_allocates = 'loop_allocates',
/** Clause `@loop pragma` */
- loop-pragma = 'loop-pragma';
+ loop_pragma = 'loop_pragma',
/** Reachable statement */
- reachable = 'reachable';
+ reachable = 'reachable',
/** Statement contract */
- code-contract = 'code-contract';
+ code_contract = 'code_contract',
/** Generalized loop invariant */
- code-invariant = 'code-invariant';
+ code_invariant = 'code_invariant',
/** Type invariant */
- type-invariant = 'type-invariant';
+ type_invariant = 'type_invariant',
/** Global invariant */
- global-invariant = 'global-invariant';
+ global_invariant = 'global_invariant',
/** Axiomatic definitions */
- axiomatic = 'axiomatic';
+ axiomatic = 'axiomatic',
/** Logical axiom */
- axiom = 'axiom';
+ axiom = 'axiom',
/** Logical lemma */
- lemma = 'lemma';
- /** ACSL extension `<clause>` */
- ext:<clause> = 'ext:<clause>';
- /** ACSL loop extension `loop <clause>` */
- loop-ext:<clause> = 'loop-ext:<clause>';
- /** Plugin Specific properties */
- prop:<prop> = 'prop:<prop>';
+ lemma = 'lemma',
}
/** Safe decoder for `propKind` */
@@ -100,7 +106,7 @@ export const jPropKindSafe: Json.Safe<propKind> =
export const jPropKind: Json.Loose<propKind> = Json.jEnum(propKind);
/** Natural order for `propKind` */
-export const byPropKind: Compare.Order<propKind> = Compare.byEnym(propKind);
+export const byPropKind: Compare.Order<propKind> = Compare.byEnum(propKind);
/** Registered tags for the above type. */
export const propKindTags: Server.GetRequest<null,tag[]> = {
@@ -113,27 +119,27 @@ export const propKindTags: Server.GetRequest<null,tag[]> = {
/** Property Status (consolidated) */
export enum propStatus {
/** Unknown status */
- unknown = 'unknown';
+ unknown = 'unknown',
/** Unknown status (never tried) */
- never_tried = 'never_tried';
+ never_tried = 'never_tried',
/** Inconsistent status */
- inconsistent = 'inconsistent';
+ inconsistent = 'inconsistent',
/** Valid property */
- valid = 'valid';
+ valid = 'valid',
/** Valid (under hypotheses) */
- valid_under_hyp = 'valid_under_hyp';
+ valid_under_hyp = 'valid_under_hyp',
/** Valid (external assumption) */
- considered_valid = 'considered_valid';
+ considered_valid = 'considered_valid',
/** Invalid property (counter example found) */
- invalid = 'invalid';
+ invalid = 'invalid',
/** Invalid property (under hypotheses) */
- invalid_under_hyp = 'invalid_under_hyp';
+ invalid_under_hyp = 'invalid_under_hyp',
/** Dead property (but invalid) */
- invalid_but_dead = 'invalid_but_dead';
+ invalid_but_dead = 'invalid_but_dead',
/** Dead property (but valid) */
- valid_but_dead = 'valid_but_dead';
+ valid_but_dead = 'valid_but_dead',
/** Dead property (but unknown) */
- unknown_but_dead = 'unknown_but_dead';
+ unknown_but_dead = 'unknown_but_dead',
}
/** Safe decoder for `propStatus` */
@@ -145,7 +151,7 @@ export const jPropStatus: Json.Loose<propStatus> = Json.jEnum(propStatus);
/** Natural order for `propStatus` */
export const byPropStatus: Compare.Order<propStatus> =
- Compare.byEnym(propStatus);
+ Compare.byEnum(propStatus);
/** Registered tags for the above type. */
export const propStatusTags: Server.GetRequest<null,tag[]> = {
@@ -158,41 +164,41 @@ export const propStatusTags: Server.GetRequest<null,tag[]> = {
/** Alarm Kinds */
export enum alarms {
/** Integer division by zero */
- division_by_zero = 'division_by_zero';
+ division_by_zero = 'division_by_zero',
/** Invalid pointer dereferencing */
- mem_access = 'mem_access';
+ mem_access = 'mem_access',
/** Array access out of bounds */
- index_bound = 'index_bound';
+ index_bound = 'index_bound',
/** Invalid pointer computation */
- pointer_value = 'pointer_value';
+ pointer_value = 'pointer_value',
/** Invalid shift */
- shift = 'shift';
+ shift = 'shift',
/** Invalid pointer comparison */
- ptr_comparison = 'ptr_comparison';
+ ptr_comparison = 'ptr_comparison',
/** Operation on pointers within different blocks */
- differing_blocks = 'differing_blocks';
+ differing_blocks = 'differing_blocks',
/** Integer overflow or downcast */
- overflow = 'overflow';
+ overflow = 'overflow',
/** Overflow in float to int conversion */
- float_to_int = 'float_to_int';
+ float_to_int = 'float_to_int',
/** Unsequenced side-effects on non-separated memory */
- separation = 'separation';
+ separation = 'separation',
/** Overlap between left- and right-hand-side in assignment */
- overlap = 'overlap';
+ overlap = 'overlap',
/** Uninitialized memory read */
- initialization = 'initialization';
+ initialization = 'initialization',
/** Read of a dangling pointer */
- dangling_pointer = 'dangling_pointer';
+ dangling_pointer = 'dangling_pointer',
/** Non-finite (nan or infinite) floating-point value */
- is_nan_or_infinite = 'is_nan_or_infinite';
+ is_nan_or_infinite = 'is_nan_or_infinite',
/** NaN floating-point value */
- is_nan = 'is_nan';
+ is_nan = 'is_nan',
/** Pointer to a function with non-compatible type */
- function_pointer = 'function_pointer';
+ function_pointer = 'function_pointer',
/** Uninitialized memory read of union */
- initialization_of_union = 'initialization_of_union';
+ initialization_of_union = 'initialization_of_union',
/** Trap representation of a _Bool lvalue */
- bool_value = 'bool_value';
+ bool_value = 'bool_value',
}
/** Safe decoder for `alarms` */
@@ -203,7 +209,7 @@ export const jAlarmsSafe: Json.Safe<alarms> =
export const jAlarms: Json.Loose<alarms> = Json.jEnum(alarms);
/** Natural order for `alarms` */
-export const byAlarms: Compare.Order<alarms> = Compare.byEnym(alarms);
+export const byAlarms: Compare.Order<alarms> = Compare.byEnum(alarms);
/** Registered tags for the above type. */
export const alarmsTags: Server.GetRequest<null,tag[]> = {
@@ -230,7 +236,7 @@ export const signalStatus: Server.Signal = {
/** Data for array rows [`status`](#status) */
export interface statusData {
/** Entry identifier. */
- key: Json.Key<'#status'>;
+ key: Json.key<'#status'>;
/** Full description */
descr: string;
/** Kind */
@@ -240,9 +246,9 @@ export interface statusData {
/** Status */
status: propStatus;
/** Function */
- function?: Json.Key<'#fct'>;
+ function?: Json.key<'#fct'>;
/** Instruction */
- kinstr?: Json.Key<'#stmt'>;
+ kinstr?: Json.key<'#stmt'>;
/** Position */
source: source;
/** Alarm name (if the property is an alarm) */
@@ -253,20 +259,59 @@ export interface statusData {
predicate?: string;
}
+/** Safe decoder for `statusData` */
+export const jStatusDataSafe: Json.Safe<statusData> =
+ Json.jFail(jStatusData,'StatusData expected');
+
+/** Loose decoder for `statusData` */
+export const jStatusData: Json.Loose<statusData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey('#status'),'#status expected'),
+ descr: Json.jFail(Json.jString,'String expected'),
+ kind: jPropKindSafe,
+ names: Json.jList(Json.jString),
+ status: jPropStatusSafe,
+ function: Json.jKey('#fct'),
+ kinstr: Json.jKey('#stmt'),
+ source: jSourceSafe,
+ alarm: Json.jString,
+ alarm_descr: Json.jString,
+ predicate: Json.jString,
+ });
+
+/** Natural order for `statusData` */
+export const byStatusData: Compare.Order<statusData> =
+ Compare.byFields
+ <{ key: Json.key<'#status'>, descr: string, kind: propKind,
+ names: string[], status: propStatus, function?: Json.key<'#fct'>,
+ kinstr?: Json.key<'#stmt'>, source: source, alarm?: string,
+ alarm_descr?: string, predicate?: string }>({
+ key: Compare.primitive,
+ descr: Compare.primitive,
+ kind: byPropKind,
+ names: Compare.array(Compare.primitive),
+ status: byPropStatus,
+ function: Compare.defined(Compare.primitive),
+ kinstr: Compare.defined(Compare.primitive),
+ source: bySource,
+ alarm: Compare.defined(Compare.primitive),
+ alarm_descr: Compare.defined(Compare.primitive),
+ predicate: Compare.defined(Compare.primitive),
+ });
+
/** Data fetcher for array [`status`](#status) */
export const fetchStatus: Server.GetRequest<number,
- { pending: number, updated: statusData[], removed: Json.Key<'#status'>[],
+ { pending: number, updated: statusData[], removed: Json.key<'#status'>[],
reload: boolean }> = {
kind: Server.RqKind.GET,
name: 'kernel.properties.fetchStatus',
input: Json.jNumber,
- output: Json.jTry(
- Json.jObject({
- pending: Json.jFail(Json.jNumber,'Number expected'),
- updated: Json.jList(jStatusData),
- removed: Json.jList(Json.jKey('#status')),
- reload: Json.jFail(Json.jBoolean,'Boolean expected'),
- })),
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jStatusData),
+ removed: Json.jList(Json.jKey('#status')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
};
/** Force full reload for array [`status`](#status) */
diff --git a/ivette/api/kernel/services/index.ts b/ivette/api/kernel/services/index.ts
index 53b20a5f176..9660798f216 100644
--- a/ivette/api/kernel/services/index.ts
+++ b/ivette/api/kernel/services/index.ts
@@ -6,14 +6,22 @@
@module frama-c/kernel/services
*/
+//@ts-ignore
import * as Json from 'dome/data/json';
+//@ts-ignore
import * as Compare from 'dome/data/compare';
+//@ts-ignore
import * as Server from 'frama-c/server';
+//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
import { byTag } from 'api/kernel/data';
+//@ts-ignore
import { jTag } from 'api/kernel/data';
+//@ts-ignore
import { jTagSafe } from 'api/kernel/data';
+//@ts-ignore
import { tag } from 'api/kernel/data';
/** Frama-C Kernel configuration */
@@ -23,13 +31,12 @@ export const getConfig: Server.GetRequest<null,
kind: Server.RqKind.GET,
name: 'kernel.services.getConfig',
input: Json.jNull,
- output: Json.jTry(
- Json.jObject({
- pluginpath: Json.jList(Json.jString),
- libdir: Json.jFail(Json.jString,'String expected'),
- datadir: Json.jFail(Json.jString,'String expected'),
- version: Json.jFail(Json.jString,'String expected'),
- })),
+ output: Json.jObject({
+ pluginpath: Json.jList(Json.jString),
+ libdir: Json.jFail(Json.jString,'String expected'),
+ datadir: Json.jFail(Json.jString,'String expected'),
+ version: Json.jFail(Json.jString,'String expected'),
+ }),
};
/** Load a save file. Returns an error, if not successfull. */
@@ -46,6 +53,10 @@ export type source =
/** Safe decoder for `source` */
export const jSourceSafe: Json.Safe<source> =
+ Json.jFail(jSource,'Source expected');
+
+/** Loose decoder for `source` */
+export const jSource: Json.Loose<source> =
Json.jObject({
dir: Json.jFail(Json.jString,'String expected'),
base: Json.jFail(Json.jString,'String expected'),
@@ -53,12 +64,10 @@ export const jSourceSafe: Json.Safe<source> =
line: Json.jFail(Json.jNumber,'Number expected'),
});
-/** Loose decoder for `source` */
-export const jSource: Json.Loose<source> = Json.jTry(jSourceSafe);
-
/** Natural order for `source` */
export const bySource: Compare.Order<source> =
- Compare.byFields({
+ Compare.byFields
+ <{ dir: string, base: string, file: string, line: number }>({
dir: Compare.primitive,
base: Compare.primitive,
file: Compare.primitive,
@@ -68,17 +77,17 @@ export const bySource: Compare.Order<source> =
/** Log messages categories. */
export enum logkind {
/** User Error */
- ERROR = 'ERROR';
+ ERROR = 'ERROR',
/** User Warning */
- WARNING = 'WARNING';
+ WARNING = 'WARNING',
/** Plugin Feedback */
- FEEDBACK = 'FEEDBACK';
+ FEEDBACK = 'FEEDBACK',
/** Plugin Result */
- RESULT = 'RESULT';
+ RESULT = 'RESULT',
/** Plugin Failure */
- FAILURE = 'FAILURE';
+ FAILURE = 'FAILURE',
/** Analyser Debug */
- DEBUG = 'DEBUG';
+ DEBUG = 'DEBUG',
}
/** Safe decoder for `logkind` */
@@ -89,7 +98,7 @@ export const jLogkindSafe: Json.Safe<logkind> =
export const jLogkind: Json.Loose<logkind> = Json.jEnum(logkind);
/** Natural order for `logkind` */
-export const byLogkind: Compare.Order<logkind> = Compare.byEnym(logkind);
+export const byLogkind: Compare.Order<logkind> = Compare.byEnum(logkind);
/** Registered tags for the above type. */
export const logkindTags: Server.GetRequest<null,tag[]> = {
@@ -114,7 +123,10 @@ export interface log {
}
/** Safe decoder for `log` */
-export const jLogSafe: Json.Safe<log> =
+export const jLogSafe: Json.Safe<log> = Json.jFail(jLog,'Log expected');
+
+/** Loose decoder for `log` */
+export const jLog: Json.Loose<log> =
Json.jObject({
kind: jLogkindSafe,
plugin: Json.jFail(Json.jString,'String expected'),
@@ -123,12 +135,11 @@ export const jLogSafe: Json.Safe<log> =
source: jSource,
});
-/** Loose decoder for `log` */
-export const jLog: Json.Loose<log> = Json.jTry(jLogSafe);
-
/** Natural order for `log` */
export const byLog: Compare.Order<log> =
- Compare.byFields({
+ Compare.byFields
+ <{ kind: logkind, plugin: string, message: string, category?: string,
+ source?: source }>({
kind: byLogkind,
plugin: Compare.alpha,
message: Compare.primitive,
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index 6516ae96f8a..bf359e9c59e 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -74,8 +74,8 @@ let makeJtype ?self ~names =
| Jnumber -> Format.pp_print_string fmt "number"
| Jboolean -> Format.pp_print_string fmt "boolean"
| Jstring | Jalpha -> Format.pp_print_string fmt "string"
- | Jkey kd -> Format.fprintf fmt "Json.Key<'#%s'>" kd
- | Jindex kd -> Format.fprintf fmt "Json.Index<'#%s'>" kd
+ | Jkey kd -> Format.fprintf fmt "Json.key<'#%s'>" kd
+ | Jindex kd -> Format.fprintf fmt "Json.index<'#%s'>" kd
| Jdict(kd,js) -> Format.fprintf fmt "Json.Dict<'#%s',%a>" kd pp js
| Jdata id | Jenum id -> pp_ident fmt id
| Joption js -> Format.fprintf fmt "%a |@ undefined" pp js
@@ -89,7 +89,12 @@ let makeJtype ?self ~names =
and protect fmt js = match js with
| Junion _ | Joption _ -> Format.fprintf fmt "@[<hov 2>(%a)@]" pp js
| _ -> pp fmt js
- and field fmt (fd,js) = Format.fprintf fmt "@[<hov 4>%s:@ %a@]" fd pp js
+ and field fmt (fd,js) =
+ match js with
+ | Joption js ->
+ Format.fprintf fmt "@[<hov 4>%s?:@ %a@]" fd pp js
+ | _ ->
+ Format.fprintf fmt "@[<hov 4>%s:@ %a@]" fd pp js
in pp
(* -------------------------------------------------------------------------- *)
@@ -178,7 +183,7 @@ let rec makeDecoder ~safe ?self ~names fmt js =
| Junion jts ->
let jtype = makeJtype ?self ~names in
jsafe ~safe "Union" (junion ~jtype ~makeLoose) fmt jts
- | Jrecord jfs -> jtry ~safe (jrecord ~makeSafe) fmt jfs
+ | Jrecord jfs -> jsafe ~safe "Record" (jrecord ~makeSafe) fmt jfs
| Jtuple jts -> jtry ~safe (jtuple ~makeSafe) fmt jts
let makeRootDecoder ~safe ~self ~names fmt js =
@@ -186,10 +191,10 @@ let makeRootDecoder ~safe ~self ~names fmt js =
match js with
| Joption _ | Jdict _ | Jlist _ when safe ->
jcall names fmt (Pkg.Derived.loose self)
- | Jrecord _ | Jtuple _ | Jarray _ when not safe ->
+ | Jtuple _ | Jarray _ when not safe ->
Format.fprintf fmt "Json.jTry(%a)"
(jcall names) (Pkg.Derived.safe self)
- | Junion _ when safe ->
+ | Junion _ | Jrecord _ when safe ->
Format.fprintf fmt "Json.jFail(%a,'%s expected')"
(jcall names) (Pkg.Derived.loose self)
(String.capitalize_ascii self.name)
@@ -201,9 +206,7 @@ let makeRootDecoder ~safe ~self ~names fmt js =
let typeOfParam = function
| Pkg.P_value js -> js
- | Pkg.P_named fjs ->
- let field fd = fd.Pkg.fd_name , fd.Pkg.fd_type in
- Jrecord (List.map field fjs)
+ | Pkg.P_named fjs -> Jrecord (List.map Pkg.field fjs)
(* -------------------------------------------------------------------------- *)
(* --- Jtype Order --- *)
@@ -223,7 +226,7 @@ let makeOrder ~self ~names fmt js =
| Jany | Junion _ -> (* Can not find a better solution *)
Format.fprintf fmt "Compare.structural"
| Jenum id ->
- Format.fprintf fmt "@[<hov 2>Compare.byEnym(@,%a)@]" (jcall names) id
+ Format.fprintf fmt "@[<hov 2>Compare.byEnum(@,%a)@]" (jcall names) id
| Jlist js | Jarray js ->
Format.fprintf fmt "@[<hov 2>Compare.array(@,%a)@]" pp js
| Jtuple jts ->
@@ -237,7 +240,8 @@ let makeOrder ~self ~names fmt js =
List.iter (fun js -> Format.fprintf fmt "@,%a," pp js) jts ;
Format.fprintf fmt "@]@,)@]" ;
| Jrecord jfs ->
- Format.fprintf fmt "@[<hv 0>@[<hv 2>Compare.byFields({" ;
+ Format.fprintf fmt "@[<hv 0>@[<hv 2>Compare.byFields@,<%a>({"
+ (makeJtype ~self ~names) (Jrecord jfs) ;
List.iter
(fun (fd,js) -> Format.fprintf fmt "@ @[<hov 2>%s: %a,@]" fd pp js) jfs ;
Format.fprintf fmt "@]@ })@]" ;
@@ -252,6 +256,16 @@ let makeOrder ~self ~names fmt js =
(* --- Declaration Generator --- *)
(* -------------------------------------------------------------------------- *)
+let makeRecursive fn fmt js =
+ if Pkg.isRecursive js then
+ Format.fprintf fmt "(_x) => %a(_x)" fn js
+ else fn fmt js
+
+let makeRecursive2 fn fmt js =
+ if Pkg.isRecursive js then
+ Format.fprintf fmt "(_x,_y) => %a(_x,_y)" fn js
+ else fn fmt js
+
let makeDeclaration fmt names d =
let open Pkg in
Format.pp_print_newline fmt () ;
@@ -281,7 +295,7 @@ let makeDeclaration fmt names d =
List.iter
(fun { tg_name = tag ; tg_descr = doc } ->
makeDescr ~indent:" " fmt doc ;
- Format.fprintf fmt " %s = '%s';@\n" tag tag ;
+ Format.fprintf fmt " %s = '%s',@\n" tag tag ;
) tgs ;
Format.fprintf fmt "}@\n"
@@ -348,24 +362,34 @@ let makeDeclaration fmt names d =
Format.fprintf fmt
"@[<hov 2>export const %s: Json.Safe<@,%a@,> =@ %a;@]\n"
self.name (jcall names) id
- (makeRootDecoder ~safe:true ~self:id ~names) js
+ (makeRecursive (makeRootDecoder ~safe:true ~self:id ~names)) js
| D_loose(id,js) ->
Format.fprintf fmt
"@[<hov 2>export const %s: Json.Loose<@,%a@,> =@ %a;@]\n"
self.name (jcall names) id
- (makeRootDecoder ~safe:false ~self:id ~names) js
+ (makeRecursive (makeRootDecoder ~safe:false ~self:id ~names)) js
| D_order(id,js) ->
Format.fprintf fmt
"@[<hov 2>export const %s: Compare.Order<@,%a@,> =@ %a;@]\n"
self.name (jcall names) id
- (makeOrder ~self:id ~names) js
+ (makeRecursive2 (makeOrder ~self:id ~names)) js
+
+(* -------------------------------------------------------------------------- *)
+(* --- Declaration Ranking --- *)
+(* -------------------------------------------------------------------------- *)
+
+let byRank _ _ = 0
(* -------------------------------------------------------------------------- *)
(* --- Package Generator --- *)
(* -------------------------------------------------------------------------- *)
+let makeIgnore fmt msg =
+ Format.fprintf fmt "//@ts-ignore@\n" ;
+ Format.fprintf fmt msg
+
let makePackage pkg name fmt =
begin
let open Pkg in
@@ -377,10 +401,10 @@ let makePackage pkg name fmt =
Format.fprintf fmt " @@module frama-c/%s@\n" name ;
Format.fprintf fmt "*/@\n@." ;
let names = Pkg.resolve ~keywords pkg in
- Format.fprintf fmt "import * as Json from 'dome/data/json';@\n" ;
- Format.fprintf fmt "import * as Compare from 'dome/data/compare';@\n" ;
- Format.fprintf fmt "import * as Server from 'frama-c/server';@\n" ;
- Format.fprintf fmt "import * as State from 'frama-c/states';@\n" ;
+ makeIgnore fmt "import * as Json from 'dome/data/json';@\n" ;
+ makeIgnore fmt "import * as Compare from 'dome/data/compare';@\n" ;
+ makeIgnore fmt "import * as Server from 'frama-c/server';@\n" ;
+ makeIgnore fmt "import * as State from 'frama-c/states';@\n" ;
Format.pp_print_newline fmt () ;
Pkg.IdMap.iter
(fun id name ->
@@ -389,13 +413,15 @@ let makePackage pkg name fmt =
then
let pkg = Pkg.name_of_pkg ~sep:"/" id.plugin id.package in
if id.name = name then
- Format.fprintf fmt "import { %s } from 'api/%s';@\n"
+ makeIgnore fmt "import { %s } from 'api/%s';@\n"
name pkg
else
- Format.fprintf fmt "import { %s: %s } from 'api/%s';@\n"
+ makeIgnore fmt "import { %s: %s } from 'api/%s';@\n"
id.name name pkg
) names ;
- List.iter (makeDeclaration fmt names) pkg.p_content ;
+ List.iter
+ (makeDeclaration fmt names)
+ (List.sort byRank pkg.p_content) ;
Format.pp_print_newline fmt () ;
Format.fprintf fmt "/* ------------------------------------- */@." ;
end
diff --git a/ivette/src/dome/src/renderer/data/json.ts b/ivette/src/dome/src/renderer/data/json.ts
index 7339577a393..145e4220ff7 100644
--- a/ivette/src/dome/src/renderer/data/json.ts
+++ b/ivette/src/dome/src/renderer/data/json.ts
@@ -156,7 +156,7 @@ export function jOption<A>(fn: Safe<A>, defaultValue?: A): Loose<A> {
Fail when the loose decoder returns `undefined`.
See also [[jCatch]] and [[jTry]].
*/
-export function jFail<A>(fn: Loose<A>, error: Error): Safe<A> {
+export function jFail<A>(fn: Loose<A>, error: string | Error): Safe<A> {
return (js: json) => {
const d = fn(js);
if (d !== undefined) return d;
diff --git a/ivette/src/dome/src/renderer/text/buffers.js b/ivette/src/dome/src/renderer/text/buffers.js
index 2546e8f5b7c..b25bf354c55 100644
--- a/ivette/src/dome/src/renderer/text/buffers.js
+++ b/ivette/src/dome/src/renderer/text/buffers.js
@@ -546,11 +546,11 @@ is blocked.
/**
@summary Print text containing tags into buffer (bound to `this`).
- @param {string|string[]} text - Text to print.
+ @param {any} text - Text to print.
@param {object} options - CodeMirror
[text marker](https://codemirror.net/doc/manual.html#api_marker) options.
*/
- printTextWithTags(text = '', options = {}) {
+ printTextWithTags(text, options = {}) {
if (Array.isArray(text)) {
const tag = text.shift();
if (tag !== '') {
@@ -563,7 +563,7 @@ is blocked.
}
} else if (typeof text === 'string') {
this.append(text);
- } else if (text !== null) {
+ } else if (text !== null && text !== undefined) {
console.error('[Dome.buffers] unexpected text',text);
}
}
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index ed2806f5cd2..7cabcbad64f 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -88,13 +88,13 @@ export function useProject() {
export async function setProject(project: string) {
if (Server.isRunning()) {
try {
- const sr: Server.SetRequest<null, null> = {
+ const sr: Server.SetRequest<string, null> = {
kind: Server.RqKind.SET,
name: 'kernel.project.setCurrent',
- input: Json.jNull,
+ input: Json.jString,
output: Json.jNull,
};
- await Server.send(sr, null);
+ await Server.send(sr, project);
currentProject = project;
Dome.emit(PROJECT);
} catch (error) {
@@ -167,8 +167,8 @@ export function useRequest<In, Out>(
export type Tag = {
name: string;
- label: string;
- descr: string;
+ label?: string;
+ descr?: string;
}
const holdCurrent = { offline: null, pending: null, onError: null };
@@ -213,13 +213,13 @@ export interface Array<K, A> {
key: keyof A;
signal: Server.Signal;
fetch: Server.GetRequest<number, Fetches<K, A>>;
- reload: Server.SetRequest<null, null>;
+ reload: Server.GetRequest<null, null>;
}
type id = { project: string, state: string };
// --------------------------------------------------------------------------
-// --- Handler for Synchronized States
+// --- Handler for Synchronized St byates
// --------------------------------------------------------------------------
interface Handler<A> {
@@ -328,16 +328,23 @@ export function useSyncValue<A>(va: Value<A>): A | undefined {
// --- Synchronized Arrays
// --------------------------------------------------------------------------
+export interface Model<A> {
+ clear(): void;
+ remove(key: string): void;
+ add(entry: A): void;
+ clear(): void;
+}
+
// one per project
class SyncArray<K, A> {
handler: Array<K, A>;
- model: ArrayModel<A>;
+ model: Model<A>;
insync: boolean;
- constructor(h: Array<K, A>) {
+ constructor(h: Array<K, A>, m?: Model<A>) {
this.handler = h;
this.insync = false;
- this.model = new ArrayModel<A>(h.key);
+ this.model = m ?? new ArrayModel<A>(h.key);
this.fetch = this.fetch.bind(this);
this.reload = this.reload.bind(this);
}
@@ -381,12 +388,18 @@ class SyncArray<K, A> {
const syncArrays = new Map<id, SyncArray<any, any>>();
-function getSyncArray<K, A>(arr: Array<K, A>): SyncArray<K, A> {
+function getSyncArray<K, A>(arr: Array<K, A>, model?: Model<A>): SyncArray<K, A> {
const id = { project: currentProject ?? '', state: arr.name };
let a = syncArrays.get(id);
if (!a) {
- a = new SyncArray(arr);
+ a = new SyncArray(arr, model);
syncArrays.set(id, a);
+ } else {
+ if (model && a.model !== model) {
+ model.clear();
+ a.reload();
+ a.model = model;
+ }
}
return a;
}
@@ -407,8 +420,8 @@ export function reloadArray<K, A>(arr: Array<K, A>) {
/**
Use Synchronized Array (Custom React Hook).
*/
-export function useSyncArray<K, A>(arr: Array<K, A>): ArrayModel<A> {
- const a = getSyncArray(arr);
+export function useSyncArray<K, A>(arr: Array<K, A>, model?: Model<A>): Model<A> {
+ const a = getSyncArray(arr, model);
Dome.useUpdate(PROJECT);
Server.useSignal(arr.signal, a.fetch);
return a.model;
diff --git a/ivette/src/renderer/ASTinfo.tsx b/ivette/src/renderer/ASTinfo.tsx
index 6f3fb2bdca7..8fbe76d5916 100644
--- a/ivette/src/renderer/ASTinfo.tsx
+++ b/ivette/src/renderer/ASTinfo.tsx
@@ -10,6 +10,8 @@ import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { Component } from 'frama-c/LabViews';
+import { getInfo } from 'api/kernel/ast';
+
// --------------------------------------------------------------------------
// --- Information Panel
// --------------------------------------------------------------------------
@@ -19,17 +21,11 @@ const ASTinfo = () => {
const buffer = React.useMemo(() => new RichTextBuffer(), []);
const [selection, updateSelection] = States.useSelection();
const marker = selection?.current?.marker;
- const data = States.useRequest(
- 'kernel.ast.info',
- marker,
- { offline: undefined },
- );
+ const data = States.useRequest(getInfo, marker);
React.useEffect(() => {
buffer.clear();
- if (data) {
- buffer.printTextWithTags(data, { css: 'color: blue' });
- }
+ buffer.printTextWithTags(data, { css: 'color: blue' });
}, [buffer, data]);
// Callbacks
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 14a89985336..ea50893a20a 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -16,6 +16,10 @@ import { Vfill } from 'dome/layout/boxes';
import { Splitter } from 'dome/layout/splitters';
import { Form, Section, FieldCheckbox } from 'dome/layout/forms';
+import { source as SourceLoc } from 'api/kernel/services';
+import { statusData as Property } from 'api/kernel/properties';
+import * as Properties from 'api/kernel/properties';
+
// --------------------------------------------------------------------------
// --- Filters
// --------------------------------------------------------------------------
@@ -29,7 +33,6 @@ const defaultStatusFilter =
invalid_hyp: true,
considered_valid: false,
untried: false,
- dead: false,
inconsistent: true,
};
@@ -84,7 +87,7 @@ const defaultFilter =
};
-function filterStatus(f: typeof defaultStatusFilter, status: string) {
+function filterStatus(f: typeof defaultStatusFilter, status: Properties.propStatus) {
switch (status) {
case 'valid':
case 'valid_but_dead': return f.valid;
@@ -96,27 +99,27 @@ function filterStatus(f: typeof defaultStatusFilter, status: string) {
case 'unknown_but_dead': return f.unknown;
case 'considered_valid': return f.considered_valid;
case 'never_tried': return f.untried;
- case 'dead': return f.dead;
case 'inconsistent': return f.inconsistent;
default: return true;
}
}
-function filterKind(f: typeof defaultKindFilter, kind: string) {
+function filterKind(f: typeof defaultKindFilter, kind: Properties.propKind) {
switch (kind) {
case 'assert': return f.assert;
- case 'invariant': return f.invariant;
- case 'variant': return f.variant;
+ case 'loop_invariant':
+ return f.invariant;
+ case 'loop_variant': return f.variant;
case 'requires': return f.requires;
case 'ensures': return f.ensures;
case 'instance': return f.instance;
case 'assigns': return f.assigns;
- case 'from': return f.from;
+ case 'froms': return f.from;
case 'allocates': return f.allocates;
case 'behavior': return f.behavior;
case 'reachable': return f.reachable;
case 'axiomatic': return f.axiomatic;
- case 'pragma': return f.pragma;
+ case 'loop_pragma': return f.pragma;
default: return f.others;
}
}
@@ -160,10 +163,8 @@ function filterProperty(f: typeof defaultFilter, item: Property) {
const renderCode: Renderer<string> =
(text: string) => (<Code className="code-column" title={text}>{text}</Code>);
-interface Tag { name: string; label: string; descr: string }
-
-const renderTag: Renderer<Tag> =
- (d: Tag) => <Label label={d.label} title={d.descr} />;
+const renderTag: Renderer<States.Tag> =
+ (d: States.Tag) => <Label label={d.label ?? d.name} title={d.descr} />;
const renderNames: Renderer<string[]> =
(names: string[]) => {
@@ -185,7 +186,7 @@ function ColumnCode<Row>(props: ColumnProps<Row, string>) {
return <Column render={renderCode} {...props} />;
}
-function ColumnTag<Row>(props: ColumnProps<Row, Tag>) {
+function ColumnTag<Row>(props: ColumnProps<Row, States.Tag>) {
return <Column render={renderTag} {...props} />;
}
@@ -193,26 +194,6 @@ function ColumnTag<Row>(props: ColumnProps<Row, Tag>) {
// --- Properties Table
// -------------------------------------------------------------------------
-interface SourceLoc {
- dir: string;
- base: string;
- file: string;
- line: number;
-}
-
-interface Property {
- key: string;
- descr: string;
- kind: string;
- alarm?: string;
- names: string[];
- predicate: string;
- status: string;
- function?: string;
- kinstr: string;
- source: SourceLoc;
-}
-
const bySource =
Compare.byFields<SourceLoc>({ file: Compare.alpha, line: Compare.primitive });
@@ -235,12 +216,12 @@ const byProperty: Compare.ByFields<Property> = {
status: byStatus,
function: Compare.defined(Compare.alpha),
source: bySource,
- kind: Compare.primitive,
+ kind: Compare.structural,
alarm: Compare.defined(Compare.alpha),
names: Compare.array(Compare.alpha),
predicate: Compare.defined(Compare.alpha),
key: Compare.primitive,
- kinstr: Compare.primitive,
+ kinstr: Compare.structural,
};
const byDir = Compare.byFields<SourceLoc>({ dir: Compare.alpha });
@@ -251,7 +232,7 @@ const byColumn: Arrays.ByColumns<Property> = {
file: Compare.byFields<Property>({ source: byFile }),
};
-class PropertyModel extends Arrays.ArrayModel<Property> {
+class PropertyModel extends Arrays.ArrayModel<Property> implements States.Model<Property> {
private filterFun?: string;
private filterProp = _.cloneDeep(defaultFilter);
@@ -359,26 +340,23 @@ const PropertyFilter =
const PropertyColumns = () => {
- const statusDict: { [status: string]: Tag } =
- States.useDictionary('kernel.dictionary.propstatus');
- const kindDict: { [kind: string]: Tag } =
- States.useDictionary('kernel.dictionary.propkind');
- const alarmDict: { [alarm: string]: Tag } =
- States.useDictionary('kernel.dictionary.alarmkind');
+ const statusDict = States.useTags(Properties.propStatusTags);
+ const kindDict = States.useTags(Properties.propKindTags);
+ const alarmDict = States.useTags(Properties.alarmsTags);
const getStatus = React.useCallback(
- ({ status: st }: Property) => (statusDict[st] ?? { label: st }),
+ ({ status: st }: Property) => (statusDict.get(st) ?? { name: st }),
[statusDict],
);
const getKind = React.useCallback(
- ({ kind }: Property) => (kindDict[kind] ?? { label: kind }),
+ ({ kind: kd }: Property) => (kindDict.get(kd) ?? { name: kd }),
[kindDict],
);
const getAlarm = React.useCallback(
({ alarm }: Property) => (
- alarm === undefined ? alarm : (alarmDict[alarm] ?? { label: alarm })
+ alarm === undefined ? alarm : (alarmDict.get(alarm) ?? { name: alarm })
),
[alarmDict],
);
@@ -452,20 +430,14 @@ function FilterRatio({ model }: { model: PropertyModel }) {
const RenderTable = () => {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
- const properties: { [key: string]: Property } =
- States.useSyncArray('kernel.properties');
+
+ States.useSyncArray<"#status", Property>(Properties.status, model);
const [selection, updateSelection] = States.useSelection();
const [showFilter, flipFilter] =
Dome.useSwitch('ivette.properties.showFilter', true);
- // Populating the model
- React.useEffect(() => {
- const data = _.toArray(properties);
- model.replace(data);
- }, [model, properties]);
-
// Updating the filter
const selectedFunction = selection?.current?.function;
React.useEffect(() => {
diff --git a/ivette/tsconfig.json b/ivette/tsconfig.json
index 2ffcf2dace2..0f43fba3bb9 100644
--- a/ivette/tsconfig.json
+++ b/ivette/tsconfig.json
@@ -43,6 +43,7 @@
"resolveJsonModule": true, /* Allow to load JSON files as module. */
"baseUrl": ".", /* Base directory to resolve non-absolute module names. */
"paths": { /* A series of entries which re-map imports to lookup locations relative to the 'baseUrl'. */
+ "api/*": [ "api/*" ],
"frama-c/*": [ "src/frama-c/*" ],
"dome": [ "src/dome/src/renderer/dome.js" ],
"dome/system": [ "src/dome/src/misc/system.js" ],
@@ -71,7 +72,8 @@
"forceConsistentCasingInFileNames": true /* Disallow inconsistently-cased references to the same file. */
},
"include": [
- "src/**/*"
+ "src/**/*",
+ "api/**/*"
],
"exclude": [
"node_modules",
diff --git a/ivette/webpack.renderer.js b/ivette/webpack.renderer.js
index 55008fe5010..e35b929d476 100644
--- a/ivette/webpack.renderer.js
+++ b/ivette/webpack.renderer.js
@@ -26,6 +26,7 @@ module.exports = {
resolve: {
extensions: ['.ts', '.tsx', '.js', 'jsx', '.json'],
alias: {
+ 'api': path.resolve( __dirname , 'api' ),
'frama-c': path.resolve( __dirname , 'src/frama-c' ),
'@plugins': path.resolve( __dirname , 'src/plugins' ),
'dome/misc': path.resolve( DOME , 'src/misc' ),
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 63d723535e1..f1a17dc67cf 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -378,8 +378,7 @@ struct
let jtype =
let fields = List.rev s.fields in
let id = Package.declare_id ~package ~name ~descr (D_record fields) in
- let field fd = fd.fd_name, fd.fd_type in
- derived ~package ~id (Jrecord (List.map field fields)) ;
+ derived ~package ~id (Jrecord (List.map Package.field fields)) ;
Jdata id
let default = s.default
let has fd r = fd.member r
@@ -440,6 +439,7 @@ struct
mutable syntax : Markdown.text ;
mutable published : (package * string) option ;
mutable tags : tagInfo list ;
+ mutable prefix : tagInfo list ;
mutable lookup : ('a -> string) option ;
}
@@ -456,6 +456,7 @@ struct
values = Hashtbl.create 0 ;
vindex = Hashtbl.create 0 ;
syntax = [] ;
+ prefix = [] ;
tags = [] ;
lookup = None ;
}
@@ -499,7 +500,7 @@ struct
let set_lookup (d : 'a dictionary) (tag : 'a -> 'a tag) =
d.lookup <- Some tag
- let instance_name = Printf.sprintf "%s:%s"
+ let instance_name = Printf.sprintf "%s_%s"
let instance (_,prefix) = instance_name prefix
@@ -509,7 +510,7 @@ struct
tg_label = tag_label (name ^ ".") label ;
tg_descr = descr ;
} in
- d.tags <- tg :: d.tags ; d , name
+ d.prefix <- tg :: d.prefix ; d , name
let extends ~name ?label ~descr ?value ((d,prefix) : 'a prefix) : 'a tag =
let name = tag ~name:(instance_name prefix name) ?label ~descr ?value d in
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index c34c4fb90e9..5a0b678ffbd 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -144,8 +144,8 @@ struct
in
States.register_array
~package
- ~name:"markerData"
- ~descr:(Md.plain "Markers data")
+ ~name:"markerInfo"
+ ~descr:(Md.plain "Marker informations")
~key:snd
~iter model
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 7846c929c9c..ef20336fc6a 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -44,7 +44,7 @@ struct
t_kind name (Printf.sprintf "Clause `@%s`" name)
let t_loop name =
- t_kind ("loop-" ^ name) (Printf.sprintf "Clause `@loop %s`" name)
+ t_kind ("loop_" ^ name) (Printf.sprintf "Clause `@loop %s`" name)
let t_behavior = t_kind "behavior" "Contract behavior"
let t_complete = t_kind "complete" "Complete behaviors clause"
@@ -66,17 +66,17 @@ struct
let t_assert = t_kind "assert" "Assertion"
let t_check = t_kind "check" "Check"
- let t_loop_invariant = t_kind "invariant" "Loop invariant"
+ let t_loop_invariant = t_loop "invariant"
let t_loop_assigns = t_loop "assigns"
- let t_loop_variant = t_kind "variant" "Loop termination argument"
+ let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
let t_loop_pragma = t_loop "pragma"
let t_reachable = t_kind "reachable" "Reachable statement"
- let t_code_contract = t_kind "code-contract" "Statement contract"
- let t_code_invariant = t_kind "code-invariant" "Generalized loop invariant"
- let t_type_invariant = t_kind "type-invariant" "Type invariant"
- let t_global_invariant = t_kind "global-invariant" "Global invariant"
+ let t_code_contract = t_kind "code_contract" "Statement contract"
+ let t_code_invariant = t_kind "code_invariant" "Generalized loop invariant"
+ let t_type_invariant = t_kind "type_invariant" "Type invariant"
+ let t_global_invariant = t_kind "global_invariant" "Global invariant"
let t_axiomatic = t_kind "axiomatic" "Axiomatic definitions"
let t_axiom = t_kind "axiom" "Logical axiom"
@@ -85,7 +85,7 @@ struct
let p_ext = Enum.prefix kinds ~name:"ext" ~var:"<clause>"
~descr:(Md.plain "ACSL extension `<clause>`")
- let p_loop_ext = Enum.prefix kinds ~name:"loop-ext" ~var:"<clause>"
+ let p_loop_ext = Enum.prefix kinds ~name:"loop_ext" ~var:"<clause>"
~descr:(Md.plain "ACSL loop extension `loop <clause>`")
let p_other = Enum.prefix kinds ~name:"prop" ~var:"<prop>"
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index cde3cfeb3d3..5da3ab8ad8e 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -285,6 +285,15 @@ end
(* --- Visitors --- *)
(* -------------------------------------------------------------------------- *)
+let rec isRecursive = function
+ | Jself -> true
+ | Jdata _ | Jenum _
+ | Jany | Jnull | Jboolean | Jnumber
+ | Jstring | Jalpha | Jkey _ | Jindex _ -> false
+ | Joption js | Jdict(_,js) | Jarray js | Jlist js -> isRecursive js
+ | Jtuple js | Junion js -> List.exists isRecursive js
+ | Jrecord fjs -> List.exists (fun (_,js) -> isRecursive js) fjs
+
let rec visit_jtype fn = function
| Jany | Jself | Jnull | Jboolean | Jnumber
| Jstring | Jalpha | Jkey _ | Jindex _ -> ()
@@ -339,6 +348,8 @@ type package = {
mutable revDecl : declInfo list ; (* in reverse order *)
}
+let field fd = fd.fd_name , fd.fd_type
+
let name_of_package ?sep pkg = name_of_pkginfo ?sep pkg.pkgInfo
let registry = ref IdSet.empty (* including packages *)
diff --git a/src/plugins/server/package.mli b/src/plugins/server/package.mli
index f60c02145bc..c040c985bc8 100644
--- a/src/plugins/server/package.mli
+++ b/src/plugins/server/package.mli
@@ -147,6 +147,7 @@ sig
val resolve : t -> string IdMap.t
end
+val isRecursive : jtype -> bool
val visit_jtype : (ident -> unit) -> jtype -> unit
val visit_field: (ident -> unit) -> fieldInfo -> unit
val visit_param: (ident -> unit) -> paramInfo -> unit
@@ -206,6 +207,7 @@ val iter : (packageInfo -> unit) -> unit
(** Assigns non-classing names for each identifier. *)
val resolve : ?keywords: string list -> packageInfo -> string IdMap.t
+val field : fieldInfo -> string * jtype
val name_of_pkg : ?sep:string -> plugin -> string list -> string
val name_of_pkginfo : ?sep:string -> packageInfo -> string
val name_of_package : ?sep:string -> package -> string
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index c45af471fbe..9a26d581c2c 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -287,6 +287,8 @@ let register_array ~package ~name ~descr ~key
~package ~name:(Package.Derived.data id).name
~descr:(plain "Data for array rows" @ href)
(D_record fields) in
+ let fs = List.map Package.field fields in
+ Data.derived ~package ~id:row (Jrecord fs) ;
let getter =
List.map Package.(fun (fd,to_js) -> fd.fd_name , to_js) !model in
let array = {
--
GitLab