Commit e0bf4efe authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'feature/server/generate-api' into 'master'

[server] Generator API

See merge request frama-c/frama-c!2710
parents 21864645 dcef90ff
......@@ -88,7 +88,7 @@ body {
#NAVIGATION a.root {
display: block;
font-family: "Optima", "Verdana", "Arial", sans;
font-size: 10pt;
font-size: 16pt;
margin-top: 1cm;
margin-bottom: 6mm;
}
......@@ -105,13 +105,23 @@ body {
}
#NAVIGATION ul {
width: 6cm ;
width: 8cm ;
margin: 0px ;
padding: 0px ;
}
#NAVIGATION li {
list-style-type: none;
margin: 0px;
padding-left: 8px;
}
#NAVIGATION ul > ul {
margin-left: 0px ;
padding-top: 2px ;
padding-bottom: 2px ;
#TOC > a {
font-weight: bold;
}
.TOC > ul > li > a {
font-weight: bold;
}
/* -------------------------------------------------------------------------- */
......
......@@ -23,7 +23,7 @@
$if(toc)$
$for(link)$
$if(link.toc)$
$table-of-contents$
<div class="TOC">$table-of-contents$</div>
$else$
<li><a href="$link.href$.html">$link.title$</a></li>
$endif$
......
......@@ -1112,8 +1112,6 @@ src/plugins/server/Server.mli: .ignore
src/plugins/server/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/data.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/data.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/doc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/doc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/jbuffer.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/jbuffer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_ast.ml: CEA_LGPL_OR_PROPRIETARY
......@@ -1126,16 +1124,18 @@ src/plugins/server/kernel_properties.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_properties.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/package.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/package.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_doc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_doc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/syntax.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/syntax.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/Scope.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.mli: CEA_LGPL_OR_PROPRIETARY
......
......@@ -30,6 +30,18 @@ fixlint: dome-pkg dome-templ
tsc: typecheck fixlint
# --------------------------------------------------------------------------
# --- Frama-C API
# --------------------------------------------------------------------------
.PHONY: api
api:
@echo "[Ivette] Generating TypeScript 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 {} \;
# --------------------------------------------------------------------------
# --- Ivette Documentation
# --------------------------------------------------------------------------
......
/* --- Generated Frama-C Server API --- */
/**
Ast Services
@packageDocumentation
@module api/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';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
name: 'kernel.ast.compute',
input: Json.jNull,
output: Json.jNull,
};
/** Ensures that AST is computed */
export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Marker kind */
export enum markerKind {
/** Expression */
expression = 'expression',
/** Lvalue */
lvalue = 'lvalue',
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
/** Declaration */
declaration = 'declaration',
/** Statement */
statement = 'statement',
/** Global */
global = 'global',
/** Term */
term = 'term',
/** Property */
property = 'property',
}
/** Loose decoder for `markerKind` */
export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
/** Safe decoder for `markerKind` */
export const jMarkerKindSafe: Json.Safe<markerKind> =
Json.jFail(Json.jEnum(markerKind),'kernel.ast.markerKind expected');
/** Natural order for `markerKind` */
export const byMarkerKind: Compare.Order<markerKind> =
Compare.byEnum(markerKind);
const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.markerKindTags',
input: Json.jNull,
output: Json.jList(jTag),
};
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
/** Marker short name */
name: string;
/** Marker declaration or description */
descr: string;
}
/** Loose decoder for `markerInfoData` */
export const jMarkerInfoData: Json.Loose<markerInfoData> =
Json.jObject({
key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
'#markerInfo expected'),
kind: jMarkerKindSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
});
/** Safe decoder for `markerInfoData` */
export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
Json.jFail(jMarkerInfoData,'MarkerInfoData 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,
});
/** Signal for array [`markerInfo`](#markerinfo) */
export const signalMarkerInfo: Server.Signal = {
name: 'kernel.ast.signalMarkerInfo',
};
const reloadMarkerInfo_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.reloadMarkerInfo',
input: Json.jNull,
output: Json.jNull,
};
/** Force full reload for array [`markerInfo`](#markerinfo) */
export const reloadMarkerInfo: Server.GetRequest<null,null>= reloadMarkerInfo_internal;
const fetchMarkerInfo_internal: Server.GetRequest<
number,
{ pending: number, updated: markerInfoData[],
removed: Json.key<'#markerInfo'>[], reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchMarkerInfo',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jMarkerInfoData),
removed: Json.jList(Json.jKey<'#markerInfo'>('#markerInfo')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
export const fetchMarkerInfo: Server.GetRequest<
number,
{ pending: number, updated: markerInfoData[],
removed: Json.key<'#markerInfo'>[], reload: boolean }
>= fetchMarkerInfo_internal;
const markerInfo_internal: State.Array<
Json.key<'#markerInfo'>,
markerInfoData
> = {
name: 'kernel.ast.markerInfo',
getkey: ((d:markerInfoData) => d.key),
signal: signalMarkerInfo,
fetch: fetchMarkerInfo,
reload: reloadMarkerInfo,
order: byMarkerInfoData,
};
/** Marker informations */
export const markerInfo: State.Array<Json.key<'#markerInfo'>,markerInfoData> = markerInfo_internal;
/** 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'>;
/** 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.jKey<'#stmt'>('#stmt'),
Json.jKey<'#decl'>('#decl'),
Json.jKey<'#lval'>('#lval'),
Json.jKey<'#expr'>('#expr'),
Json.jKey<'#term'>('#term'),
Json.jKey<'#global'>('#global'),
Json.jKey<'#property'>('#property'),
);
/** Safe decoder for `marker` */
export const jMarkerSafe: Json.Safe<marker> =
Json.jFail(jMarker,'Marker expected');
/** Natural order for `marker` */
export const byMarker: Compare.Order<marker> = Compare.structural;
const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
input: Json.jNull,
output: Json.jList(Json.jKey<'#fct'>('#fct')),
};
/** Collect all functions in the AST */
export const getFunctions: Server.GetRequest<null,Json.key<'#fct'>[]>= getFunctions_internal;
const printFunction_internal: Server.GetRequest<Json.key<'#fct'>,text> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.printFunction',
input: Json.jKey<'#fct'>('#fct'),
output: jText,
};
/** Print the AST of a function */
export const printFunction: Server.GetRequest<Json.key<'#fct'>,text>= printFunction_internal;
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
/** Entry identifier. */
key: Json.key<'#functions'>;
/** Name */
name: string;
/** Signature */
signature: string;
}
/** Loose decoder for `functionsData` */
export const jFunctionsData: Json.Loose<functionsData> =
Json.jObject({
key: Json.jFail(Json.jKey<'#functions'>('#functions'),
'#functions expected'),
name: Json.jFail(Json.jString,'String expected'),
signature: Json.jFail(Json.jString,'String expected'),
});
/** Safe decoder for `functionsData` */
export const jFunctionsDataSafe: Json.Safe<functionsData> =
Json.jFail(jFunctionsData,'FunctionsData 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,
});
/** Signal for array [`functions`](#functions) */
export const signalFunctions: Server.Signal = {
name: 'kernel.ast.signalFunctions',
};
const reloadFunctions_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.reloadFunctions',
input: Json.jNull,
output: Json.jNull,
};
/** Force full reload for array [`functions`](#functions) */
export const reloadFunctions: Server.GetRequest<null,null>= reloadFunctions_internal;
const fetchFunctions_internal: Server.GetRequest<
number,
{ pending: number, updated: functionsData[],
removed: Json.key<'#functions'>[], reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchFunctions',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jFunctionsData),
removed: Json.jList(Json.jKey<'#functions'>('#functions')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`functions`](#functions) */
export const fetchFunctions: Server.GetRequest<
number,
{ pending: number, updated: functionsData[],
removed: Json.key<'#functions'>[], reload: boolean }
>= fetchFunctions_internal;
const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
name: 'kernel.ast.functions',
getkey: ((d:functionsData) => d.key),
signal: signalFunctions,
fetch: fetchFunctions,
reload: reloadFunctions,
order: byFunctionsData,
};
/** AST Functions */
export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
const getInfo_internal: Server.GetRequest<marker,text> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getInfo',
input: jMarker,
output: jText,
};
/** Get textual information about a marker */
export const getInfo: Server.GetRequest<marker,text>= getInfo_internal;
const getFiles_internal: Server.GetRequest<null,string[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFiles',
input: Json.jNull,
output: Json.jList(Json.jString),
};
/** Get the currently analyzed source file names */
export const getFiles: Server.GetRequest<null,string[]>= getFiles_internal;
const setFiles_internal: Server.SetRequest<string[],null> = {
kind: Server.RqKind.SET,
name: 'kernel.ast.setFiles',
input: Json.jList(Json.jString),
output: Json.jNull,
};
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
/* ------------------------------------- */
/* --- Generated Frama-C Server API --- */
/**
Informations
@packageDocumentation
@module api/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';
/** Markdown (inlined) text. */
export type markdown = string;
/** Loose decoder for `markdown` */
export const jMarkdown: Json.Loose<markdown> = Json.jString;
/** Safe decoder for `markdown` */
export const jMarkdownSafe: Json.Safe<markdown> =
Json.jFail(Json.jString,'String expected');
/** Natural order for `markdown` */
export const byMarkdown: Compare.Order<markdown> = Compare.primitive;
/** 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[];
/** Loose decoder for `text` */
export const jText: Json.Loose<text> =
(_x: any) => Json.jUnion<null | string | text[]>(
Json.jNull,
Json.jString,
Json.jList(jText),
)(_x);
/** Safe decoder for `text` */
export const jTextSafe: Json.Safe<text> =
(_x: any) => Json.jFail(jText,'Text expected')(_x);
/** Natural order for `text` */
export const byText: Compare.Order<text> =
(_x: any, _y: any) => Compare.structural(_x,_y);
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
/** Loose decoder for `tag` */
export const jTag: Json.Loose<tag> =
Json.jObject({
name: Json.jFail(Json.jString,'String expected'),
label: jMarkdownSafe,
descr: jMarkdownSafe,
});
/** Safe decoder for `tag` */
export const jTagSafe: Json.Safe<tag> = Json.jFail(jTag,'Tag expected');
/** Natural order for `tag` */
export const byTag: Compare.Order<tag> =
Compare.byFields
<{ name: string, label: markdown, descr: markdown }>({
name: Compare.alpha,
label: byMarkdown,
descr: byMarkdown,
});
/* ------------------------------------- */
/* --- Generated Frama-C Server API --- */
/**
Project Management
@packageDocumentation
@module api/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 };
/** Loose decoder for `projectInfo` */
export const jProjectInfo: Json.Loose<projectInfo> =
Json.jObject({
id: Json.jFail(Json.jKey<'#project'>('#project'),'#project expected'),
name: Json.jFail(Json.jString,'String expected'),
current: Json.jFail(Json.jBoolean,'Boolean expected'),
});
/** Safe decoder for `projectInfo` */
export const jProjectInfoSafe: Json.Safe<projectInfo> =
Json.jFail(jProjectInfo,'ProjectInfo expected');
/** Natural order for `projectInfo` */
export const byProjectInfo: Compare.Order<projectInfo> =
Compare.byFields
<{ id: Json.key<'#project'>, name: string, current: boolean }>({
id: Compare.primitive,
name: Compare.alpha,
current: Compare.primitive,
});
/** Request to be executed on the specified project. */
export type projectRequest =
{ project: Json.key<'#project'>, request: string, data: Json.json };
/** Loose decoder for `projectRequest` */
export const jProjectRequest: Json.Loose<projectRequest> =
Json.jObject({
project: Json.jFail(Json.jKey<'#project'>('#project'),
'#project expected'),
request: Json.jFail(Json.jString,'String expected'),
data: Json.jAny,
});
/** Safe decoder for `projectRequest` */
export const jProjectRequestSafe: Json.Safe<projectRequest> =
Json.jFail(jProjectRequest,'ProjectRequest expected');
/** Natural order for `projectRequest` */
export const byProjectRequest: Compare.Order<projectRequest> =
Compare.byFields
<{ project: Json.key<'#project'>, request: string, data: Json.json }>({
project: Compare.primitive,
request: Compare.primitive,
data: Compare.structural,
});
const getCurrent_internal: Server.GetRequest<null,projectInfo> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getCurrent',
input: Json.jNull,
output: jProjectInfo,
};
/** Returns the current project */
export const getCurrent: Server.GetRequest<null,projectInfo>= getCurrent_internal;
const setCurrent_internal: Server.SetRequest<Json.key<'#project'>,null> = {
kind: Server.RqKind.SET,
name: 'kernel.project.setCurrent',
input: Json.jKey<'#project'>('#project'),
output: Json.jNull,
};
/** Switches the current project */
export const setCurrent: Server.SetRequest<Json.key<'#project'>,null>= setCurrent_internal;
const getList_internal: Server.GetRequest<null,projectInfo[]> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getList',
input: Json.jNull,
output: Json.jList(jProjectInfo),
};
/** Returns the list of all projects */
export const getList: Server.GetRequest<null,projectInfo[]>= getList_internal;
const getOn_internal: Server.GetRequest<projectRequest,Json.json> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getOn',