From dd01837721ddbf3e151ca6137916bee4c0b7ab83 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jun 2020 15:56:06 +0200
Subject: [PATCH] [ivette] package structure

---
 ivette/api/dive.ts              | 38 ++++++++++++++
 ivette/api/kernel/ast.ts        | 93 +++++++++++++++++++++++++++++++++
 ivette/api/kernel/data.ts       | 21 ++++++++
 ivette/api/kernel/project.ts    | 46 ++++++++++++++++
 ivette/api/kernel/properties.ts | 54 +++++++++++++++++++
 ivette/api/kernel/services.ts   | 40 ++++++++++++++
 src/plugins/server/package.ml   | 14 ++---
 7 files changed, 297 insertions(+), 9 deletions(-)
 create mode 100644 ivette/api/dive.ts
 create mode 100644 ivette/api/kernel/ast.ts
 create mode 100644 ivette/api/kernel/data.ts
 create mode 100644 ivette/api/kernel/project.ts
 create mode 100644 ivette/api/kernel/properties.ts
 create mode 100644 ivette/api/kernel/services.ts

diff --git a/ivette/api/dive.ts b/ivette/api/dive.ts
new file mode 100644
index 00000000000..1414a99e710
--- /dev/null
+++ b/ivette/api/dive.ts
@@ -0,0 +1,38 @@
+/* --- Generated Frama-C Server API --- */
+/** Dive Services
+   @packageDocumentation
+   @module frama-c/dive
+*/
+import * as Json from 'dome/data/json'
+import { addFunctionAlarms } from 'api/dive';
+import { addVar } from 'api/dive';
+import { clear } from 'api/dive';
+import { explore } from 'api/dive';
+import { graph } from 'api/dive';
+import { hide } from 'api/dive';
+import { show } from 'api/dive';
+import { variableName } from 'api/dive';
+
+
+/** The name of variable of the program */
+
+
+/** Retrieve the whole graph */
+
+
+/** Erase the graph and start over with an empty one */
+
+
+/** Add a variable to the graph */
+
+
+/** Add all alarms of the given function */
+
+
+/** Explore the graph starting from an existing vertex */
+
+
+/** Show the dependencies of an existing vertex */
+
+
+/** Hide the dependencies of an existing vertex */
diff --git a/ivette/api/kernel/ast.ts b/ivette/api/kernel/ast.ts
new file mode 100644
index 00000000000..bcd79e62e60
--- /dev/null
+++ b/ivette/api/kernel/ast.ts
@@ -0,0 +1,93 @@
+/* --- Generated Frama-C Server API --- */
+/** Ast Services
+   @packageDocumentation
+   @module frama-c/kernel/ast
+*/
+import * as Json from 'dome/data/json'
+import { compute } from 'api/kernel/ast';
+import { functions } from 'api/kernel/ast';
+import { functionsFetch } from 'api/kernel/ast';
+import { functionsReload } from 'api/kernel/ast';
+import { functionsRow } from 'api/kernel/ast';
+import { functionsSig } from 'api/kernel/ast';
+import { getFiles } from 'api/kernel/ast';
+import { getFunctions } from 'api/kernel/ast';
+import { getInfo } from 'api/kernel/ast';
+import { marker } from 'api/kernel/ast';
+import { markerData } from 'api/kernel/ast';
+import { markerDataFetch } from 'api/kernel/ast';
+import { markerDataReload } from 'api/kernel/ast';
+import { markerDataRow } from 'api/kernel/ast';
+import { markerDataSig } from 'api/kernel/ast';
+import { markerKind } from 'api/kernel/ast';
+import { markerKindTags } from 'api/kernel/ast';
+import { printFunction } from 'api/kernel/ast';
+import { setFiles } from 'api/kernel/ast';
+import { tag } from 'api/kernel/data';
+import { text } from 'api/kernel/data';
+
+
+/** Ensures that AST is computed */
+
+
+/** Marker kind */
+
+
+/** Returns all registered tags for the above type. */
+
+
+/** Markers data */
+
+
+/** Signal for array [`markerData`](#markerdata)  */
+
+
+/** Data rows for array [`markerData`](#markerdata)
+ */
+
+
+/** Data fetcher for array [`markerData`](#markerdata)
+ */
+
+
+/** Force full reload for array [`markerData`](#markerdata)
+ */
+
+
+/** Localizable AST markers */
+type marker = Json.Key<'stmt'> | Json.Key<'decl'> | Json.Key<'lval'>
+                | Json.Key<'expr'> | Json.Key<'term'> | Json.Key<'global'>
+                | Json.Key<'property'>;
+
+
+/** Collect all functions in the AST */
+
+
+/** Print the AST of a function */
+
+
+/** AST Functions */
+
+
+/** Signal for array [`functions`](#functions)  */
+
+
+/** Data rows for array [`functions`](#functions)
+ */
+
+
+/** Data fetcher for array [`functions`](#functions)
+ */
+
+
+/** Force full reload for array [`functions`](#functions)
+ */
+
+
+/** Get textual information about a marker */
+
+
+/** Get the currently analyzed source file names */
+
+
+/** Set the source file names to analyze. */
diff --git a/ivette/api/kernel/data.ts b/ivette/api/kernel/data.ts
new file mode 100644
index 00000000000..60091f91ce3
--- /dev/null
+++ b/ivette/api/kernel/data.ts
@@ -0,0 +1,21 @@
+/* --- Generated Frama-C Server API --- */
+/** Informations
+   @packageDocumentation
+   @module frama-c/kernel/data
+*/
+import * as Json from 'dome/data/json'
+import { markdown } from 'api/kernel/data';
+import { tag } from 'api/kernel/data';
+import { text } from 'api/kernel/data';
+
+
+/** Markdown (inlined) text. */
+type markdown = string;
+
+
+/** 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. */
+type text = null | string | text[];
+
+
+/** Enum Tag Description */
+type tag = { name: string, label: markdown, descr: markdown };
diff --git a/ivette/api/kernel/project.ts b/ivette/api/kernel/project.ts
new file mode 100644
index 00000000000..190b724fd31
--- /dev/null
+++ b/ivette/api/kernel/project.ts
@@ -0,0 +1,46 @@
+/* --- Generated Frama-C Server API --- */
+/** Project Management
+   @packageDocumentation
+   @module frama-c/kernel/project
+*/
+import * as Json from 'dome/data/json'
+import { create } from 'api/kernel/project';
+import { execOn } from 'api/kernel/project';
+import { getCurrent } from 'api/kernel/project';
+import { getList } from 'api/kernel/project';
+import { getOn } from 'api/kernel/project';
+import { projectInfo } from 'api/kernel/project';
+import { projectRequest } from 'api/kernel/project';
+import { setCurrent } from 'api/kernel/project';
+import { setOn } from 'api/kernel/project';
+
+
+/** Project informations */
+type projectInfo = { id: Json.Key<'project'>, name: string, current: boolean
+                     };
+
+
+/** Request to be executed on the specified project. */
+type projectRequest = { project: Json.Key<'project'>, request: string,
+                        data: Json.json };
+
+
+/** Returns the current project */
+
+
+/** Switches the current project */
+
+
+/** Returns the list of all projects */
+
+
+/** Execute a GET request within the given project */
+
+
+/** Execute a SET request within the given project */
+
+
+/** Execute an EXEC request within the given project */
+
+
+/** Create a new project */
diff --git a/ivette/api/kernel/properties.ts b/ivette/api/kernel/properties.ts
new file mode 100644
index 00000000000..76d4dc1ec23
--- /dev/null
+++ b/ivette/api/kernel/properties.ts
@@ -0,0 +1,54 @@
+/* --- Generated Frama-C Server API --- */
+/** Property Services
+   @packageDocumentation
+   @module frama-c/kernel/properties
+*/
+import * as Json from 'dome/data/json'
+import { tag } from 'api/kernel/data';
+import { alarms } from 'api/kernel/properties';
+import { alarmsTags } from 'api/kernel/properties';
+import { propKind } from 'api/kernel/properties';
+import { propKindTags } from 'api/kernel/properties';
+import { propStatus } from 'api/kernel/properties';
+import { propStatusTags } from 'api/kernel/properties';
+import { status } from 'api/kernel/properties';
+import { statusFetch } from 'api/kernel/properties';
+import { statusReload } from 'api/kernel/properties';
+import { statusRow } from 'api/kernel/properties';
+import { statusSig } from 'api/kernel/properties';
+import { source } from 'api/kernel/services';
+
+
+/** Property Kinds */
+
+
+/** Returns all registered tags for the above type. */
+
+
+/** Property Status (consolidated) */
+
+
+/** Returns all registered tags for the above type. */
+
+
+/** Alarm Kinds */
+
+
+/** Returns all registered tags for the above type. */
+
+
+/** Status of Registered Properties */
+
+
+/** Signal for array [`status`](#status)  */
+
+
+/** Data rows for array [`status`](#status)  */
+
+
+/** Data fetcher for array [`status`](#status)
+ */
+
+
+/** Force full reload for array [`status`](#status)
+ */
diff --git a/ivette/api/kernel/services.ts b/ivette/api/kernel/services.ts
new file mode 100644
index 00000000000..4a6fcde07ce
--- /dev/null
+++ b/ivette/api/kernel/services.ts
@@ -0,0 +1,40 @@
+/* --- Generated Frama-C Server API --- */
+/** Kernel Services
+   @packageDocumentation
+   @module frama-c/kernel/services
+*/
+import * as Json from 'dome/data/json'
+import { tag } from 'api/kernel/data';
+import { getConfig } from 'api/kernel/services';
+import { getLogs } from 'api/kernel/services';
+import { load } from 'api/kernel/services';
+import { log } from 'api/kernel/services';
+import { logkind } from 'api/kernel/services';
+import { logkindTags } from 'api/kernel/services';
+import { setLogs } from 'api/kernel/services';
+import { source } from 'api/kernel/services';
+
+
+/** Frama-C Kernel configuration */
+
+
+/** Load a save file. Returns an error, if not successfull. */
+
+
+/** Source file positions. */
+type source = { dir: string, base: string, file: string, line: number };
+
+
+/** Log messages categories. */
+
+
+/** Returns all registered tags for the above type. */
+
+
+/** Message event record. */
+
+
+/** Turn logs monitoring on/off */
+
+
+/** Flush the last emitted logs since last call (max 100) */
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 982269288b2..4f035474016 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -30,21 +30,17 @@ module Md = Markdown
 type plugin = Kernel | Plugin of string
 type ident = { plugin: plugin; package: string list; name: string }
 
-let pp_plugin fmt = function
-  | Kernel -> Format.pp_print_string fmt "Kernel"
-  | Plugin p -> Format.fprintf fmt "Plugin %s" p
-
 let pp_step fmt a =
   ( Format.pp_print_string fmt a ; Format.pp_print_char fmt '.' )
 
-let pp_plugin_step fmt = function
-  | Kernel -> ()
+let pp_plugin fmt = function
+  | Kernel -> pp_step fmt "kernel"
   | Plugin p -> pp_step fmt p
 
 let pp_ident fmt { plugin ; package ; name } =
-  ( pp_plugin_step fmt plugin ;
+  ( pp_plugin fmt plugin ;
     List.iter (pp_step fmt) package ;
-    pp_step fmt name )
+    Format.pp_print_string fmt name )
 
 (* -------------------------------------------------------------------------- *)
 (* --- Name Resolution                                                    --- *)
@@ -246,7 +242,7 @@ let name_of_pkginfo ?sep { p_plugin ; p_package } =
   name_of_pkg ?sep p_plugin p_package
 
 let pp_pkgname fmt { p_plugin ; p_package } =
-  ( pp_plugin_step fmt p_plugin ;
+  ( pp_plugin fmt p_plugin ;
     List.iter (pp_step fmt) p_package )
 
 (* -------------------------------------------------------------------------- *)
-- 
GitLab