Skip to content

GitLab

Commits (177)
Hide whitespace changes
Inline Side-by-side
Makefile
View file @ 9b464ff0
......@@ -538,7 +538,6 @@ KERNEL_CMO=\
src/kernel_internals/parsing/errorloc.cmo \
src/kernel_services/ast_printing/cil_printer.cmo \
src/kernel_services/ast_printing/cil_descriptive_printer.cmo \
src/kernel_services/parsetree/cabs.cmo \
src/kernel_services/parsetree/cabshelper.cmo \
src/kernel_services/ast_queries/logic_utils.cmo \
src/kernel_services/ast_printing/logic_print.cmo \
......@@ -640,7 +639,8 @@ MLI_ONLY+=\
src/libraries/utils/hptmap_sig.mli \
src/kernel_services/cmdline_parameters/parameter_sig.mli \
src/kernel_services/ast_data/cil_types.mli \
src/kernel_services/parsetree/logic_ptree.mli \
src/kernel_services/parsetree/cabs.mli \
src/kernel_services/parsetree/logic_ptree.mli \
src/kernel_services/ast_printing/printer_api.mli \
src/kernel_services/abstract_interp/float_sig.mli \
src/kernel_services/abstract_interp/float_interval_sig.mli \
......@@ -652,15 +652,6 @@ MLI_ONLY+=\
src/kernel_services/abstract_interp/lmap_sig.mli \
src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
NO_MLI+= src/kernel_services/parsetree/cabs.mli \
src/kernel_internals/runtime/machdep_ppc_32.mli \
src/kernel_internals/runtime/machdep_x86_16.mli \
src/kernel_internals/runtime/machdep_x86_32.mli \
src/kernel_internals/runtime/machdep_x86_64.mli \
src/kernel_services/ast_printing/cabs_debug.mli \
src/kernel_internals/parsing/logic_lexer.mli \
src/kernel_internals/parsing/lexerhack.mli \
MODULES_NODOC+= src/kernel_internals/runtime/machdep_ppc_32.ml \
src/kernel_internals/runtime/machdep_x86_16.ml \
src/kernel_internals/runtime/machdep_x86_32.ml \
......@@ -1219,8 +1210,7 @@ FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \
$(addsuffix /*.ml,$(FRAMAC_SRC_DIRS))
MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
$(MLI_ONLY) $(NO_MLI:.mli=.ml) \
$(filter-out $(NO_MLI),\
$(MLI_ONLY) \
$(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli))))
################################
......
configure.in
View file @ 9b464ff0
......@@ -396,9 +396,9 @@ AC_ARG_ENABLE(
ENABLE_LANDMARKS=yes)
if test "$ENABLE_LANDMARKS" = yes ; then
AC_MSG_CHECKING(for Landmarks)
AC_MSG_CHECKING(for Landmarks and Landmarks-ppx)
LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks-ppx 2>/dev/null | tr -d '\r\n')
if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
HAS_LANDMARKS="yes";
AC_MSG_RESULT(found)
......
headers/header_spec.txt
View file @ 9b464ff0
......@@ -380,6 +380,7 @@ src/kernel_internals/parsing/cparser.mly: CIL
src/kernel_internals/parsing/errorloc.ml: CIL
src/kernel_internals/parsing/errorloc.mli: CIL
src/kernel_internals/parsing/lexerhack.ml: CIL
src/kernel_internals/parsing/lexerhack.mli: CIL
src/kernel_internals/parsing/logic_lexer.mli: CEA_INRIA_LGPL
src/kernel_internals/parsing/logic_lexer.mll: CEA_INRIA_LGPL
src/kernel_internals/parsing/logic_parser.mly: CEA_INRIA_LGPL
......@@ -615,7 +616,7 @@ src/kernel_services/cmdline_parameters/parameter_state.mli: CEA_LGPL
src/kernel_services/cmdline_parameters/typed_parameter.ml: CEA_LGPL
src/kernel_services/cmdline_parameters/typed_parameter.mli: CEA_LGPL
src/kernel_services/parsetree/README.md: .ignore
src/kernel_services/parsetree/cabs.ml: CIL
src/kernel_services/parsetree/cabs.mli: CIL
src/kernel_services/parsetree/cabshelper.ml: CIL
src/kernel_services/parsetree/cabshelper.mli: CIL
src/kernel_services/parsetree/logic_ptree.mli: CEA_INRIA_LGPL
......@@ -1426,6 +1427,7 @@ src/plugins/value/utils/red_statuses.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
......
ivette/.gitignore
View file @ 9b464ff0
......@@ -3,6 +3,7 @@
# --------------------------------------------------------------------------
.ivette
.frama-c
.dome-*.stamp
.dome-*.back
.eslint-cache
......
ivette/src/dome/main/dome.ts
View file @ 9b464ff0
......@@ -500,6 +500,7 @@ function showSettingsWindow() {
maximizable: false,
minimizable: false,
});
PreferenceWindow.setMenuBarVisibility(false);
PreferenceWindow.show();
PreferenceWindow.on('closed', () => { PreferenceWindow = undefined; });
}
......
ivette/src/dome/renderer/dialogs.tsx
View file @ 9b464ff0
......@@ -157,7 +157,7 @@ export interface FileFilter {
export interface FileDialogProps {
/** Prompt message. */
message?: string;
title?: string;
/** Open button label (default is « Open »). */
label?: string;
/** Initially selected path. */
......@@ -196,11 +196,11 @@ export interface OpenDirProps extends FileDialogProps {
export async function showOpenFile(
props: OpenFileProps,
): Promise<string | undefined> {
const { message, label, path, hidden = false, filters } = props;
const { title, label, path, hidden = false, filters } = props;
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
message,
title,
buttonLabel: label,
defaultPath: path && defaultPath(path),
properties: (hidden ? ['openFile', 'showHiddenFiles'] : ['openFile']),
......@@ -219,12 +219,12 @@ export async function showOpenFile(
export async function showOpenFiles(
props: OpenFileProps,
): Promise<string[] | undefined> {
const { message, label, path, hidden, filters } = props;
const { title, label, path, hidden, filters } = props;
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
message,
title,
buttonLabel: label,
defaultPath: path && defaultPath(path),
properties: (
......@@ -257,11 +257,11 @@ export async function showOpenFiles(
export async function showSaveFile(
props: SaveFileProps,
): Promise<string | undefined> {
const { message, label, path, filters } = props;
const { title, label, path, filters } = props;
return remote.dialog.showSaveDialog(
remote.getCurrentWindow(),
{
message,
title,
buttonLabel: label,
defaultPath: path,
filters,
......@@ -282,7 +282,7 @@ type openDirProperty =
export async function showOpenDir(
props: OpenDirProps,
): Promise<string | undefined> {
const { message, label, path, hidden } = props;
const { title, label, path, hidden } = props;
const properties: openDirProperty[] = ['openDirectory'];
if (hidden) properties.push('showHiddenFiles');
......@@ -295,7 +295,7 @@ export async function showOpenDir(
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
message,
title,
buttonLabel: label,
defaultPath: path,
properties,
......
ivette/src/frama-c/api/generated/kernel/ast/index.ts
View file @ 9b464ff0
......@@ -67,10 +67,16 @@ const compute_internal: Server.ExecRequest<null,null> = {
name: 'kernel.ast.compute',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Ensures that AST is computed */
export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Emitted when the AST has been changed */
export const changed: Server.Signal = {
name: 'kernel.ast.changed',
};
/** Marker kind */
export enum markerKind {
/** Expression */
......@@ -105,6 +111,7 @@ const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.ast.markerKindTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
......@@ -135,6 +142,7 @@ const markerVarTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.ast.markerVarTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_internal;
......@@ -193,6 +201,7 @@ const reloadMarkerInfo_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadMarkerInfo',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Force full reload for array [`markerInfo`](#markerinfo) */
export const reloadMarkerInfo: Server.GetRequest<null,null>= reloadMarkerInfo_internal;
......@@ -211,6 +220,7 @@ const fetchMarkerInfo_internal: Server.GetRequest<
removed: Json.jList(Json.jString),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
export const fetchMarkerInfo: Server.GetRequest<
......@@ -284,11 +294,30 @@ export const byLocation: Compare.Order<location> =
marker: byMarker,
});
const getMainFunction_internal: Server.GetRequest<
null,
Json.key<'#fct'> |
undefined
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getMainFunction',
input: Json.jNull,
output: Json.jKey<'#fct'>('#fct'),
signals: [],
};
/** Get the current 'main' function. */
export const getMainFunction: Server.GetRequest<
null,
Json.key<'#fct'> |
undefined
>= getMainFunction_internal;
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')),
signals: [],
};
/** Collect all functions in the AST */
export const getFunctions: Server.GetRequest<null,Json.key<'#fct'>[]>= getFunctions_internal;
......@@ -298,6 +327,7 @@ const printFunction_internal: Server.GetRequest<Json.key<'#fct'>,text> = {
name: 'kernel.ast.printFunction',
input: Json.jKey<'#fct'>('#fct'),
output: jText,
signals: [],
};
/** Print the AST of a function */
export const printFunction: Server.GetRequest<Json.key<'#fct'>,text>= printFunction_internal;
......@@ -370,6 +400,7 @@ const reloadFunctions_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadFunctions',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Force full reload for array [`functions`](#functions) */
export const reloadFunctions: Server.GetRequest<null,null>= reloadFunctions_internal;
......@@ -388,6 +419,7 @@ const fetchFunctions_internal: Server.GetRequest<
removed: Json.jList(Json.jKey<'#functions'>('#functions')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
/** Data fetcher for array [`functions`](#functions) */
export const fetchFunctions: Server.GetRequest<
......@@ -412,6 +444,7 @@ const getInfo_internal: Server.GetRequest<marker,text> = {
name: 'kernel.ast.getInfo',
input: jMarker,
output: jText,
signals: [],
};
/** Get textual information about a marker */
export const getInfo: Server.GetRequest<marker,text>= getInfo_internal;
......@@ -421,6 +454,7 @@ const getFiles_internal: Server.GetRequest<null,string[]> = {
name: 'kernel.ast.getFiles',
input: Json.jNull,
output: Json.jList(Json.jString),
signals: [],
};
/** Get the currently analyzed source file names */
export const getFiles: Server.GetRequest<null,string[]>= getFiles_internal;
......@@ -430,6 +464,7 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
name: 'kernel.ast.setFiles',
input: Json.jList(Json.jString),
output: Json.jNull,
signals: [],
};
/** Set the source file names to analyze. */
export const setFiles: Server.SetRequest<string[],null>= setFiles_internal;
......
ivette/src/frama-c/api/generated/kernel/project/index.ts
View file @ 9b464ff0
......@@ -94,6 +94,7 @@ const getCurrent_internal: Server.GetRequest<null,projectInfo> = {
name: 'kernel.project.getCurrent',
input: Json.jNull,
output: jProjectInfo,
signals: [],
};
/** Returns the current project */
export const getCurrent: Server.GetRequest<null,projectInfo>= getCurrent_internal;
......@@ -103,6 +104,7 @@ const setCurrent_internal: Server.SetRequest<Json.key<'#project'>,null> = {
name: 'kernel.project.setCurrent',
input: Json.jKey<'#project'>('#project'),
output: Json.jNull,
signals: [],
};
/** Switches the current project */
export const setCurrent: Server.SetRequest<Json.key<'#project'>,null>= setCurrent_internal;
......@@ -112,6 +114,7 @@ const getList_internal: Server.GetRequest<null,projectInfo[]> = {
name: 'kernel.project.getList',
input: Json.jNull,
output: Json.jList(jProjectInfo),
signals: [],
};
/** Returns the list of all projects */
export const getList: Server.GetRequest<null,projectInfo[]>= getList_internal;
......@@ -121,6 +124,7 @@ const getOn_internal: Server.GetRequest<projectRequest,Json.json> = {
name: 'kernel.project.getOn',
input: jProjectRequest,
output: Json.jAny,
signals: [],
};
/** Execute a GET request within the given project */
export const getOn: Server.GetRequest<projectRequest,Json.json>= getOn_internal;
......@@ -130,6 +134,7 @@ const setOn_internal: Server.SetRequest<projectRequest,Json.json> = {
name: 'kernel.project.setOn',
input: jProjectRequest,
output: Json.jAny,
signals: [],
};
/** Execute a SET request within the given project */
export const setOn: Server.SetRequest<projectRequest,Json.json>= setOn_internal;
......@@ -139,6 +144,7 @@ const execOn_internal: Server.ExecRequest<projectRequest,Json.json> = {
name: 'kernel.project.execOn',
input: jProjectRequest,
output: Json.jAny,
signals: [],
};
/** Execute an EXEC request within the given project */
export const execOn: Server.ExecRequest<projectRequest,Json.json>= execOn_internal;
......@@ -148,6 +154,7 @@ const create_internal: Server.SetRequest<string,projectInfo> = {
name: 'kernel.project.create',
input: Json.jString,
output: jProjectInfo,
signals: [],
};
/** Create a new project */
export const create: Server.SetRequest<string,projectInfo>= create_internal;
......
ivette/src/frama-c/api/generated/kernel/properties/index.ts
View file @ 9b464ff0
......@@ -141,6 +141,7 @@ const propKindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.propKindTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const propKindTags: Server.GetRequest<null,tag[]>= propKindTags_internal;
......@@ -187,6 +188,7 @@ const propStatusTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.propStatusTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const propStatusTags: Server.GetRequest<null,tag[]>= propStatusTags_internal;
......@@ -246,6 +248,7 @@ const alarmsTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.alarmsTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const alarmsTags: Server.GetRequest<null,tag[]>= alarmsTags_internal;
......@@ -326,6 +329,7 @@ const reloadStatus_internal: Server.GetRequest<null,null> = {
name: 'kernel.properties.reloadStatus',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Force full reload for array [`status`](#status) */
export const reloadStatus: Server.GetRequest<null,null>= reloadStatus_internal;
......@@ -344,6 +348,7 @@ const fetchStatus_internal: Server.GetRequest<
removed: Json.jList(Json.jKey<'#property'>('#property')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
/** Data fetcher for array [`status`](#status) */
export const fetchStatus: Server.GetRequest<
......
ivette/src/frama-c/api/generated/kernel/services/index.ts
View file @ 9b464ff0
......@@ -59,6 +59,7 @@ const getConfig_internal: Server.GetRequest<
datadir: Json.jFail(Json.jString,'String expected'),
version: Json.jFail(Json.jString,'String expected'),
}),
signals: [],
};
/** Frama-C Kernel configuration */
export const getConfig: Server.GetRequest<
......@@ -71,10 +72,21 @@ const load_internal: Server.SetRequest<string,string | undefined> = {
name: 'kernel.services.load',
input: Json.jString,
output: Json.jString,
signals: [],
};
/** Load a save file. Returns an error, if not successfull. */
export const load: Server.SetRequest<string,string | undefined>= load_internal;
const save_internal: Server.SetRequest<string,string | undefined> = {
kind: Server.RqKind.SET,
name: 'kernel.services.save',
input: Json.jString,
output: Json.jString,
signals: [],
};
/** Save the current session. Returns an error, if not successfull. */
export const save: Server.SetRequest<string,string | undefined>= save_internal;
/** Source file positions. */
export type source =
{ dir: string, base: string, file: string, line: number };
......@@ -133,6 +145,7 @@ const logkindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.services.logkindTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const logkindTags: Server.GetRequest<null,tag[]>= logkindTags_internal;
......@@ -181,6 +194,7 @@ const setLogs_internal: Server.SetRequest<boolean,null> = {
name: 'kernel.services.setLogs',
input: Json.jBoolean,
output: Json.jNull,
signals: [],
};
/** Turn logs monitoring on/off */
export const setLogs: Server.SetRequest<boolean,null>= setLogs_internal;
......@@ -190,6 +204,7 @@ const getLogs_internal: Server.GetRequest<null,log[]> = {
name: 'kernel.services.getLogs',
input: Json.jNull,
output: Json.jList(jLog),
signals: [],
};
/** Flush the last emitted logs since last call (max 100) */
export const getLogs: Server.GetRequest<null,log[]>= getLogs_internal;
......
ivette/src/frama-c/api/generated/plugins/dive/index.ts
View file @ 9b464ff0
......@@ -315,6 +315,7 @@ const window_internal: Server.SetRequest<explorationWindow,null> = {
name: 'plugins.dive.window',
input: jExplorationWindow,
output: Json.jNull,
signals: [],
};
/** Set the exploration window */
export const window: Server.SetRequest<explorationWindow,null>= window_internal;
......@@ -324,6 +325,7 @@ const graph_internal: Server.GetRequest<null,graphData> = {
name: 'plugins.dive.graph',
input: Json.jNull,
output: jGraphData,
signals: [],
};
/** Retrieve the whole graph */
export const graph: Server.GetRequest<null,graphData>= graph_internal;
......@@ -333,6 +335,7 @@ const clear_internal: Server.ExecRequest<null,null> = {
name: 'plugins.dive.clear',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Erase the graph and start over with an empty one */
export const clear: Server.ExecRequest<null,null>= clear_internal;
......@@ -342,6 +345,7 @@ const add_internal: Server.ExecRequest<marker,diffData> = {
name: 'plugins.dive.add',
input: jMarker,
output: jDiffData,
signals: [],
};
/** Add a node to the graph */
export const add: Server.ExecRequest<marker,diffData>= add_internal;
......@@ -351,6 +355,7 @@ const explore_internal: Server.ExecRequest<nodeId,diffData> = {
name: 'plugins.dive.explore',
input: jNodeId,
output: jDiffData,
signals: [],
};
/** Explore the graph starting from an existing vertex */
export const explore: Server.ExecRequest<nodeId,diffData>= explore_internal;
......@@ -360,6 +365,7 @@ const show_internal: Server.ExecRequest<nodeId,diffData> = {
name: 'plugins.dive.show',
input: jNodeId,
output: jDiffData,
signals: [],
};
/** Show the dependencies of an existing vertex */
export const show: Server.ExecRequest<nodeId,diffData>= show_internal;
......@@ -369,6 +375,7 @@ const hide_internal: Server.ExecRequest<nodeId,diffData> = {
name: 'plugins.dive.hide',
input: jNodeId,
output: jDiffData,
signals: [],
};
/** Hide the dependencies of an existing vertex */
export const hide: Server.ExecRequest<nodeId,diffData>= hide_internal;
......
ivette/src/frama-c/api/generated/plugins/eva/general/index.ts
View file @ 9b464ff0
......@@ -59,6 +59,7 @@ const isComputed_internal: Server.GetRequest<null,boolean> = {
name: 'plugins.eva.general.isComputed',
input: Json.jNull,
output: Json.jBoolean,
signals: [],
};
/** True if the Eva analysis has been done */
export const isComputed: Server.GetRequest<null,boolean>= isComputed_internal;
......@@ -76,6 +77,7 @@ const getCallers_internal: Server.GetRequest<
Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
Json.jFail(Json.jKey<'#stmt'>('#stmt'),'#stmt expected'),
))),
signals: [],
};
/** Get the list of call site of a function */
export const getCallers: Server.GetRequest<
......@@ -115,21 +117,28 @@ const getDeadCode_internal: Server.GetRequest<Json.key<'#fct'>,deadCode> = {
name: 'plugins.eva.general.getDeadCode',
input: Json.jKey<'#fct'>('#fct'),
output: jDeadCode,
signals: [],
};
/** Get the lists of unreachable and of non terminating statements in a function */
export const getDeadCode: Server.GetRequest<Json.key<'#fct'>,deadCode>= getDeadCode_internal;
/** TODO */
/** Taint status of logical properties */
export enum taintStatus {
/** The Eva taint analysis has not been computed */
/** **Not computed:**
the Eva taint domain has not been enabled, or the Eva analysis has not been run */
not_computed = 'not_computed',
/** Error: the memory zone on which this property depends could not be computed */
/** **Error:**
the memory zone on which this property depends could not be computed */
error = 'error',
/** No taint for this kind of property */
/** **Not applicable:** no taint for this kind of property */
not_applicable = 'not_applicable',
/** Tainted property: this property is related to a memory zone that can be affected by an attacker, according to the Eva taint domain. */
tainted = 'tainted',
/** Untainted property: this property is safe, according to the Eva taint domain. */
/** **Data tainted:**
this property is related to a memory location that can be affected by an attacker */
data_tainted = 'data_tainted',
/** **Control tainted:**
this property is related to a memory location whose assignment depends on path conditions that can be affected by an attacker */
control_tainted = 'control_tainted',
/** **Untainted property:** this property is safe */
not_tainted = 'not_tainted',
}
......@@ -150,6 +159,7 @@ const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.eva.general.taintStatusTags',
input: Json.jNull,
output: Json.jList(jTag),
signals: [],
};
/** Registered tags for the above type. */
export const taintStatusTags: Server.GetRequest<null,tag[]>= taintStatusTags_internal;
......@@ -195,6 +205,7 @@ const reloadProperties_internal: Server.GetRequest<null,null> = {
name: 'plugins.eva.general.reloadProperties',
input: Json.jNull,
output: Json.jNull,
signals: [],
};
/** Force full reload for array [`properties`](#properties) */
export const reloadProperties: Server.GetRequest<null,null>= reloadProperties_internal;
......@@ -213,6 +224,7 @@ const fetchProperties_internal: Server.GetRequest<
removed: Json.jList(Json.jKey<'#property'>('#property')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
/** Data fetcher for array [`properties`](#properties) */
export const fetchProperties: Server.GetRequest<
......
ivette/src/frama-c/api/generated/plugins/eva/values/index.ts
View file @ 9b464ff0
......@@ -70,6 +70,7 @@ const getCallstacks_internal: Server.GetRequest<marker[],callstack[]> = {
name: 'plugins.eva.values.getCallstacks',
input: Json.jList(jMarker),
output: Json.jList(jCallstack),
signals: [],
};
/** Callstacks for markers */
export const getCallstacks: Server.GetRequest<marker[],callstack[]>= getCallstacks_internal;
......@@ -89,6 +90,7 @@ const getCallstackInfo_internal: Server.GetRequest<
stmt: Json.jKey<'#stmt'>('#stmt'),
rank: Json.jNumber,
})),
signals: [],
};
/** Callstack Description */
export const getCallstackInfo: Server.GetRequest<
......@@ -108,6 +110,7 @@ const getStmtInfo_internal: Server.GetRequest<
rank: Json.jFail(Json.jNumber,'Number expected'),
fct: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
}),
signals: [],
};
/** Stmt Information */
export const getStmtInfo: Server.GetRequest<
......@@ -130,6 +133,7 @@ const getProbeInfo_internal: Server.GetRequest<
stmt: Json.jKey<'#stmt'>('#stmt'),
code: Json.jString,
}),
signals: [],
};
/** Probe informations */
export const getProbeInfo: Server.GetRequest<
......@@ -163,6 +167,7 @@ const getValues_internal: Server.GetRequest<
Json.jFail(Json.jString,'String expected'),
))),
}),
signals: [],
};
/** Abstract values for the given marker */
export const getValues: Server.GetRequest<
......
ivette/src/frama-c/api/generated/plugins/studia/studia/index.ts
View file @ 9b464ff0
......@@ -89,6 +89,7 @@ const getReadsLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
name: 'plugins.studia.studia.getReadsLval',
input: Json.jKey<'#lval'>('#lval'),
output: jEffects,
signals: [],
};
/** Get the list of statements that read a lval. */
export const getReadsLval: Server.GetRequest<Json.key<'#lval'>,effects>= getReadsLval_internal;
......@@ -98,6 +99,7 @@ const getWritesLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
name: 'plugins.studia.studia.getWritesLval',
input: Json.jKey<'#lval'>('#lval'),
output: jEffects,
signals: [],
};
/** Get the list of statements that write a lval. */
export const getWritesLval: Server.GetRequest<Json.key<'#lval'>,effects>= getWritesLval_internal;
......
ivette/src/frama-c/api/generator.ml
View file @ 9b464ff0
......@@ -335,6 +335,10 @@ let makeDeclaration fmt names d =
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
Format.fprintf fmt " input: %a,@\n" makeParam input ;
Format.fprintf fmt " output: %a,@\n" makeParam output ;
Format.fprintf fmt " signals: [%a],@\n"
(Pretty_utils.pp_list ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
(fun fmt s -> Format.fprintf fmt "{ name: '%s' }" s))
rq.rq_signals;
Format.fprintf fmt "};@\n" ;
makeDescr fmt d.d_descr ;
Format.fprintf fmt
......@@ -432,6 +436,19 @@ let depends d =
match d.Pkg.d_kind with
| D_loose(id,t) when makeLooseNeedSafe t -> [Pkg.Derived.safe id]
| D_safe(id,t) when not (makeLooseNeedSafe t) -> [Pkg.Derived.loose id]
| D_value _ ->
let id = d.d_ident in
[
Pkg.Derived.signal id;
Pkg.Derived.getter id
]
| D_state _ ->
let id = d.d_ident in
[
Pkg.Derived.signal id;
Pkg.Derived.getter id;
Pkg.Derived.setter id
]
| D_array _ ->
let id = d.d_ident in
let data = Pkg.Derived.data id in
......
ivette/src/frama-c/index.tsx
View file @ 9b464ff0
......@@ -29,6 +29,7 @@ import * as Ivette from 'ivette';
import History from 'frama-c/kernel/History';
import Globals from 'frama-c/kernel/Globals';
import Status from 'frama-c/kernel/Status';
import ASTview from 'frama-c/kernel/ASTview';
import ASTinfo from 'frama-c/kernel/ASTinfo';
import SourceCode from 'frama-c/kernel/SourceCode';
......@@ -37,6 +38,10 @@ import Properties from 'frama-c/kernel/Properties';
import 'frama-c/kernel/style.css';
import * as Menu from 'frama-c/menu';
Menu.init();
/* --------------------------------------------------------------------------*/
/* --- Frama-C Kernel Groups ---*/
/* --------------------------------------------------------------------------*/
......@@ -47,6 +52,7 @@ Ivette.registerGroup({
}, () => {
Ivette.registerSidebar({ id: 'frama-c.globals', children: <Globals /> });
Ivette.registerToolbar({ id: 'frama-c.history', children: <History /> });
Ivette.registerStatusbar({ id: 'frama-c.message', children: <Status /> });
Ivette.registerComponent({
id: 'frama-c.astview',
label: 'AST',
......@@ -89,3 +95,17 @@ Ivette.registerGroup({
});
/* --------------------------------------------------------------------------*/
/* --- Frama-C Views ---*/
/* --------------------------------------------------------------------------*/
Ivette.registerView({
id: 'source',
rank: 1,
label: 'Source Code',
layout: [
['frama-c.astview', 'frama-c.sourcecode'],
'frama-c.astinfo',
],
});
/* --------------------------------------------------------------------------*/
ivette/src/frama-c/kernel/ASTview.tsx
View file @ 9b464ff0
......@@ -201,14 +201,20 @@ export default function ASTview() {
return () => { buffer.off('change', setBullets); };
}, [buffer, setBullets]);
async function reload() {
printed.current = theFunction;
loadAST(buffer, theFunction, theMarker);
}
// Hook: async loading
React.useEffect(() => {
if (printed.current !== theFunction) {
printed.current = theFunction;
loadAST(buffer, theFunction, theMarker);
}
if (printed.current !== theFunction)
reload();
});
// Also reload the buffer when the AST is recomputed.
Server.onSignal(Ast.changed, reload);
React.useEffect(() => {
const decorator = (marker: string) => {
if (multipleSelections?.some((location) => location?.marker === marker))
......
ivette/src/frama-c/kernel/Properties.tsx
View file @ 9b464ff0
......@@ -99,7 +99,8 @@ const DEFAULTS: { [key: string]: boolean } = {
'alarms.union_initialization': true,
'alarms.bool_value': true,
'eva.priority_only': false,
'eva.tainted_only': false,
'eva.data_tainted_only': false,
'eva.ctrl_tainted_only': false,
};
function filter(path: string) {
......@@ -203,9 +204,21 @@ function filterEva(p: Property) {
let b = true;
if (p.priority === false && filter('eva.priority_only'))
b = false;
if ((p.taint === 'not_tainted' || p.taint === 'not_applicable')
&& filter('eva.tainted_only'))
b = false;
switch (p.taint) {
case 'not_tainted':
case 'not_applicable':
if (filter('eva.data_tainted_only') || filter('eva.ctrl_tainted_only'))
b = false;
break;
case 'data_tainted':
if (filter('eva.ctrl_tainted_only'))
b = false;
break;
case 'control_tainted':
if (filter('eva.data_tainted_only'))
b = false;
break;
}
return b;
}
......@@ -251,8 +264,10 @@ const renderTaint: Renderer<any> =
let color = 'black';
switch (taint.name) {
case 'not_tainted': id = 'DROP.EMPTY'; color = '#00B900'; break;
case 'tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
case 'data_tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
case 'control_tainted': id = 'DROP.FILLED'; color = '#73BBBB'; break;
case 'error': id = 'HELP'; break;
case 'not_applicable': id = 'MINUS'; break;
default:
}
return (id ? <Icon id={id} fill={color} title={taint.descr} /> : null);
......@@ -288,6 +303,16 @@ const byStatus =
'considered_valid',
);
const byTaint =
Compare.byRank(
'data_tainted',
'control_tainted',
'not_tainted',
'error',
'not_applicable',
'not_computed',
);
const byProperty: Compare.ByFields<Property> = {
status: byStatus,
fct: Compare.defined(Compare.alpha),
......@@ -299,7 +324,7 @@ const byProperty: Compare.ByFields<Property> = {
key: Compare.string,
kinstr: Compare.structural,
priority: Compare.structural,
taint: Compare.structural,
taint: byTaint,
};
const byDir = Compare.byFields<SourceLoc>({ dir: Compare.alpha });
......@@ -444,9 +469,14 @@ function PropertyFilter() {
title="Show only high-priority properties for the Eva analysis"
/>
<CheckField
label="Tainted only"
path="eva.tainted_only"
title="Show only tainted properties according to the Eva taint domain"
label="Data-tainted only"
path="eva.data_tainted_only"
title="Show only data-tainted properties according to the Eva taint domain"
/>
<CheckField
label="Control-tainted only"
path="eva.ctrl_tainted_only"
title="Show only control-tainted properties according to the Eva taint domain"
/>
</Section>
</Scroll>
......@@ -576,11 +606,15 @@ export default function RenderProperties() {
const model = React.useMemo(() => new PropertyModel(), []);
const kernelData = States.useSyncArray(Properties.status).getArray();
const evaData = States.useSyncArray(Eva.properties).getArray();
useEffect(() => {
model.removeAllData();
const data = new Array(kernelData.length);
for (let i = 0; i < kernelData.length; i++) {
data[i] = { ...kernelData[i], ...evaData[i] };
const kernel = kernelData[i];
const { key } = kernel;
const eva = evaData.find((elt) => elt.key === key);
data[i] = { ...kernel, ...eva };
}
model.updateData(data);
model.reload();
......
ivette/src/frama-c/kernel/Status.tsx 0 → 100644
View file @ 9b464ff0
/* ************************************************************************ */
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2021 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/* ************************************************************************ */
/* --------------------------------------------------------------------------*/
/* --- Frama-C Selection History ---*/
/* --------------------------------------------------------------------------*/
import React from 'react';
import { Code } from 'dome/controls/labels';
import { LED, IconButton } from 'dome/controls/buttons';
import { Icon } from 'dome/controls/icons';
import * as Toolbars from 'dome/frame/toolbars';
import { GlobalState, useGlobalState } from 'dome/data/states';
export type kind =
'none' | 'info' | 'warning' | 'error' | 'success' | 'progress';
export interface Message {
kind: kind;
text: string;
title?: string;
}
const emptyMessage: Message = { text: '', kind: 'none' };
const GlobalMessage = new GlobalState(emptyMessage);
export function setMessage(message: Message) {
GlobalMessage.setValue(message);
}
export default function Message() {
const [message] = useGlobalState(GlobalMessage);
return (
<>
<Toolbars.Space />
{ message.kind === 'progress' && <LED status="active" blink /> }
{ message.kind === 'success' && <Icon id="CHECK" fill="green" /> }
{ message.kind === 'warning' && <Icon id="ATTENTION" /> }
{ message.kind === 'error' && <Icon id="CROSS" fill="red" /> }
{ message.kind === 'info' && <Icon id="CIRC.INFO" /> }
<Code label={message.text} title={message.title} />
<Toolbars.Space />
<IconButton
icon="CROSS"
onClick={() => setMessage(emptyMessage)}
visible={message !== emptyMessage}
title="Hide current message"
/>
<Toolbars.Space />
</>
);
}
/* --------------------------------------------------------------------------*/
ivette/src/frama-c/menu.ts 0 → 100644
View file @ 9b464ff0
/* ************************************************************************ */
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2021 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/* ************************************************************************ */
/* --------------------------------------------------------------------------*/
/* --- Frama-C MENU ---*/
/* --------------------------------------------------------------------------*/
import * as Dome from 'dome';
import * as Dialogs from 'dome/dialogs';
import * as Server from 'frama-c/server';
import * as Services from 'frama-c/api/kernel/services';
import * as Ast from 'frama-c/api/kernel/ast';
import * as Status from 'frama-c/kernel/Status';
import * as States from 'frama-c/states';
const cFilter = {
name: 'C source files',
extensions: ['c', 'i', 'h'],
};
const allFilter = {
name: 'all',
extensions: ['*'],
};
async function parseFiles(files: string[]): Promise<void> {
Status.setMessage({ text: 'Parsing source files…', kind: 'progress' });
await Server.send(Ast.setFiles, files);
await Server.send(Ast.compute, { });
Status.setMessage({ text: 'Source files parsed.', kind: 'success' });
return;
}
async function setFiles(): Promise<void> {
const files = await Dialogs.showOpenFiles({
title: 'Select C source files',
filters: [cFilter, allFilter],
});
if (files) {
await parseFiles(files);
States.resetSelection();
}
return;
}
async function addFiles(): Promise<void> {
const dialog = Dialogs.showOpenFiles({
title: 'Add C source files',
filters: [cFilter, allFilter],
});
const request = Server.send(Ast.getFiles, {});
const [oldFiles, newFiles] = await Promise.all([request, dialog]);
if (newFiles) {
const files = oldFiles ? oldFiles.concat(newFiles) : newFiles;
parseFiles(files);
}
return;
}
async function reparseFiles(): Promise<void> {
Status.setMessage({ text: 'Parsing source files…', kind: 'progress' });
const files = await Server.send(Ast.getFiles, {});
if (files) {
await Server.send(Ast.setFiles, []);
parseFiles(files);
}
return;
}
async function loadSession(): Promise<void> {
const file = await Dialogs.showOpenFile({ title: 'Load a saved session' });
Status.setMessage({ text: 'Loading session…', kind: 'progress' });
const error = await Server.send(Services.load, file);
States.resetSelection();
if (error) {
Status.setMessage({
text: 'Error when loading the session',
title: error,
kind: 'error',
});
await Dialogs.showMessageBox({
message: 'An error has occurred when loading the file',
details: `File: ${file}\nError: ${error}`,
kind: 'error',
buttons: [{ label: 'Cancel' }],
});
}
else
Status.setMessage({
text: 'Session successfully loaded.',
kind: 'success',
});
return;
}
async function saveSession(): Promise<void> {
const title = 'Save the current session';
const file = await Dialogs.showSaveFile({ title });
Status.setMessage({ text: 'Saving session…', kind: 'progress' });
const error = await Server.send(Services.save, file);
if (error) {
Status.setMessage({
text: 'Error when saving the session',
title: error,
kind: 'error',
});
await Dialogs.showMessageBox({
message: 'An error has occurred when saving the session',
kind: 'error',
buttons: [{ label: 'Cancel' }],
});
}
else
Status.setMessage({ text: 'Session successfully saved.', kind: 'success' });
return;
}
export function init() {
Dome.addMenuItem({
menu: 'File',
label: 'Set source files…',
id: 'file_set',
onClick: setFiles,
type: 'normal',
});
Dome.addMenuItem({
menu: 'File',
label: 'Add source files…',
id: 'file_add',
onClick: addFiles,
type: 'normal',
});
Dome.addMenuItem({
menu: 'File',
label: 'Reparse',
id: 'file_reparse',
onClick: reparseFiles,
type: 'normal',
});
Dome.addMenuItem({
menu: 'File',
id: 'file_separator',
type: 'separator',
});
Dome.addMenuItem({
menu: 'File',
label: 'Load session…',
id: 'file_load',
onClick: loadSession,
type: 'normal',
});
Dome.addMenuItem({
menu: 'File',
label: 'Save session…',
id: 'file_save',
onClick: saveSession,
type: 'normal',
});
}
/* --------------------------------------------------------------------------*/