...
 
Commits (215)
......@@ -140,21 +140,16 @@ internal_nightly:
tags:
- nix
frama-c-ocaml-4.06:
frama-c-ocaml-4.09:
variables:
OCAML: "4_06"
OCAML: "4_09"
<<: *frama-c-ocaml
only:
- schedules
frama-c-ocaml-4.07:
frama-c-ocaml-4.10:
variables:
OCAML: "4_07"
<<: *frama-c-ocaml
frama-c-ocaml-4.05:
variables:
OCAML: "4_05"
OCAML: "4_10"
<<: *frama-c-ocaml
......
......@@ -17,6 +17,10 @@
Open Source Release <next-release>
##################################
- Eva [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using
equality operators, temporary variables introduced by the Frama-C
normalization or goto statements.
- Eva [2020-05-29] New builtins for trigonometric functions acos, asin
and atan (and their single-precision version acosf, asinf, atanf).
- Kernel [2020-05-28] Support for C11's _Thread_local storage specifier
......
......@@ -827,9 +827,9 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
PLUGIN_ENABLE:=$(ENABLE_EVA)
PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains domains/cvalue domains/apron \
PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
values/numerors domains/numerors
api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
......@@ -910,11 +910,13 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
api/general_requests \
utils/unit_tests \
api/values_request \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
# These files are used by the GUI, but do not depend on Lablgtk
VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
......@@ -1502,11 +1504,11 @@ endif
$(DOC_DIR)/docgen.cmo: $(DOC_DIR)/docgen.ml
$(PRINT_OCAMLC) $@
$(OCAMLC) -c -I +ocamldoc -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml
$(OCAMLC) -c -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml
$(DOC_DIR)/docgen.cmxs: $(DOC_DIR)/docgen.ml
$(PRINT_PACKING) $@
$(OCAMLOPT) -o $@ -shared -I +ocamldoc -I $(CONFIG_DIR) \
$(OCAMLOPT) -o $@ -shared -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) \
$(DOC_DIR)/docgen.ml
clean-doc::
......
......@@ -6,6 +6,7 @@
/callgraph_gui/
/constant_propagation/
/counter-examples/
/dive/
/dynamic_plugins/
/e-acsl/
/from/
......
......@@ -130,11 +130,11 @@ struct
match_s
rel
in
if StringSet.mem match_s known_types_names then
if String.Set.mem match_s known_types_names then
"<a href=\"" ^ self#path match_s ^ Naming.complete_target Naming.mark_type
match_s ^"\">" ^ s_final ^ "</a>"
else
if StringSet.mem match_s known_classes_names then
if String.Set.mem match_s known_classes_names then
let (html_file, _) = Naming.html_files match_s in
"<a href=\""^ self#path html_file ^ html_file^"\">"^s_final^"</a>"
else
......@@ -158,7 +158,7 @@ struct
match_s
rel
in
if StringSet.mem match_s known_modules_names then
if String.Set.mem match_s known_modules_names then
let (html_file, _) = Naming.html_files match_s in
"<a href=\"" ^ self#path match_s ^ html_file^"\">"^s_final^"</a>"
else
......@@ -287,7 +287,7 @@ struct
let types = Odoc_info.Search.types module_list in
known_types_names <-
List.fold_left
(fun acc t -> StringSet.add t.Odoc_type.ty_name acc)
(fun acc t -> String.Set.add t.Odoc_type.ty_name acc)
known_types_names
types ;
......@@ -296,12 +296,12 @@ struct
let class_types = Odoc_info.Search.class_types module_list in
known_classes_names <-
List.fold_left
(fun acc c -> StringSet.add c.Odoc_class.cl_name acc)
(fun acc c -> String.Set.add c.Odoc_class.cl_name acc)
known_classes_names
classes ;
known_classes_names <-
List.fold_left
(fun acc ct -> StringSet.add ct.Odoc_class.clt_name acc)
(fun acc ct -> String.Set.add ct.Odoc_class.clt_name acc)
known_classes_names
class_types ;
......@@ -310,12 +310,12 @@ struct
let modules = Odoc_info.Search.modules module_list in
known_modules_names <-
List.fold_left
(fun acc m -> StringSet.add m.m_name acc)
(fun acc m -> String.Set.add m.m_name acc)
known_modules_names
modules ;
known_modules_names <-
List.fold_left
(fun acc mt -> StringSet.add mt.mt_name acc)
(fun acc mt -> String.Set.add mt.mt_name acc)
known_modules_names
module_types ;
......
......@@ -990,6 +990,16 @@ file, run it only once.
test
& \textit{None}
\\
& \texttt{TIMEOUT}\nscodeidxdef{Test!Directive}{TIMEOUT}
& kill the test after the given duration (in seconds of CPU user time)
and report a failure
& \textit{None}
\\
& \texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
& empty the list of frama-c commands to be launched
(\texttt{EXEC} and \texttt{EXECNOW} directives are still executed).
& \textit{None}
\\
\hline \multirow{2}{23mm}{\centering{Test suite}}
& \texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
& Do not execute this test
......@@ -1017,11 +1027,17 @@ test
Any directive can identify a file using a relative path.
The default directory considered for \texttt{.} is always the parent
directory of directory \texttt{tests}\codeidx{tests}. The
\texttt{DONTRUN} directive does not need to have any content, but it
is useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is currently developed and not fully
\texttt{DONTRUN} and \texttt{NOFRAMAC} directives
do not need to have any content, but it might be
useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is under development and not fully
operational yet).
If there are \texttt{OPT}/\texttt{STDOPT} directives \textit{after} a
\texttt{NOFRAMAC} directive, they will be executed, unless
they are themselves discarded by another subsequent \texttt{NOFRAMAC}
directive.
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
\begin{enumerate}
......
......@@ -5,6 +5,12 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
\section*{Frama-C+dev}
\begin{itemize}
\item \textbf{Testing}: Document new directives \texttt{TIMEOUT} and
\texttt{NOFRAMAC}
\end{itemize}
\section*{21.0 Scandium}
\begin{itemize}
\item \textbf{Configure}: Documentation of \texttt{configure\_pkg},
......@@ -13,13 +19,13 @@ This chapter summarizes the major changes in this documentation between each
\section*{20.0 Calcium}
\begin{itemize}
\item \textbf{Ptests}: Documentation of the new directive \texttt{MODULE}.
\item \textbf{Testing}: Documentation of the new directive \texttt{MODULE}.
\end{itemize}
\section*{19.0 Potassium}
\begin{itemize}
\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
\item \textbf{Testing}: Document usage of \texttt{@@} in a directive
\item \textbf{Profiling with Landmarks}: New section
\end{itemize}
......
......@@ -548,11 +548,11 @@ For this tutorial, there will be no such source code. A file
\texttt{./tests/hello/hello\_test.c} is then created:
\listingname{./tests/hello/hello\_test.c}
\sscodeidx{Test}{Directive}{OPT}
\nscodeidx{Test!Directive}{OPT}
\lstinputlisting[style=c]{./tutorial/hello/generated/with_test/tests/hello/hello_test.c}
In this file, there is only one directive
\texttt{OPT: -hello}\sscodeidx{Test}{Directive}{OPT} which requires
\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT} which requires
to run \framac on this test with the \texttt{-hello} option.
A look at Section~\ref{ptests:directives} gives you an idea of the kind of
directives which can be used to test plug-ins.
......
......@@ -768,14 +768,18 @@ src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/context.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/context.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_graph.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_range.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_range.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
......@@ -1208,6 +1212,10 @@ src/plugins/value/Changelog_non_free: .ignore
src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
......
......@@ -6,7 +6,6 @@
.dome-*.stamp
.dome-*.back
node_modules
yarn.lock
yarn-error.log
/bin
/dist
......
......@@ -47,10 +47,6 @@ export enum markerKind {
expression = 'expression',
/** Lvalue */
lvalue = 'lvalue',
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
/** Declaration */
declaration = 'declaration',
/** Statement */
......@@ -83,12 +79,44 @@ const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
/** Marker variable */
export enum markerVar {
/** None */
none = 'none',
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
}
/** Loose decoder for `markerVar` */
export const jMarkerVar: Json.Loose<markerVar> = Json.jEnum(markerVar);
/** Safe decoder for `markerVar` */
export const jMarkerVarSafe: Json.Safe<markerVar> =
Json.jFail(Json.jEnum(markerVar),'kernel.ast.markerVar expected');
/** Natural order for `markerVar` */
export const byMarkerVar: Compare.Order<markerVar> =
Compare.byEnum(markerVar);
const markerVarTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.markerVarTags',
input: Json.jNull,
output: Json.jList(jTag),
};
/** Registered tags for the above type. */
export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_internal;
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
/** Marker variable */
var: markerVar;
/** Marker short name */
name: string;
/** Marker declaration or description */
......@@ -101,6 +129,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> =
key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
'#markerInfo expected'),
kind: jMarkerKindSafe,
var: jMarkerVarSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
});
......@@ -112,12 +141,13 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
/** 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,
<{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
name: string, descr: string }>({
key: Compare.string,
kind: byMarkerKind,
var: byMarkerVar,
name: Compare.alpha,
descr: Compare.primitive,
descr: Compare.string,
});
/** Signal for array [`markerInfo`](#markerinfo) */
......@@ -197,6 +227,33 @@ export const jMarkerSafe: Json.Safe<marker> =
/** Natural order for `marker` */
export const byMarker: Compare.Order<marker> = Compare.structural;
/** Location: function and marker */
export interface location {
/** Function */
function: Json.key<'#fct'>;
/** Marker */
marker: marker;
}
/** Loose decoder for `location` */
export const jLocation: Json.Loose<location> =
Json.jObject({
function: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
marker: jMarkerSafe,
});
/** Safe decoder for `location` */
export const jLocationSafe: Json.Safe<location> =
Json.jFail(jLocation,'Location expected');
/** Natural order for `location` */
export const byLocation: Compare.Order<location> =
Compare.byFields
<{ function: Json.key<'#fct'>, marker: marker }>({
function: Compare.string,
marker: byMarker,
});
const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
......@@ -242,9 +299,9 @@ export const jFunctionsDataSafe: Json.Safe<functionsData> =
export const byFunctionsData: Compare.Order<functionsData> =
Compare.byFields
<{ key: Json.key<'#functions'>, name: string, signature: string }>({
key: Compare.primitive,
key: Compare.string,
name: Compare.alpha,
signature: Compare.primitive,
signature: Compare.string,
});
/** Signal for array [`functions`](#functions) */
......
......@@ -27,7 +27,7 @@ export const jMarkdownSafe: Json.Safe<markdown> =
Json.jFail(Json.jString,'String expected');
/** Natural order for `markdown` */
export const byMarkdown: Compare.Order<markdown> = Compare.primitive;
export const byMarkdown: Compare.Order<markdown> = Compare.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. */
export type text = null | string | text[];
......
......@@ -36,9 +36,9 @@ export const jProjectInfoSafe: Json.Safe<projectInfo> =
export const byProjectInfo: Compare.Order<projectInfo> =
Compare.byFields
<{ id: Json.key<'#project'>, name: string, current: boolean }>({
id: Compare.primitive,
id: Compare.string,
name: Compare.alpha,
current: Compare.primitive,
current: Compare.boolean,
});
/** Request to be executed on the specified project. */
......@@ -62,8 +62,8 @@ export const jProjectRequestSafe: Json.Safe<projectRequest> =
export const byProjectRequest: Compare.Order<projectRequest> =
Compare.byFields
<{ project: Json.key<'#project'>, request: string, data: Json.json }>({
project: Compare.primitive,
request: Compare.primitive,
project: Compare.string,
request: Compare.string,
data: Compare.structural,
});
......
......@@ -275,17 +275,17 @@ export const byStatusData: Compare.Order<statusData> =
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,
key: Compare.string,
descr: Compare.string,
kind: byPropKind,
names: Compare.array(Compare.primitive),
names: Compare.array(Compare.string),
status: byPropStatus,
function: Compare.defined(Compare.primitive),
kinstr: Compare.defined(Compare.primitive),
function: Compare.defined(Compare.string),
kinstr: Compare.defined(Compare.string),
source: bySource,
alarm: Compare.defined(Compare.primitive),
alarm_descr: Compare.defined(Compare.primitive),
predicate: Compare.defined(Compare.primitive),
alarm: Compare.defined(Compare.string),
alarm_descr: Compare.defined(Compare.string),
predicate: Compare.defined(Compare.string),
});
/** Signal for array [`status`](#status) */
......
......@@ -74,10 +74,10 @@ export const jSourceSafe: Json.Safe<source> =
export const bySource: Compare.Order<source> =
Compare.byFields
<{ dir: string, base: string, file: string, line: number }>({
dir: Compare.primitive,
base: Compare.primitive,
file: Compare.primitive,
line: Compare.primitive,
dir: Compare.string,
base: Compare.string,
file: Compare.string,
line: Compare.number,
});
/** Log messages categories. */
......@@ -149,8 +149,8 @@ export const byLog: Compare.Order<log> =
source?: source }>({
kind: byLogkind,
plugin: Compare.alpha,
message: Compare.primitive,
category: Compare.defined(Compare.primitive),
message: Compare.string,
category: Compare.defined(Compare.string),
source: Compare.defined(bySource),
});
......
This diff is collapsed.
/* --- Generated Frama-C Server API --- */
/**
Eva General Services
@packageDocumentation
@module api/plugins/eva/general
*/
//@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 { byMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarkerSafe } from 'api/kernel/ast';
//@ts-ignore
import { marker } from 'api/kernel/ast';
const getCallers_internal: Server.GetRequest<
Json.key<'#fct'>,
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.getCallers',
input: Json.jKey<'#fct'>('#fct'),
output: Json.jList(Json.jTry(
Json.jPair(
Json.jFail(Json.jKey<'#fct'>('#fct'),
'#fct expected'),
Json.jFail(Json.jKey<'#stmt'>('#stmt'),
'#stmt expected'),
))),
};
/** Get the list of call site of a function */
export const getCallers: Server.GetRequest<
Json.key<'#fct'>,
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
>= getCallers_internal;
/** Dead code. */
export interface deadCode {
/** List of unreachable statements of a function */
unreachable: marker[];
/** List of reachable but non terminating statements. */
nonTerminating: marker[];
}
/** Loose decoder for `deadCode` */
export const jDeadCode: Json.Loose<deadCode> =
Json.jObject({
unreachable: Json.jList(jMarker),
nonTerminating: Json.jList(jMarker),
});
/** Safe decoder for `deadCode` */
export const jDeadCodeSafe: Json.Safe<deadCode> =
Json.jFail(jDeadCode,'DeadCode expected');
/** Natural order for `deadCode` */
export const byDeadCode: Compare.Order<deadCode> =
Compare.byFields
<{ unreachable: marker[], nonTerminating: marker[] }>({
unreachable: Compare.array(byMarker),
nonTerminating: Compare.array(byMarker),
});
const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.general.getDeadCode',
input: Json.jKey<'#fct'>('#fct'),
output: jDeadCode,
};
/** Get the list of unreachable statements and non terminating statements in a function */
export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
/* ------------------------------------- */
/* --- Generated Frama-C Server API --- */
/**
Eva Values
@packageDocumentation
@module api/plugins/eva/values
*/
//@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 { byMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarkerSafe } from 'api/kernel/ast';
//@ts-ignore
import { marker } from 'api/kernel/ast';
/** CallStack */
export interface callstack {
/** Callstack id */
id: number;
/** Short name for the callstack */
short: string;
/** Full name for the callstack */
full: string;
}
/** Loose decoder for `callstack` */
export const jCallstack: Json.Loose<callstack> =
Json.jObject({
id: Json.jFail(Json.jNumber,'Number expected'),
short: Json.jFail(Json.jString,'String expected'),
full: Json.jFail(Json.jString,'String expected'),
});
/** Safe decoder for `callstack` */
export const jCallstackSafe: Json.Safe<callstack> =
Json.jFail(jCallstack,'Callstack expected');
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> =
Compare.byFields
<{ id: number, short: string, full: string }>({
id: Compare.number,
short: Compare.string,
full: Compare.string,
});
/** Data for array rows [`values`](#values) */
export interface valuesData {
/** Entry identifier. */
key: Json.key<'#values'>;
/** CallStack */
callstack: callstack;
/** Value inferred just before the selected point */
value_before: string;
/** Did the evaluation led to an alarm? */
alarm: boolean;
/** Value inferred just after the selected point */
value_after?: string;
}
/** Loose decoder for `valuesData` */
export const jValuesData: Json.Loose<valuesData> =
Json.jObject({
key: Json.jFail(Json.jKey<'#values'>('#values'),'#values expected'),
callstack: jCallstackSafe,
value_before: Json.jFail(Json.jString,'String expected'),
alarm: Json.jFail(Json.jBoolean,'Boolean expected'),
value_after: Json.jString,
});
/** Safe decoder for `valuesData` */
export const jValuesDataSafe: Json.Safe<valuesData> =
Json.jFail(jValuesData,'ValuesData expected');
/** Natural order for `valuesData` */
export const byValuesData: Compare.Order<valuesData> =
Compare.byFields
<{ key: Json.key<'#values'>, callstack: callstack, value_before: string,
alarm: boolean, value_after?: string }>({
key: Compare.string,
callstack: byCallstack,
value_before: Compare.string,
alarm: Compare.boolean,
value_after: Compare.defined(Compare.string),
});
/** Signal for array [`values`](#values) */
export const signalValues: Server.Signal = {
name: 'plugins.eva.values.signalValues',
};
const reloadValues_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.reloadValues',
input: Json.jNull,
output: Json.jNull,
};
/** Force full reload for array [`values`](#values) */
export const reloadValues: Server.GetRequest<null,null>= reloadValues_internal;
const fetchValues_internal: Server.GetRequest<
number,
{ pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.fetchValues',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jValuesData),
removed: Json.jList(Json.jKey<'#values'>('#values')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`values`](#values) */
export const fetchValues: Server.GetRequest<
number,
{ pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
reload: boolean }
>= fetchValues_internal;
const values_internal: State.Array<Json.key<'#values'>,valuesData> = {
name: 'plugins.eva.values.values',
getkey: ((d:valuesData) => d.key),
signal: signalValues,
fetch: fetchValues,
reload: reloadValues,
order: byValuesData,
};
/** Abstract values inferred by the Eva analysis */
export const values: State.Array<Json.key<'#values'>,valuesData> = values_internal;
const getValues_internal: Server.GetRequest<marker,null> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getValues',
input: jMarker,
output: Json.jNull,
};
/** Get the abstract values computed for an expression or lvalue */
export const getValues: Server.GetRequest<marker,null>= getValues_internal;
/* ------------------------------------- */
......@@ -74,6 +74,7 @@ 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"
| Jtag a -> Format.fprintf fmt "\"%s\"" a
| 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
......@@ -166,6 +167,7 @@ let rec makeDecoder ~safe ?self ~names fmt js =
| Jboolean -> jsafe ~safe "Boolean" jprim fmt "jBoolean"
| Jnumber -> jsafe ~safe "Number" jprim fmt "jNumber"
| Jstring | Jalpha -> jsafe ~safe "String" jprim fmt "jString"
| Jtag a -> Format.fprintf fmt "Json.jTag(\"%s\")" a
| Jkey kd -> jsafe ~safe ("#" ^ kd) jkey fmt kd
| Jindex kd -> jsafe ~safe ("#" ^ kd) jindex fmt kd
| Jdata id -> jcall names fmt (Pkg.Derived.decode ~safe id)
......@@ -186,6 +188,10 @@ let rec makeDecoder ~safe ?self ~names fmt js =
| Jrecord jfs -> jsafe ~safe "Record" (jrecord ~makeSafe) fmt jfs
| Jtuple jts -> jtry ~safe (jtuple ~makeSafe) fmt jts
let makeLooseNeedSafe = function
| Pkg.Jtuple _ | Pkg.Jarray _ -> true
| _ -> false
let makeRootDecoder ~safe ~self ~names fmt js =
let open Pkg in
match js with
......@@ -217,14 +223,13 @@ let makeOrder ~self ~names fmt js =
let rec pp fmt = function
| Jnull -> Format.pp_print_string fmt "Compare.equal"
| Jalpha -> Format.pp_print_string fmt "Compare.alpha"
| Jnumber | Jstring | Jboolean | Jkey _ | Jindex _
-> Format.pp_print_string fmt "Compare.primitive"
| Jnumber | Jindex _ -> Format.pp_print_string fmt "Compare.number"
| Jstring | Jkey _ -> Format.pp_print_string fmt "Compare.string"
| Jboolean -> Format.pp_print_string fmt "Compare.boolean"
| Jself -> jcall names fmt (Pkg.Derived.order self)
| Jdata id -> jcall names fmt (Pkg.Derived.order id)
| Joption js ->
Format.fprintf fmt "@[<hov 2>Compare.defined(@,%a)@]" pp js
| Jany | Junion _ -> (* Can not find a better solution *)
Format.fprintf fmt "Compare.structural"
| Jenum id ->
Format.fprintf fmt "@[<hov 2>Compare.byEnum(@,%a)@]" (jcall names) id
| Jlist js | Jarray js ->
......@@ -250,6 +255,8 @@ let makeOrder ~self ~names fmt js =
Format.fprintf fmt
"@[<hov 2>Compare.dictionary<@,Json.dict<'#%s'@,%a>>(@,%a)@]"
kd jtype js pp js
| Jany | Junion _ | Jtag _ ->
Format.fprintf fmt "Compare.structural"
in pp fmt js
(* -------------------------------------------------------------------------- *)
......@@ -411,12 +418,13 @@ let makeDeclaration fmt names d =
type ranking = {
mutable rank : int ;
mutable mark : int Pkg.IdMap.t ;
index : Pkg.declInfo Pkg.IdMap.t ;
}
let depends d =
match d.Pkg.d_kind with
| D_loose(id,(Jtuple _ | Jarray _)) -> [Pkg.Derived.safe id]
| D_safe(id,_) -> [Pkg.Derived.loose id]
| D_loose(id,t) when makeLooseNeedSafe t -> [Pkg.Derived.safe id]
| D_safe(id,t) when not (makeLooseNeedSafe t) -> [Pkg.Derived.loose id]
| D_array _ ->
let id = d.d_ident in
let data = Pkg.Derived.data id in
......@@ -436,13 +444,20 @@ let next m id =
m.mark <- Pkg.IdMap.add id r m.mark ;
m.rank <- succ r
let mark m d =
let rec mark m d =
let id = d.Pkg.d_ident in
if not (Pkg.IdMap.mem id m.mark) then
( List.iter (next m) (depends d) ; next m id )
( List.iter (mark_id m) (depends d) ; next m id )
and mark_id m id =
try mark m (Pkg.IdMap.find id m.index)
with Not_found -> ()
let ranking ds =
let m = { rank = 0 ; mark = Pkg.IdMap.empty } in
let index = List.fold_left
(fun m d -> Pkg.IdMap.add d.Pkg.d_ident d m)
Pkg.IdMap.empty ds in
let m = { rank = 0 ; mark = Pkg.IdMap.empty ; index } in
List.iter (mark m) ds ;
let rk = m.mark in
let getRank a = try Pkg.IdMap.find a.Pkg.d_ident rk with Not_found -> 0 in
......
......@@ -22,6 +22,7 @@
"@babel/preset-typescript": "^7.9.0",
"@hot-loader/react-dom": "^16.13.0",
"@types/codemirror": "^0.0.89",
"@types/cytoscape": "^3.14.5",
"@types/lodash": "^4.14.149",
"@types/node": "12.12.21",
"@types/react": "^16.9.17",
......@@ -33,7 +34,7 @@
"css-loader": "^3.4.0",
"electron": "^7",
"electron-builder": "^22.4.1",
"electron-devtools-installer": "^2.2.4",
"electron-devtools-installer": "^3.0.0",
"electron-webpack": "^2.8.2",
"eslint": "^6.8.0",
"eslint-config-airbnb": "^18.1.0",
......@@ -53,15 +54,25 @@
},
"dependencies": {
"@babel/runtime": "^7.9.2",
"@fortawesome/fontawesome-free": "^5.13.1",
"codemirror": "^5.52.2",
"cytoscape": "^3.15.1",
"cytoscape-cola": "^2.3.1",
"cytoscape-cose-bilkent": "^4.1.0",
"cytoscape-cxtmenu": "^3.1.2",
"cytoscape-dagre": "^2.2.2",
"cytoscape-klay": "^3.1.3",
"cytoscape-popper": "^1.0.7",
"immutable": "^4.0.0-rc.12",
"lodash": "^4.17.15",
"react": "^16.8",
"react-cytoscapejs": "^1.2.1",
"react-dom": "^16.13.1",
"react-draggable": "^4.2.0",
"react-fast-compare": "^3.2.0",
"react-virtualized": "^9.21.2",
"source-map-support": "^0.5.16",
"tippy.js": "5.2.1",
"zeromq": "^6.0.0-beta.5"
}
}
......@@ -392,7 +392,10 @@ function createPrimaryWindow()
// React Developper Tools
if (DEVEL)
installExtension(REACT_DEVELOPER_TOOLS,true);
installExtension(REACT_DEVELOPER_TOOLS,true)
.catch((err) => {
console.error('[Dome] Enable to install React dev-tools',err);
});
const cwd = process.cwd();
const wdir = cwd === '/' ? app.getPath('home') : cwd ;
const argv = stripElectronArgv(process.argv);
......
......@@ -8,5 +8,5 @@ export const REACT_DEVELOPER_TOOLS = undefined ;
// Shall not be used in non-development mode
export default function installExtension(_id) {
return Promise.reject();
return Promise.resolve();
}
......@@ -41,28 +41,37 @@ export function isBigNum(x: any): x is bignum {
return typeof (x) === 'bigint' || (typeof (x) === 'number' && !Number.isNaN(x));
}
/**
Primitive comparison.
Can only compare arguments that have
comparable primitive type.
This includes symbols, boolean, non-NaN numbers, bigints and strings.
Numbers and big-ints can also be compared with each others.
*/
export function primitive(x: symbol, y: symbol): number;
export function primitive(x: boolean, y: boolean): number;
export function primitive(x: bignum, y: bignum): number;
export function primitive(x: string, y: string): number;
export function primitive(x: any, y: any) {
/** @internal */
function primitive(x: any, y: any) {
if (x < y) return -1;
if (x > y) return 1;
return 0;
}
/**
Primitive comparison for numbers (NaN included).
Primitive comparison for symbols.
*/
export const symbol: Order<symbol> = primitive;
/**
Primitive comparison for booleans.
*/
export const boolean: Order<boolean> = primitive;
/**
Primitive comparison for strings. See also [[alpha]].
*/
export const string: Order<string> = primitive;
/**
Primitive comparison for (big) integers (non NaN numbers included).
*/
export const bignum: Order<bignum> = primitive;
/**
Primitive comparison for number (NaN included).
*/
export function float(x: number, y: number) {
export function number(x: number, y: number) {
const nx = Number.isNaN(x);
const ny = Number.isNaN(y);
if (nx && ny) return 0;
......
......@@ -118,6 +118,15 @@ export const jString: Loose<string> = (js: json) => (
typeof js === 'string' ? js : undefined
);
/** JSON constant.
Capture the tag or returns `undefined`.
Can be used with [[jUnion]], although [[jEnum]]
might be more efficient.
*/
export function jTag<A>(tg: A): Loose<A> {
return (js: json) => Object.is(js, tg) ? tg : undefined;
}
/**
Lookup tags in a dictionary.
Can be used directly for enum types, eg. `jEnum(myEnumType)`.
......@@ -179,7 +188,7 @@ export function jCatch<A>(fn: Loose<A>, fallBack: A): Safe<A> {
try {
return fn(js) ?? fallBack;
} catch (err) {
if (DEVEL) console.error('[Dome.json]', err);
if (DEVEL) console.warn('[Dome.json]', err);
return fallBack;
}
};
......@@ -193,7 +202,8 @@ export function jTry<A>(fn: Loose<A>, defaultValue?: A): Loose<A> {
return (js: json) => {
try {
return fn(js) ?? defaultValue;
} catch (_err) {
} catch (err) {
if (DEVEL) console.warn('[Dome.json]', err);
return defaultValue;
}
};
......
......@@ -429,7 +429,7 @@ export class ArrayModel<Key, Row>
// --------------------------------------------------------------------------
/**
@template Row - object data that also contains their « key »
@template Row - object data that also contains their « key ».
*/
export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
......@@ -448,13 +448,17 @@ export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
Requires a final trigger to update views. */
updateData(data: Collection<Row>) {
forEach(data, (row: Row) => this.setData(this.getkey(row), row));
this.reload();
}
/**
Replace all previous data with the new one.
Replace all previous data with the new ones.
Finally triggers a reload.
*/
replaceAllDataWith(data: Collection<Row>) {
this.removeAllData();
this.updateData(data);
this.reload();
}
}
......
......@@ -235,15 +235,21 @@ export abstract class Model<Key, Row> {
// --------------------------------------------------------------------------
/**
For a component to re-render on any updates and reloads.
The returned number can be used to memoise effects and callbacks.
Make the component to synchronize with the model and re-render on
every updates.
@param sync - whether to synchronize on model updates or not, `true`
by default.
@return a number that can be used to memoize other effects
*/
export function useModel(model: Model<any, any>): number {
export function useModel(model: Model<any, any>, sync = true): number {
const [age, setAge] = React.useState(0);
React.useEffect(() => {
const w = model.link(() => setImmediate(() => setAge(age + 1)));
return w.unlink;
if (sync) {
const w = model.link(() => setImmediate(() => setAge(age + 1)));
return w.unlink;
}
return undefined;
});
return age;
}
......
......@@ -59,6 +59,14 @@ export type RenderByFields<Row> = {
export type index = number | number[]
/**
Column Properties.
__Warning:__ callback properties, namely `getter`, `render`
and `onContextMenu`, shall be as stable as possible to prevent
the table from constantly re-rendering.