diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4574184317f1fda2f69a2546368a9d5df11c9630..3394befbc709bec2d77dbc1603508d8c0e8f786e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -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
diff --git a/Makefile b/Makefile
index 8bd4ad0cf6397d041cdf7844e9b2450d3b6c0c64..7dd57fbf16620ad4344ab825ae8e30793e42e470 100644
--- a/Makefile
+++ b/Makefile
@@ -829,7 +829,7 @@ PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
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.
@@ -912,6 +912,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
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
@@ -1503,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::
diff --git a/doc/code/docgen.ml b/doc/code/docgen.ml
index 914a292268b83bffbb9b1ce5956e7a25ea801140..6b2ea3937c04698721a6a37d962e93716763a8ba 100644
--- a/doc/code/docgen.ml
+++ b/doc/code/docgen.ml
@@ -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 ;
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 59e9fb34c5d2e4e2109c35715e024463d3cd40b3..67258fcf5c5904b29fbf2bc050108ba16dca68ab 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1214,6 +1214,8 @@ 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
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index 1ce6eb2e0370f03c2416ac242e27f60f6977ba72..64b119c98b4d1b4315d7031fdbd8e1a6d8eee987 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -43,10 +43,6 @@ export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Marker kind */
export enum markerKind {
- /** Variable */
- variable = 'variable',
- /** Function */
- function = 'function',
/** Expression */
expression = 'expression',
/** Lvalue */
@@ -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,10 +141,11 @@ 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: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
+ name: string, descr: string }>({
key: Compare.string,
kind: byMarkerKind,
+ var: byMarkerVar,
name: Compare.alpha,
descr: Compare.string,
});
diff --git a/ivette/api/plugins/eva/index.ts b/ivette/api/plugins/eva/general/index.ts
similarity index 92%
rename from ivette/api/plugins/eva/index.ts
rename to ivette/api/plugins/eva/general/index.ts
index 4b46b34354923641cd17852220a4a7ff037b790f..9f77331803e084829e2e0d6ac13847d0f4d7f625 100644
--- a/ivette/api/plugins/eva/index.ts
+++ b/ivette/api/plugins/eva/general/index.ts
@@ -3,7 +3,7 @@
/**
Eva General Services
@packageDocumentation
- @module api/plugins/eva
+ @module api/plugins/eva/general
*/
//@ts-ignore
@@ -21,7 +21,7 @@ const getCallers_internal: Server.GetRequest<
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
> = {
kind: Server.RqKind.GET,
- name: 'plugins.eva.getCallers',
+ name: 'plugins.eva.general.getCallers',
input: Json.jKey<'#fct'>('#fct'),
output: Json.jList(Json.jTry(
Json.jPair(
diff --git a/ivette/api/plugins/eva/values/index.ts b/ivette/api/plugins/eva/values/index.ts
new file mode 100644
index 0000000000000000000000000000000000000000..22375d253f9b2f0bac5f1242c8cfe80693973c0e
--- /dev/null
+++ b/ivette/api/plugins/eva/values/index.ts
@@ -0,0 +1,154 @@
+/* --- 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;
+
+/* ------------------------------------- */
diff --git a/ivette/package.json b/ivette/package.json
index 24fe83a28e67d63846249ebca1c2fee8199fb2b5..884a4f23f15556839aa6de27ce229d358f4f021a 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -34,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",
diff --git a/ivette/src/dome/src/main/dome.js b/ivette/src/dome/src/main/dome.js
index cd01363afb0b82961da1f77f1baed2b3865e5b7c..e6291c5e4f94505092119aea4872d1cd07500c02 100644
--- a/ivette/src/dome/src/main/dome.js
+++ b/ivette/src/dome/src/main/dome.js
@@ -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);
diff --git a/ivette/src/dome/src/misc/devtools.js b/ivette/src/dome/src/misc/devtools.js
index 222b66d9d3d159ba7703dbf7d822519abc0b5ab8..4c921aa6c9ed956aaa131813074cb4303c6af844 100644
--- a/ivette/src/dome/src/misc/devtools.js
+++ b/ivette/src/dome/src/misc/devtools.js
@@ -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();
}
diff --git a/ivette/src/dome/src/renderer/table/arrays.ts b/ivette/src/dome/src/renderer/table/arrays.ts
index 705ec7fd0d214947bfa69aca49718097b11a21a6..e506d8237fc7e5ff1fdd635a9b0b630e761c5161 100644
--- a/ivette/src/dome/src/renderer/table/arrays.ts
+++ b/ivette/src/dome/src/renderer/table/arrays.ts
@@ -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> {
@@ -460,7 +460,6 @@ export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
this.reload();
}
-
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/src/renderer/table/views.tsx b/ivette/src/dome/src/renderer/table/views.tsx
index 5e7888b7c89035af4b1b8de6cfa738f47a075fdd..3089b35483683f8efa470dc7e241091877333937 100644
--- a/ivette/src/dome/src/renderer/table/views.tsx
+++ b/ivette/src/dome/src/renderer/table/views.tsx
@@ -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.
+ Use constant callbacks whenever possible, or memoize them with
+ `React.useCallback()` hook.
+
@template Row - table row data of some table entries
@template Cell - type of cell data to render in this column
*/
@@ -104,14 +112,17 @@ export interface ColumnProps<Row, Cell> {
visible?: boolean | 'never' | 'always';
/**
Data getter for this column.
+ Shall be constant or protected by `React.useCallback`.
*/
getter?: (row: Row, dataKey: string) => Cell | undefined;
/**
Override table by-fields cell renderers.
+ Shall be constant or protected by `React.useCallback`.
*/
render?: Renderer<Cell>;
/**
Override table right-click callback.
+ Shall be constant or protected by `React.useCallback`.
*/
onContextMenu?: (row: Row, index: number, dataKey: string) => void;
}
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index f97145728dc4ddb26db0f447df3a9c93aecd843a..ebfcbe4595ad602b0786f1b65ec8395388e81edb 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -15,7 +15,7 @@ import { IconButton } from 'dome/controls/buttons';
import { Component, TitleBar } from 'frama-c/LabViews';
import { printFunction, markerInfo } from 'api/kernel/ast';
-import { getCallers } from 'api/plugins/eva';
+import { getCallers } from 'api/plugins/eva/general';
import 'codemirror/mode/clike/clike';
import 'codemirror/theme/ambiance.css';
@@ -123,7 +123,7 @@ const ASTview = () => {
const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2);
const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
- function onTextSelection(id: key<'#markerIndo'>) {
+ function onTextSelection(id: key<'#markerInfo'>) {
if (selection.current) {
const location = { ...selection.current, marker: id };
updateSelection({ location });
@@ -133,18 +133,8 @@ const ASTview = () => {
async function onContextMenu(id: key<'#markerInfo'>) {
const items = [];
const selectedMarkerInfo = markersInfo.find((e) => e.key === id);
- switch (selectedMarkerInfo?.kind) {
- case 'function': {
- items.push({
- label: `Go to definition of ${selectedMarkerInfo.name}`,
- onClick: () => {
- const location = { function: selectedMarkerInfo.name };
- updateSelection({ location });
- },
- });
- break;
- }
- case 'declaration': {
+ if (selectedMarkerInfo?.var === 'function') {
+ if (selectedMarkerInfo.kind === 'declaration') {
if (selectedMarkerInfo?.name) {
const locations = await functionCallers(selectedMarkerInfo.name);
const locationsByFunction = _.groupBy(locations, (e) => e.function);
@@ -162,10 +152,15 @@ const ASTview = () => {
});
});
}
- break;
+ } else {
+ items.push({
+ label: `Go to definition of ${selectedMarkerInfo.name}`,
+ onClick: () => {
+ const location = { function: selectedMarkerInfo.name };
+ updateSelection({ location });
+ },
+ });
}
- default:
- break;
}
if (items.length > 0)
Dome.popupMenu(items);
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index 3c1e996f35f3d00319d6cb47849cd5968c93d9b5..cf01222181acde5a5daef680ecb593f020745107 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -22,6 +22,7 @@ import ASTinfo from './ASTinfo';
import Globals from './Globals';
import Properties from './Properties';
import Locations from './Locations';
+import Values from './Values';
// --------------------------------------------------------------------------
// --- Selection Controls
@@ -103,6 +104,7 @@ export default (() => {
<ASTinfo />
<Locations />
<Dive />
+ <Values />
</Group>
</LabView>
</Splitter>
diff --git a/ivette/src/renderer/Values.tsx b/ivette/src/renderer/Values.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..652f48fc1072c0a0ea7186293fdcaec0504e00c5
--- /dev/null
+++ b/ivette/src/renderer/Values.tsx
@@ -0,0 +1,141 @@
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import * as States from 'frama-c/states';
+import * as Json from 'dome/data/json';
+import * as Eva from 'api/plugins/eva/values';
+import * as Ast from 'api/kernel/ast';
+import * as Compare from 'dome/data/compare';
+
+import { Table, Column } from 'dome/table/views';
+import { ArrayModel } from 'dome/table/arrays';
+import { Component } from 'frama-c/LabViews';
+import { Icon } from 'dome/controls/icons';
+import { Label } from 'dome/controls/labels';
+
+// --------------------------------------------------------------------------
+// --- Columns
+// --------------------------------------------------------------------------
+
+const CallstackRenderer = (
+ (cs: Eva.callstack) => <Label label={cs.short} title={cs.full} />
+);
+
+const ColumnCallstack = () => Column({
+ id: 'callstack',
+ label: 'Callstack',
+ title: 'Context of the evaluation',
+ align: 'left',
+ width: 150,
+ render: CallstackRenderer,
+});
+
+const AlarmRenderer = (
+ (alarm: boolean) => <>{alarm && <Icon id="ATTENTION" />}</>
+);
+
+const ColumnAlarm = (props: { visible: boolean }) => Column({
+ id: 'alarm',
+ label: 'Alarm',
+ title: 'Did the evaluation emit an alarm?',
+ align: 'center',
+ width: 26,
+ fixed: true,
+ icon: 'WARNING',
+ visible: props.visible,
+ render: AlarmRenderer,
+});
+
+const byValues: Compare.ByFields<Eva.valuesData> =
+ { callstack: Compare.defined(Compare.byFields({ full: Compare.string })) };
+
+class ValuesModel extends ArrayModel<Json.key<'#values'>, Eva.valuesData> {
+ constructor() {
+ super();
+ this.setOrderingByFields(byValues);
+ }
+}
+
+// --------------------------------------------------------------------------
+// --- Values Panel
+// --------------------------------------------------------------------------
+
+const Values = () => {
+
+ const model = React.useMemo(() => new ValuesModel(), []);
+ const evaValues = States.useSyncArray(Eva.values).getArray();
+ const selectMarker = States.useSelection()[0]?.current?.marker;
+ const markerInfo = States.useSyncArray(Ast.markerInfo).getArray();
+ const [name, setName] = React.useState<string | undefined>(undefined);
+
+ States.useRequest(Eva.getValues, selectMarker);
+
+ React.useEffect(() => {
+ model.removeAllData();
+ if (selectMarker && evaValues) {
+ const selectMarkerInfo = markerInfo.find((e) => e.key === selectMarker);
+ if (selectMarkerInfo && selectMarkerInfo.var !== 'function') {
+ switch (selectMarkerInfo.kind) {
+ case 'expression':
+ case 'lvalue':
+ evaValues.forEach((i) => model.setData(i.key, i));
+ setName(selectMarkerInfo.descr);
+ break;
+ case 'declaration':
+ evaValues.forEach((i) => model.setData(i.key, i));
+ setName(selectMarkerInfo.name);
+ break;
+ default:
+ setName(undefined);
+ }
+ }
+ } else {
+ setName(undefined);
+ }
+ model.reload();
+ }, [evaValues, selectMarker, markerInfo, model]);
+
+ // Component
+ return (
+ <>
+ <Table model={model}>
+ <ColumnCallstack />
+ <Column
+ id="value_before"
+ visible={!!name}
+ label={name && `${name} (before)`}
+ title="Values inferred by Eva just before the selected point"
+ disableSort
+ width={300}
+ />
+ <ColumnAlarm visible={!!name} />
+ <Column
+ id="value_after"
+ visible={!!name}
+ label={name && `${name} (after)`}
+ title="Values inferred by Eva just after the selected point"
+ disableSort
+ width={300}
+ />
+ </Table>
+ </>
+ );
+};
+
+// --------------------------------------------------------------------------
+// --- Export Component
+// --------------------------------------------------------------------------
+
+export default () => (
+ <Component
+ id="frama-c.values"
+ label="Eva Values"
+ title="Values inferred by the Eva analysis"
+ >
+ <Values />
+ </Component>
+);
+
+// --------------------------------------------------------------------------
diff --git a/ivette/tests/eva-2.i b/ivette/tests/eva-2.i
new file mode 100644
index 0000000000000000000000000000000000000000..8b0998c24954c340558942ef8f4bf7e1c66205da
--- /dev/null
+++ b/ivette/tests/eva-2.i
@@ -0,0 +1,20 @@
+volatile int nondet;
+
+void fun () {
+ int x = nondet;
+ x = -x;
+}
+
+void yet_another () {
+ int x = nondet;
+ fun ();
+ int y = 100 / x;
+}
+
+void main () {
+ fun ();
+ /*@ assert boh: 1 == 1; */
+ yet_another ();
+ int i = 0;
+ /*@ assert user: i == 0; */
+}
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index 50e706f1a7a5573f1477b519262c98cda997649b..f3c5b7485450b40955f0664e50ae5ab6c6a7b421 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -3445,6 +3445,15 @@ electron-devtools-installer@^2.2.4:
rimraf "^2.5.2"
semver "^5.3.0"
+electron-devtools-installer@^3.0.0:
+ version "3.1.1"
+ resolved "https://registry.yarnpkg.com/electron-devtools-installer/-/electron-devtools-installer-3.1.1.tgz#7b56c8c86475c5e4e10de6917d150c53c9ceb55e"
+ integrity sha512-g2D4J6APbpsiIcnLkFMyKZ6bOpEJ0Ltcc2m66F7oKUymyGAt628OWeU9nRZoh1cNmUs/a6Cls2UfOmsZtE496Q==
+ dependencies:
+ rimraf "^3.0.2"
+ semver "^7.2.1"
+ unzip-crx-3 "^0.2.0"
+
electron-publish@22.4.1:
version "22.4.1"
resolved "https://registry.yarnpkg.com/electron-publish/-/electron-publish-22.4.1.tgz#a7fcf166786f7d5957f19a70ee8389f219769ba5"
@@ -4933,6 +4942,11 @@ ignore@^4.0.6:
resolved "https://registry.yarnpkg.com/ignore/-/ignore-4.0.6.tgz#750e3db5862087b4737ebac8207ffd1ef27b25fc"
integrity sha512-cyFDKrqc/YdcWFniJhzI42+AzS+gNwmUzOSFcRCQYwySuBBBy/KjuxWLZ/FHEH6Moq1NizMOBWyTcv8O4OZIMg==
+immediate@~3.0.5:
+ version "3.0.6"
+ resolved "https://registry.yarnpkg.com/immediate/-/immediate-3.0.6.tgz#9db1dbd0faf8de6fbe0f5dd5e56bb606280de69b"
+ integrity sha1-nbHb0Pr43m++D13V5Wu2BigN5ps=
+
immutable@^4.0.0-rc.12:
version "4.0.0-rc.12"
resolved "https://registry.yarnpkg.com/immutable/-/immutable-4.0.0-rc.12.tgz#ca59a7e4c19ae8d9bf74a97bdf0f6e2f2a5d0217"
@@ -5513,6 +5527,16 @@ jsx-ast-utils@^2.4.1:
array-includes "^3.1.1"
object.assign "^4.1.0"
+jszip@^3.1.0:
+ version "3.5.0"
+ resolved "https://registry.yarnpkg.com/jszip/-/jszip-3.5.0.tgz#b4fd1f368245346658e781fec9675802489e15f6"
+ integrity sha512-WRtu7TPCmYePR1nazfrtuF216cIVon/3GWOvHS9QR5bIwSbnxtdpma6un3jyGGNhHsKCSzn5Ypk+EkDRvTGiFA==
+ dependencies:
+ lie "~3.3.0"
+ pako "~1.0.2"
+ readable-stream "~2.3.6"
+ set-immediate-shim "~1.0.1"
+
keyv@^3.0.0:
version "3.1.0"
resolved "https://registry.yarnpkg.com/keyv/-/keyv-3.1.0.tgz#ecc228486f69991e49e9476485a5be1e8fc5c4d9"
@@ -5617,6 +5641,13 @@ levn@^0.3.0, levn@~0.3.0:
prelude-ls "~1.1.2"
type-check "~0.3.2"
+lie@~3.3.0:
+ version "3.3.0"
+ resolved "https://registry.yarnpkg.com/lie/-/lie-3.3.0.tgz#dcf82dee545f46074daf200c7c1c5a08e0f40f6a"
+ integrity sha512-UaiMJzeWRlEujzAuw5LokY1L5ecNQYZKfmyZ9L7wDHb/p5etKaxXhohBcrw0EYby+G/NA52vRSN4N39dxHAIwQ==
+ dependencies:
+ immediate "~3.0.5"
+
linkify-it@^2.0.0:
version "2.2.0"
resolved "https://registry.yarnpkg.com/linkify-it/-/linkify-it-2.2.0.tgz#e3b54697e78bf915c70a38acd78fd09e0058b1cf"
@@ -6546,7 +6577,7 @@ package-json@^6.3.0:
registry-url "^5.0.0"
semver "^6.2.0"
-pako@~1.0.5:
+pako@~1.0.2, pako@~1.0.5:
version "1.0.11"
resolved "https://registry.yarnpkg.com/pako/-/pako-1.0.11.tgz#6c9599d340d54dfd3946380252a35705a6b992bf"
integrity sha512-4hLB8Py4zZce5s4yd9XzopqwVv/yGNhV1Bl8NTmCq1763HeK2+EwVTv+leGeL13Dnh2wfbqowVPXCIO0z4taYw==
@@ -7724,6 +7755,13 @@ rimraf@^2.5.2, rimraf@^2.5.4, rimraf@^2.6.3, rimraf@^2.7.1:
dependencies:
glob "^7.1.3"
+rimraf@^3.0.2:
+ version "3.0.2"
+ resolved "https://registry.yarnpkg.com/rimraf/-/rimraf-3.0.2.tgz#f1a5402ba6220ad52cc1282bac1ae3aa49fd061a"
+ integrity sha512-JZkJMZkAGFFPP2YqXZXPbMlMBgsxzE8ILs4lMIX/2o0L9UBw9O/Y3o6wFw/i9YLapcUJWwqbi3kdxIPdC62TIA==
+ dependencies:
+ glob "^7.1.3"
+
ripemd160@^2.0.0, ripemd160@^2.0.1:
version "2.0.2"
resolved "https://registry.yarnpkg.com/ripemd160/-/ripemd160-2.0.2.tgz#a1c1a6f624751577ba5d07914cbc92850585890c"
@@ -7871,7 +7909,7 @@ semver@^6.0.0, semver@^6.1.2, semver@^6.2.0, semver@^6.3.0:
resolved "https://registry.yarnpkg.com/semver/-/semver-6.3.0.tgz#ee0a64c8af5e8ceea67687b133761e1becbd1d3d"
integrity sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==
-semver@^7.1.1:
+semver@^7.1.1, semver@^7.2.1:
version "7.3.2"
resolved "https://registry.yarnpkg.com/semver/-/semver-7.3.2.tgz#604962b052b81ed0786aae84389ffba70ffd3938"
integrity sha512-OrOb32TeeambH6UrhtShmF7CRDqhL6/5XpPNp2DuRH6+9QLw/orhp72j87v8Qa1ScDkvrrBNpZcDejAirJmfXQ==
@@ -7969,6 +8007,11 @@ set-blocking@^2.0.0:
resolved "https://registry.yarnpkg.com/set-blocking/-/set-blocking-2.0.0.tgz#045f9782d011ae9a6803ddd382b24392b3d890f7"
integrity sha1-BF+XgtARrppoA93TgrJDkrPYkPc=
+set-immediate-shim@~1.0.1:
+ version "1.0.1"
+ resolved "https://registry.yarnpkg.com/set-immediate-shim/-/set-immediate-shim-1.0.1.tgz#4b2b1b27eb808a9f8dcc481a58e5e56f599f3f61"
+ integrity sha1-SysbJ+uAip+NzEgaWOXlb1mfP2E=
+
set-value@^2.0.0, set-value@^2.0.1:
version "2.0.1"
resolved "https://registry.yarnpkg.com/set-value/-/set-value-2.0.1.tgz#a18d40530e6f07de4228c7defe4227af8cad005b"
@@ -8916,6 +8959,15 @@ unset-value@^1.0.0:
has-value "^0.3.1"
isobject "^3.0.0"
+unzip-crx-3@^0.2.0:
+ version "0.2.0"
+ resolved "https://registry.yarnpkg.com/unzip-crx-3/-/unzip-crx-3-0.2.0.tgz#d5324147b104a8aed9ae8639c95521f6f7cda292"
+ integrity sha512-0+JiUq/z7faJ6oifVB5nSwt589v1KCduqIJupNVDoWSXZtWDmjDGO3RAEOvwJ07w90aoXoP4enKsR7ecMrJtWQ==
+ dependencies:
+ jszip "^3.1.0"
+ mkdirp "^0.5.1"
+ yaku "^0.16.6"
+
upath@^1.1.1:
version "1.2.0"
resolved "https://registry.yarnpkg.com/upath/-/upath-1.2.0.tgz#8f66dbcd55a883acdae4408af8b035a5044c1894"
@@ -9374,6 +9426,11 @@ xtend@^4.0.0, xtend@~4.0.1:
resolved "https://registry.yarnpkg.com/y18n/-/y18n-4.0.0.tgz#95ef94f85ecc81d007c264e190a120f0a3c8566b"
integrity sha512-r9S/ZyXu/Xu9q1tYlpsLIsa3EeLXXk0VwlxqTcFRfg9EhMW+17kbt9G0NrgCmhGb5vT2hyhJZLfDGx+7+5Uj/w==
+yaku@^0.16.6:
+ version "0.16.7"
+ resolved "https://registry.yarnpkg.com/yaku/-/yaku-0.16.7.tgz#1d195c78aa9b5bf8479c895b9504fd4f0847984e"
+ integrity sha1-HRlceKqbW/hHnIlblQT9TwhHmE4=
+
yallist@^2.1.2:
version "2.1.2"
resolved "https://registry.yarnpkg.com/yallist/-/yallist-2.1.2.tgz#1c11f9218f076089a47dd512f93c6699a6a81d52"
diff --git a/nix/default.nix b/nix/default.nix
index 0121a1d19f4c87a04e15fa7da4876daede52c45c..b7804254b581310c919738b827b0dd22a9aa0ba7 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -1,5 +1,5 @@
# paramaterised derivation with dependencies injected (callPackage style)
-{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_05.ocaml", plugins ? { } }:
+{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_08.ocaml", plugins ? { } }:
let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
[ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages ++ opam2nix.build {
diff --git a/src/libraries/utils/utf8_logic.ml b/src/libraries/utils/utf8_logic.ml
index 1c2f3a6ddf068d4d24cec065a1d52cbad7f28301..92f594e89998bdcfad518673c529275de25a26e6 100644
--- a/src/libraries/utils/utf8_logic.ml
+++ b/src/libraries/utils/utf8_logic.ml
@@ -78,6 +78,9 @@ let integer = from_unichar 0x2124
let real = from_unichar 0x211D
let pi = from_unichar 0x3C0
+
+let infinity = from_unichar 0x221E
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/libraries/utils/utf8_logic.mli b/src/libraries/utils/utf8_logic.mli
index 449e20476bd3f55a53b09dd0cf143395d1ce5fad..7b6ea13a0da7362607108c23d890ca96d5f34184 100644
--- a/src/libraries/utils/utf8_logic.mli
+++ b/src/libraries/utils/utf8_logic.mli
@@ -49,6 +49,7 @@ val boolean: string
val integer: string
val real: string
val pi: string
+val infinity: string
(*
Local Variables:
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
deleted file mode 100644
index bb570ee92a885dcd365840665e9b00de514a5dab..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/arith.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
deleted file mode 100644
index 5e053cab3c744e96f02ea58ddbfac726d008ca3f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/array.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
deleted file mode 100644
index b42f8f987b3811fcd47315b45c397fc50c18ae68..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/at.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
deleted file mode 100644
index 63ab243f0f0ac90b52eb92796f458031b2f23bc9..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/at_on-purely-logic-variables.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
deleted file mode 100644
index 7a5cede891e1d7fc3175c8f0839ee423771fa84a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/bitwise.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
deleted file mode 100644
index 4e888498a7d29bd018398fa488d5cd0bcd5d6caf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/cast.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
deleted file mode 100644
index 8e470a21dcd8bc3a4fb7cbd653e6337840efddb5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/comparison.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
deleted file mode 100644
index 26a62cddaa2b4afdf33d1692dae5a3a79c99e62c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/functions.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
deleted file mode 100644
index 455ec56a835fd3d1536d3d10137cf67286160091..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/functions_rec.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
deleted file mode 100644
index 1b7f30270118bd782618efb4910af0ce98954bd0..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/integer_constant.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
deleted file mode 100644
index 803e26e12bb488545504f8066fe36c9f59a6de14..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/let.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
deleted file mode 100644
index 7e06012b6641a71b7d86732ac93f9801f42f1f5a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/longlong.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
deleted file mode 100644
index 58a67ef052fb929bfd6e270717f18174ad1403fe..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/not.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
deleted file mode 100644
index 912f940b8d7f93255e66171733e59b74f0fb30ce..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/arith/quantif.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
deleted file mode 100644
index 590199db8f04040ab84e966d5307b0dfc39f2ec5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing tests/arith/rationals.c (with preprocessing)
-[kernel:parser:decimal-float] tests/arith/rationals.c:19: Warning:
- Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/src/plugins/e-acsl/tests/bts/bts2252.c b/src/plugins/e-acsl/tests/bts/bts2252.c
index c52b56d04f0cd46500998328172f2f3c9d3c43a3..7bd739ccc4fe5826554b48a894bb58c5c1264992 100644
--- a/src/plugins/e-acsl/tests/bts/bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/bts2252.c
@@ -3,6 +3,7 @@
*/
#include <stdlib.h>
+#include <string.h>
int main() {
char* srcbuf = "Test Code";
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
index 9516b93607c4dc48622167d15db9d2a662cdf286..c0d14a505d07b9519cd7815386d12346a4c15e42 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
@@ -1,6 +1,25 @@
-[kernel:typing:implicit-function-declaration] tests/bts/bts2252.c:22: Warning:
- Calling undeclared function strncpy. Old style K&R code?
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `strncpy':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning:
+ E-ACSL construct `logic functions performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/bts/bts2252.c:17: Warning:
+[eva:alarm] tests/bts/bts2252.c:18: Warning:
out of bounds read. assert \valid_read(srcbuf + i);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
index 4ee6b66b44b57196aa0861c7e89c5fcd16e2ea9f..989bcb1766bd17886c7cc66d06c696124849a70f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
@@ -1,8 +1,149 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+#include "string.h"
char *__gen_e_acsl_literal_string;
-extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2);
+extern int __e_acsl_sound_verdict;
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes src_fits: strlen(src) < n;
+ ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+
+ behavior partial:
+ assumes src_too_long: n ≤ strlen(src);
+ ensures
+ equal_prefix:
+ memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * __restrict dest,
+ char const * __restrict src, size_t n);
+
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
+ requires room_nstring: \valid(dest + (0 .. n - 1));
+ requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
+ ensures result_ptr: \result ≡ \old(dest);
+ ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
+ assigns *(dest + (0 .. n - 1)), \result;
+ assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
+ assigns \result \from dest;
+
+ behavior complete:
+ assumes src_fits: strlen(src) < n;
+ ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
+
+ behavior partial:
+ assumes src_too_long: n ≤ strlen(src);
+ ensures
+ equal_prefix:
+ memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
+ */
+char *__gen_e_acsl_strncpy(char * __restrict dest,
+ char const * __restrict src, size_t n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ char *__gen_e_acsl_at_2;
+ char *__gen_e_acsl_at;
+ char *__retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
+ __gen_e_acsl__3,(void *)dest,
+ (void *)(& dest));
+ __e_acsl_assert(__gen_e_acsl_valid,"Precondition","strncpy",
+ "\\valid(dest + (0 .. n - 1))",
+ "FRAMAC_SHARE/libc/string.h",364);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_clear(__gen_e_acsl_n_2);
+ }
+ __gen_e_acsl_at_2 = dest;
+ __gen_e_acsl_at = dest;
+ __retres = strncpy(dest,src,n);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ unsigned long __gen_e_acsl__6;
+ int __gen_e_acsl_initialized;
+ __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","strncpy",
+ "\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",
+ 369);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set_si(__gen_e_acsl__5,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
+ 1 * 0),
+ __gen_e_acsl__6);
+ __e_acsl_assert(__gen_e_acsl_initialized,"Postcondition","strncpy",
+ "\\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
+ "FRAMAC_SHARE/libc/string.h",370);
+ __e_acsl_delete_block((void *)(& dest));
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_at_3);
+ return __retres;
+ }
+}
void __e_acsl_globals_init(void)
{
@@ -29,6 +170,8 @@ int main(void)
__e_acsl_full_init((void *)(& srcbuf));
int loc = 1;
char *destbuf = malloc((unsigned long)10 * sizeof(char));
+ __e_acsl_store_block((void *)(& destbuf),(size_t)8);
+ __e_acsl_full_init((void *)(& destbuf));
char ch = (char)'o';
if (destbuf != (char *)0) {
i = -1;
@@ -40,17 +183,19 @@ int main(void)
(void *)srcbuf,
(void *)(& srcbuf));
__e_acsl_assert(! __gen_e_acsl_valid_read,"Assertion","main",
- "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",16);
+ "!\\valid_read(srcbuf + i)","tests/bts/bts2252.c",17);
}
/*@ assert ¬\valid_read(srcbuf + i); */ ;
/*@ assert Eva: mem_access: \valid_read(srcbuf + i); */
if ((int)*(srcbuf + i) == (int)ch) loc = i;
i ++;
}
- strncpy(destbuf + loc,srcbuf + loc,1);
+ __gen_e_acsl_strncpy(destbuf + loc,(char const *)(srcbuf + loc),
+ (unsigned long)1);
free((void *)destbuf);
}
__retres = 0;
+ __e_acsl_delete_block((void *)(& destbuf));
__e_acsl_delete_block((void *)(& srcbuf));
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
deleted file mode 100644
index 19b0f068878a54abe6eb70c9b11771166b5fb060..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
deleted file mode 100644
index 0b966552605c312df3df587c9091b5dc19f54d58..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
-[kernel:parser:decimal-float] tests/bts/bts1307.i:17: Warning:
- Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
deleted file mode 100644
index e65b24385610fbf0e9291a09879dba416d9cfe8e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1324.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
deleted file mode 100644
index 99bd8d2ca4576581e7e3419c51e1178a1542723a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1326.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
deleted file mode 100644
index 93a1829d941669150d1f398004cdc422a7041bc6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1386_complex_flowgraph.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
deleted file mode 100644
index 3790aca8b1648cf45e6ab0e2e7266144f44af3ae..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1390.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
deleted file mode 100644
index cb9a17cb49257c74abf0d92dee4c7b8549ecd8b1..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1395.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1395.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
deleted file mode 100644
index ce219311963cd7c5a48aa4b07869a6c3d3c3389c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1398.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
deleted file mode 100644
index ea0b0b3e5e737e8e972eab0de467729f1b55189b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1399.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
deleted file mode 100644
index 1baa04b66fa314c4f33180491d831eea829a54fe..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1478.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
deleted file mode 100644
index d13cbafb98cd23d76f9ee695bc5c1e0e9158f7a4..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1700.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
deleted file mode 100644
index 2ed4f6df3461b85181897a66820a8073efcbefdf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1717.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
deleted file mode 100644
index 1c4ca2adb3d7fa12bc94ab4b2420f2c3a44603a7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1718.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1718.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
deleted file mode 100644
index 9751b7a8a5562c012c8a3a6bf06e091659203991..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1740.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1740.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
deleted file mode 100644
index f751f743c00132de9c3f257ce73c01deb8859b22..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts1837.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts1837.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
deleted file mode 100644
index 4c326f214a130cf42d1e795388b0c88f34f6caa7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2191.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2191.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
deleted file mode 100644
index 0122a7e4246394af3459e31969e6a0375ed0c61c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2192.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2192.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
deleted file mode 100644
index 4ef916d51cbfbbc01e1fb200ecaded57aa452471..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2231.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2231.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
deleted file mode 100644
index d21a94caccea54821812cfe937ca2446a230fb1c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2252.res.oracle
+++ /dev/null
@@ -1,3 +0,0 @@
-[kernel] Parsing tests/bts/bts2252.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/bts/bts2252.c:22: Warning:
- Calling undeclared function strncpy. Old style K&R code?
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
deleted file mode 100644
index 5c570a670fa5408249a025b31ade7311a391fdd2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2305.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2305.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
deleted file mode 100644
index 3bd50695afb1343ab68cf179bf22c6364bacf2f7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2386.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2386.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
deleted file mode 100644
index b09566f3aaf5b42219646778e6125c8a6b38df98..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/bts2406.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/bts2406.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
deleted file mode 100644
index 382eac9f065213428beb5ef5a6abbfb49a9b6194..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue-eacsl-105.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
deleted file mode 100644
index 2bd68e9f6dcd4681dfd4f5261d57da8bade8f5bc..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue-eacsl-91.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
deleted file mode 100644
index c2db810f8d36e24400c596766b288e2e333c8a3d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/bts/oracle_dev/issue69.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/bts/issue69.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle
deleted file mode 100644
index 7b03a368b78507b4138ef777b52cfbb963f7a0a8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/false.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle
deleted file mode 100644
index a26972504fc11c11cb0b4cef5dc3098de33f50f9..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/function_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle
deleted file mode 100644
index c88d3077a73d1a0859eb8b27a861254b12c7b37e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/ghost.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle
deleted file mode 100644
index bf1ef00efd5c9ce675530be79c853f6c7f5dc661..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/invariant.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle
deleted file mode 100644
index f970d17171ee2581d7d7f6be3d0fae73707be8d2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/labeled_stmt.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle
deleted file mode 100644
index ade1e36d99e66024de2eda4d09cfd72bc0377643..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/lazy.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle
deleted file mode 100644
index 84d2f0dd9410127e39335170feab7597534b1c14..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/loop.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle
deleted file mode 100644
index 79c41e376ff4d3e3a59dca0bf24993370504d131..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/nested_code_annot.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle
deleted file mode 100644
index b7000fff6c16bad99f08ac1e17b2f329a6292ead..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/result.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle
deleted file mode 100644
index 908fd31137c0504497dbb0b32676afc8e843b780..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/stmt_contract.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle
deleted file mode 100644
index 3b950952f857555f940f059c2ba5ff05d023283a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/true.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle
deleted file mode 100644
index bc4b2fca8240d19b78ea23ba7f785c8c25e90178..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/constructs/typedef.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
deleted file mode 100644
index 56f5b9ce5503a767bb5f388ef9430ee5c135e7a2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/examples/functions_contiki.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
deleted file mode 100644
index 9e5f8b0f3d2f462c08830f4fbec1f7cb555bde52..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/examples/linear_search.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
deleted file mode 100644
index 6209d961c8a49396a36a19193d6ba7a3fa8e4367..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
+++ /dev/null
@@ -1,362 +0,0 @@
-/* Generated by Frama-C */
-#include "signal.h"
-#include "stdio.h"
-#include "stdlib.h"
-#include "string.h"
-#include "sys/time.h"
-#include "sys/wait.h"
-#include "time.h"
-#include "unistd.h"
-#include "wchar.h"
-char *__gen_e_acsl_literal_string_6;
-char *__gen_e_acsl_literal_string_8;
-char *__gen_e_acsl_literal_string_5;
-char *__gen_e_acsl_literal_string_9;
-char *__gen_e_acsl_literal_string_7;
-char *__gen_e_acsl_literal_string;
-char *__gen_e_acsl_literal_string_2;
-char *__gen_e_acsl_literal_string_4;
-char *__gen_e_acsl_literal_string_3;
-void signal_eval(int status, int expect_signal, char const *at)
-{
- __e_acsl_store_block((void *)(& at),(size_t)8);
- __e_acsl_store_block((void *)(& expect_signal),(size_t)4);
- __e_acsl_store_block((void *)(& status),(size_t)4);
- int signalled = (int)((signed char)((status & 0x7f) + 1)) >> 1 > 0;
- __e_acsl_store_block((void *)(& signalled),(size_t)4);
- __e_acsl_full_init((void *)(& signalled));
- if (signalled) {
- if (expect_signal) __e_acsl_builtin_printf("s",
- __gen_e_acsl_literal_string,
- at);
- else goto _LAND_1;
- }
- else
- _LAND_1:
- if (! signalled) {
- if (! expect_signal) __e_acsl_builtin_printf("s",
- __gen_e_acsl_literal_string_2,
- at);
- else goto _LAND_0;
- }
- else
- _LAND_0:
- if (! signalled) {
- if (expect_signal) {
- __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_3,at);
- __gen_e_acsl_exit(1);
- }
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (signalled)
- if (! expect_signal) {
- __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_4,at);
- __gen_e_acsl_exit(2);
- }
- }
- __e_acsl_delete_block((void *)(& at));
- __e_acsl_delete_block((void *)(& expect_signal));
- __e_acsl_delete_block((void *)(& status));
- __e_acsl_delete_block((void *)(& signalled));
- return;
-}
-
-char const *valid_specifiers = "diouxfFeEgGaAcspn";
-void apply_specifier(char *format, int spec)
-{
- int n;
- char *tmp_1;
- __e_acsl_store_block((void *)(& tmp_1),(size_t)8);
- __e_acsl_store_block((void *)(& n),(size_t)4);
- __e_acsl_store_block((void *)(& spec),(size_t)4);
- __e_acsl_store_block((void *)(& format),(size_t)8);
- void *p = (void *)0;
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_full_init((void *)(& p));
- __e_acsl_full_init((void *)(& tmp_1));
- tmp_1 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_5,spec);
- if (tmp_1 != (char *)0) __e_acsl_builtin_printf("e",(char const *)format,
- 1.0);
- else {
- char *tmp_0;
- __e_acsl_store_block((void *)(& tmp_0),(size_t)8);
- __e_acsl_full_init((void *)(& tmp_0));
- tmp_0 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_6,spec);
- if (tmp_0 != (char *)0) __e_acsl_builtin_printf("D",(char const *)format,
- 1U);
- else {
- char *tmp;
- __e_acsl_store_block((void *)(& tmp),(size_t)8);
- __e_acsl_full_init((void *)(& tmp));
- tmp = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_7,spec);
- if (tmp != (char *)0) __e_acsl_builtin_printf("d",(char const *)format,
- 97);
- else
- if (spec == 's') __e_acsl_builtin_printf("s",(char const *)format,
- __gen_e_acsl_literal_string_8);
- else
- if (spec == 'n') __e_acsl_builtin_printf("i",(char const *)format,
- & n);
- else
- if (spec == 'p') __e_acsl_builtin_printf("p",
- (char const *)format,p);
- else __gen_e_acsl_abort();
- __e_acsl_delete_block((void *)(& tmp));
- }
- __e_acsl_delete_block((void *)(& tmp_0));
- }
- __e_acsl_delete_block((void *)(& spec));
- __e_acsl_delete_block((void *)(& format));
- __e_acsl_delete_block((void *)(& tmp_1));
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& n));
- return;
-}
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *);
-
-/* compiler builtin:
- void *__builtin_alloca(unsigned long); */
-void test_specifier_application(char const *allowed, char const *fmt,
- int only_negative, char *at)
-{
- size_t tmp;
- unsigned long __lengthof_format;
- __e_acsl_store_block((void *)(& __lengthof_format),(size_t)8);
- __e_acsl_store_block((void *)(& tmp),(size_t)8);
- __e_acsl_store_block((void *)(& at),(size_t)8);
- __e_acsl_store_block((void *)(& only_negative),(size_t)4);
- __e_acsl_store_block((void *)(& fmt),(size_t)8);
- __e_acsl_store_block((void *)(& allowed),(size_t)8);
- __e_acsl_full_init((void *)(& tmp));
- tmp = __gen_e_acsl_strlen(fmt);
- int len = (int)tmp;
- __e_acsl_store_block((void *)(& len),(size_t)4);
- __e_acsl_full_init((void *)(& len));
- /*@ assert
- alloca_bounds: 0 < sizeof(char) * (len + 1) ≤ 18446744073709551615;
- */
- {
- int __gen_e_acsl_and;
- if (0L < 1L * (len + 1L)) {
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_le;
- __gmpz_init_set_si(__gen_e_acsl_,1L * (len + 1L));
- __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gen_e_acsl_and = __gen_e_acsl_le <= 0;
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl__2);
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
- (char *)"test_specifier_application",
- (char *)"alloca_bounds: 0 < sizeof(char) * (len + 1) <= 18446744073709551615",
- 82);
- }
- __e_acsl_full_init((void *)(& __lengthof_format));
- __lengthof_format = (unsigned long)(len + 1);
- char *format = __builtin_alloca(sizeof(char) * __lengthof_format);
- __e_acsl_store_block((void *)format,sizeof(char) * __lengthof_format);
- __e_acsl_store_block((void *)(& format),(size_t)8);
- __e_acsl_full_init((void *)(& format));
- __gen_e_acsl_strcpy(format,fmt);
- {
- int i_0 = 0;
- __e_acsl_store_block((void *)(& i_0),(size_t)4);
- __e_acsl_full_init((void *)(& i_0));
- while (1) {
- size_t tmp_3;
- __e_acsl_store_block((void *)(& tmp_3),(size_t)8);
- __e_acsl_full_init((void *)(& tmp_3));
- tmp_3 = __gen_e_acsl_strlen(valid_specifiers);
- ;
- if (! ((size_t)i_0 < tmp_3)) {
- __e_acsl_delete_block((void *)(& tmp_3));
- break;
- }
- {
- char *tmp_2;
- __e_acsl_store_block((void *)(& tmp_2),(size_t)8);
- int c = (int)*(valid_specifiers + i_0);
- __e_acsl_store_block((void *)(& c),(size_t)4);
- __e_acsl_full_init((void *)(& c));
- __e_acsl_initialize((void *)(format + (len - 1)),sizeof(char));
- *(format + (len - 1)) = (char)c;
- __e_acsl_full_init((void *)(& tmp_2));
- tmp_2 = __gen_e_acsl_strchr(allowed,c);
- if (tmp_2) {
- if (! only_negative) {
- {
- pid_t pid = fork();
- __e_acsl_store_block((void *)(& pid),(size_t)4);
- __e_acsl_full_init((void *)(& pid));
- if (! pid) {
- apply_specifier(format,c);
- __gen_e_acsl_exit(0);
- }
- else {
- int process_status;
- __e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
- signal_eval(process_status,0,(char const *)at);
- __e_acsl_delete_block((void *)(& process_status));
- }
- __e_acsl_delete_block((void *)(& pid));
- }
- }
- }
- else {
- {
- pid_t pid_0 = fork();
- __e_acsl_store_block((void *)(& pid_0),(size_t)4);
- __e_acsl_full_init((void *)(& pid_0));
- if (! pid_0) {
- apply_specifier(format,c);
- __gen_e_acsl_exit(0);
- }
- else {
- int process_status_0;
- __e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
- signal_eval(process_status_0,1,(char const *)at);
- __e_acsl_delete_block((void *)(& process_status_0));
- }
- __e_acsl_delete_block((void *)(& pid_0));
- }
- }
- __e_acsl_delete_block((void *)(& tmp_2));
- __e_acsl_delete_block((void *)(& c));
- }
- __e_acsl_full_init((void *)(& i_0));
- i_0 ++;
- __e_acsl_delete_block((void *)(& tmp_3));
- }
- __e_acsl_delete_block((void *)(& i_0));
- }
- __e_acsl_delete_block((void *)format);
- __e_acsl_delete_block((void *)(& at));
- __e_acsl_delete_block((void *)(& only_negative));
- __e_acsl_delete_block((void *)(& fmt));
- __e_acsl_delete_block((void *)(& allowed));
- __e_acsl_delete_block((void *)(& __lengthof_format));
- __e_acsl_delete_block((void *)(& format));
- __e_acsl_delete_block((void *)(& tmp));
- __e_acsl_delete_block((void *)(& len));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- __gen_e_acsl_literal_string_6 = "uoxX";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("uoxX"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __gen_e_acsl_literal_string_8 = "foo";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof("foo"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_5 = "fFeEgGaA";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("fFeEgGaA"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_9 = "diouxfFeEgGaAcspn";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("diouxfFeEgGaAcspn"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_7 = "dic";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof("dic"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __gen_e_acsl_literal_string = "OK: expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("OK: expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
- __gen_e_acsl_literal_string_2 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_3 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strcpy),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strcpy));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strchr),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strchr));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strlen),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strlen));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
- __e_acsl_store_block((void *)(& test_specifier_application),(size_t)1);
- __e_acsl_full_init((void *)(& test_specifier_application));
- __e_acsl_store_block((void *)(& apply_specifier),(size_t)1);
- __e_acsl_full_init((void *)(& apply_specifier));
- __e_acsl_store_block((void *)(& valid_specifiers),(size_t)8);
- __e_acsl_full_init((void *)(& valid_specifiers));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& __fc_p_time_tm),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_time_tm));
- __e_acsl_store_block((void *)(& __fc_time_tm),(size_t)36);
- __e_acsl_full_init((void *)(& __fc_time_tm));
- __e_acsl_store_block((void *)(__fc_fds),(size_t)4096);
- __e_acsl_full_init((void *)(& __fc_fds));
- __e_acsl_store_block((void *)(& __fc_fds_state),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_fds_state));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)4096);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
- return;
-}
-
-int main(int argc, char const **argv)
-{
- int __retres;
- __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
- __e_acsl_globals_init();
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- __e_acsl_full_init((void *)(& __retres));
- __retres = 0;
- __e_acsl_delete_block((void *)(& argv));
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_delete_block((void *)(& test_specifier_application));
- __e_acsl_delete_block((void *)(& apply_specifier));
- __e_acsl_delete_block((void *)(& valid_specifiers));
- __e_acsl_delete_block((void *)(& signal_eval));
- __e_acsl_delete_block((void *)(& __fc_p_time_tm));
- __e_acsl_delete_block((void *)(& __fc_time_tm));
- __e_acsl_delete_block((void *)(__fc_fds));
- __e_acsl_delete_block((void *)(& __fc_fds_state));
- __e_acsl_delete_block((void *)(& __fc_time));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
- __e_acsl_delete_block((void *)(& __retres));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
deleted file mode 100644
index ebab565158d2b71aeb27fdb9077718b4788f1a36..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
+++ /dev/null
@@ -1,83 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __fc_fopen[0..511] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __e_acsl_internal_heap ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
- __fc_fds_state ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
- __fc_time_tm ∈ {0}
- __fc_p_time_tm ∈ {{ &__fc_time_tm }}
- valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
- __gen_e_acsl_literal_string ∈ {0}
- __gen_e_acsl_literal_string_2 ∈ {0}
- __gen_e_acsl_literal_string_3 ∈ {0}
- __gen_e_acsl_literal_string_4 ∈ {0}
- __gen_e_acsl_literal_string_5 ∈ {0}
- __gen_e_acsl_literal_string_6 ∈ {0}
- __gen_e_acsl_literal_string_7 ∈ {0}
- __gen_e_acsl_literal_string_8 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
deleted file mode 100644
index c3ff63dd0ce700cb2c8f81b5d3966c411b35d835..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
+++ /dev/null
@@ -1,84 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
- __e_acsl_init ∈ [--..--]
- __fc_fopen[0..511] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
- __e_acsl_internal_heap ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
- __fc_fds_state ∈ [--..--]
- __fc_fds[0..1023] ∈ {0}
- __fc_time_tm ∈ {0}
- __fc_p_time_tm ∈ {{ &__fc_time_tm }}
- valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
- __gen_e_acsl_literal_string ∈ {0}
- __gen_e_acsl_literal_string_2 ∈ {0}
- __gen_e_acsl_literal_string_3 ∈ {0}
- __gen_e_acsl_literal_string_4 ∈ {0}
- __gen_e_acsl_literal_string_5 ∈ {0}
- __gen_e_acsl_literal_string_6 ∈ {0}
- __gen_e_acsl_literal_string_7 ∈ {0}
- __gen_e_acsl_literal_string_8 ∈ {0}
- __gen_e_acsl_literal_string_9 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
deleted file mode 100644
index 78e0d254f7ce67cf02ea35288b8c99260bfd5144..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/format/fprintf.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
deleted file mode 100644
index 0de6311c2b2b21dbcb077c89367f32525dad330e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.res.oracle
+++ /dev/null
@@ -1,242 +0,0 @@
-[kernel] Parsing tests/format/printf.c (with preprocessing)
-[kernel:parser:decimal-float] tests/format/printf.c:89: Warning:
- Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[variadic] tests/format/printf.c:29: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:31: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:33: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:35: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:37: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:39: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:186: Warning:
- Not enough arguments: expected 5, given 4.
-[variadic] tests/format/printf.c:189: Warning:
- Too many arguments: expected 5, given 6. Superfluous arguments will be removed.
-[variadic] tests/format/printf.c:194: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
-[variadic] tests/format/printf.c:197: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:199: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:201: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:204: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:206: Warning: Unknown conversion specifier $.
-[variadic] tests/format/printf.c:226: Warning: Unknown conversion specifier l.
-[variadic] tests/format/printf.c:257: Warning:
- Incorrect type for argument 2. The argument will be cast from wint_t to intmax_t.
-[variadic] tests/format/printf.c:279: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:279: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:292: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:292: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:293: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:293: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to ptrdiff_t.
-[variadic] tests/format/printf.c:307: Warning: Unknown conversion specifier C.
-[variadic] tests/format/printf.c:308: Warning: Unknown conversion specifier S.
-[variadic] tests/format/printf.c:309: Warning: Unknown conversion specifier m.
-[variadic] tests/format/printf.c:315: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:315: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:316: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:316: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:317: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to int.
-[variadic] tests/format/printf.c:317: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to int.
-[variadic] tests/format/printf.c:318: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:318: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:328: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:328: Warning:
- Incorrect type for argument 2. The argument will be cast from int to size_t.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:334: Warning:
- Incorrect type for argument 2. The argument will be cast from long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:335: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:336: Warning:
- Incorrect type for argument 2. The argument will be cast from double to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:337: Warning:
- Incorrect type for argument 2. The argument will be cast from void * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:338: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to unsigned int.
-[variadic] tests/format/printf.c:355: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:355: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:356: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:356: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:357: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:357: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:359: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:359: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:360: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:360: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:361: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:361: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:363: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:363: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:364: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:364: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:365: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:365: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:367: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:367: Warning:
- Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/format/printf.c:368: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:368: Warning:
- Incorrect type for argument 2. The argument will be cast from int to double.
-[variadic] tests/format/printf.c:369: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:369: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to double.
-[variadic] tests/format/printf.c:372: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:372: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:374: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:374: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:375: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:375: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:376: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:376: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:378: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:378: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:379: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:379: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:380: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:380: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:382: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:382: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:383: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:383: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:384: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:384: Warning:
- Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/format/printf.c:386: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:386: Warning:
- Incorrect type for argument 2. The argument will be cast from int to long double.
-[variadic] tests/format/printf.c:387: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:387: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned long to long double.
-[variadic] tests/format/printf.c:393: Warning:
- Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/format/printf.c:394: Warning:
- Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/format/printf.c:395: Warning:
- Incorrect type for argument 2. The argument will be cast from double to int.
-[variadic] tests/format/printf.c:396: Warning:
- Incorrect type for argument 2. The argument will be cast from char * to int.
-[variadic] tests/format/printf.c:399: Warning:
- Incorrect type for argument 2. The argument will be cast from wint_t to intmax_t.
-[variadic] tests/format/printf.c:400: Warning:
- Incorrect type for argument 2. The argument will be cast from long to intmax_t.
-[variadic] tests/format/printf.c:409: Warning:
- Incorrect type for argument 2. The argument will be cast from int to char *.
-[variadic] tests/format/printf.c:464: Warning: Unknown conversion specifier '.
-[variadic] tests/format/printf.c:465: Warning:
- Flag 0 and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:466: Warning:
- Flag # and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:467: Warning:
- Flag ' ' and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:468: Warning:
- Flag + and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:469: Warning:
- Flag - and conversion specififer n are not compatibles.
-[variadic] tests/format/printf.c:470: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:471: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:472: Warning:
- Conversion specifier n does not expect a field width.
-[variadic] tests/format/printf.c:473: Warning:
- Conversion specifier n does not expect a precision.
-[variadic] tests/format/printf.c:476: Warning: Unknown conversion specifier '.
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
deleted file mode 100644
index 25dfbfef069fb1a71fc6f837a41f73a9eaa741c6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] using specification for function __e_acsl_initialized
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
deleted file mode 100644
index 25dfbfef069fb1a71fc6f837a41f73a9eaa741c6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_full_init
-[eva] using specification for function __e_acsl_initialized
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
deleted file mode 100644
index 3c2bad6f858c1f3248748229c2c4d76d1e06bc24..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
+++ /dev/null
@@ -1,82 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-void f(void)
-{
- int m;
- int *u;
- int *p;
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_store_block((void *)(& u),(size_t)8);
- __e_acsl_store_block((void *)(& m),(size_t)4);
- __e_acsl_full_init((void *)(& u));
- u = & m;
- __e_acsl_full_init((void *)(& p));
- p = u;
- __e_acsl_full_init((void *)(& m));
- m = 123;
- /*@ assert \initialized(p); */
- {
- int __gen_e_acsl_initialized;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
- __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
- (char *)"\\initialized(p)",10);
- }
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& u));
- __e_acsl_delete_block((void *)(& m));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __e_acsl_store_block((void *)(& f),(size_t)1);
- __e_acsl_full_init((void *)(& f));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_globals_init();
- __e_acsl_store_block((void *)(& __retres),(size_t)4);
- int x = 0;
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_full_init((void *)(& x));
- f();
- /*@ assert &x ≡ &x; */
- __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
- (char *)"&x == &x",16);
- __e_acsl_full_init((void *)(& __retres));
- __retres = 0;
- __e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
- __e_acsl_delete_block((void *)(& x));
- __e_acsl_delete_block((void *)(& __retres));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
deleted file mode 100644
index e53ffdec61d97f8b6372416756249550b782b0c3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_dev/addrOf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/full-mmodel/addrOf.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
deleted file mode 100644
index 252a6e43c513855c224c72e0dde01bdb64de093c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/arith.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/gmp-only/arith.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
deleted file mode 100644
index 6da7a17c6cbd609d91afb9420a61b43173acc0d6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/gmp-only/functions.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
deleted file mode 100644
index 431070f4cd2c23a54e002e700cf5e3b38de5ee9b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/addrOf.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/addrOf.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
deleted file mode 100644
index 76570c39a1839f0a05c5bb260d0478f294dfc87d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/alias.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/alias.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
deleted file mode 100644
index fe96bbc669e4065fbba7c900a12576e99798f01f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/base_addr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/base_addr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
deleted file mode 100644
index 9a8b757a2a064fbd610f0f38dcc832bf08a72d7e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/block_length.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/block_length.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
deleted file mode 100644
index 1b45bb1e9d4e0c412975f7f584a3f5f41190bf4f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/block_valid.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/block_valid.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
deleted file mode 100644
index bc2fc3b1336d2d4591be415e6e62bd22371b58ef..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/bypassed_var.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/bypassed_var.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
deleted file mode 100644
index 5809c1481efc478b1ae9179ce5afbc4336029d2b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/call.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/call.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
deleted file mode 100644
index fdb2f2e29f43957563faa4c8433c28ca551a71cd..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/compound_initializers.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/compound_initializers.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
deleted file mode 100644
index fb272a3c444be10982f0bbcd669f61999550fd56..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/constructor.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/constructor.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
deleted file mode 100644
index 106c9f6f4a7d36a2dced986139176c3d82abc26a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ctype_macros.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ctype_macros.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
deleted file mode 100644
index 453f7b598d1082df921d710e460f9ef10443dc4c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/decl_in_switch.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
deleted file mode 100644
index 165982a9f80f193617a7400635a8ac6442cbe4d7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/early_exit.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/early_exit.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
deleted file mode 100644
index 46094a4bbe226c576a8f95aee14ba27b5dfe70bf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/errno.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/errno.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
deleted file mode 100644
index b995f5e2ce349ed69711ca6030bd3cec2977eefd..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/freeable.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/freeable.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
deleted file mode 100644
index a076fcedfdb07a6e5dbd7554e48c110d6e0b1c0e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ghost_parameters.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
deleted file mode 100644
index 7f32099663f3add488d205bbd2f791e3e39a9b34..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/goto.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/goto.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
deleted file mode 100644
index c1d1529325342788673c66157df18cac73916533..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/hidden_malloc.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/hidden_malloc.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
deleted file mode 100644
index cd480f356c1cfca1517bff6ce0d69645e293b149..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
deleted file mode 100644
index bd7713301eb0c15cb7f54248e38c2a8cff586b8f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/init_function.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/init_function.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
deleted file mode 100644
index ec68705fe630ce62dd5a9b90bf9c2e039d45e2cb..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/initialized.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/initialized.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
deleted file mode 100644
index adabc66ff0a7eea47c5f7efafdcfb92cfa00f744..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/literal_string.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/literal_string.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
deleted file mode 100644
index b8fcb3470dbfcb8da050df6fa58387387fe69b0d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_goto.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/local_goto.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
deleted file mode 100644
index 460acb5fa597139c788b65a53882d3224f769e9d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/local_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
deleted file mode 100644
index 3743a714794545c5ef62287213e81fef3ffa0e4b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/local_var.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/local_var.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
deleted file mode 100644
index 36343fa0223fdbb51d13cac0fdb58f44c333a609..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/mainargs.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/mainargs.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
deleted file mode 100644
index 5b0314a0e239de01f82fde92d898059b25fa62f5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/memalign.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/memalign.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
deleted file mode 100644
index e6f6288929b8f85163da1241f838185526930c70..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/memsize.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/memsize.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
deleted file mode 100644
index 5a854c58c96a09f37219080a6c6cb8129f640230..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/null.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/null.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
deleted file mode 100644
index 9a18d848004451c94fd0b42a86ac95ecc99ddf61..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/offset.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/offset.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
deleted file mode 100644
index b56718829921013ea3f8f5fc73a2f19c8496796b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/other_constants.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/other_constants.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
deleted file mode 100644
index fcdcd5edd933540db9cfee10d831693420f086bf..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ptr.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
deleted file mode 100644
index 0b2ed5a9fc3516dbce7cc694cfdcaf45e0a8ed9a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ptr_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ptr_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
deleted file mode 100644
index 15a2210f13df3c32991408613e0b5ebb2091b79f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/ranges_in_builtins.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/ranges_in_builtins.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
deleted file mode 100644
index 45453873f24881a5367652c3ec53912d1685ea36..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/sizeof.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/sizeof.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
deleted file mode 100644
index b54acaedc8843427148c51bb6a1c7a8aebee30b7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/stdout.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/stdout.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
deleted file mode 100644
index c325574714e3a2da8ca342144e3088da774e8e2b..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/valid.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
deleted file mode 100644
index 767b46d932fa96248caba8ceeedf72cd7bd2356c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_alias.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/valid_alias.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
deleted file mode 100644
index 45dec02aac951fda0a503a2edf6a9011ef36bc1a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/valid_in_contract.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/valid_in_contract.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
deleted file mode 100644
index 296f399f3c8f267c128d2a151780ed432257574f..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/vector.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/vector.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
deleted file mode 100644
index cfa640a9f3642c03e9400b7012a5e580ef2f39e3..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle_dev/vla.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/memory/vla.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
deleted file mode 100644
index cfdeb9b03b56b0a1aa61b11bb839839e8951d589..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/builtin.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
deleted file mode 100644
index 455c37d94db4f36ab2df34f71c0d191461914e5c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-functions.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/e-acsl-functions.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
deleted file mode 100644
index 1ac7a10c191fa0fe8b4f4cb3890b06b28fb79ffa..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/special/e-acsl-instrument.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
deleted file mode 100644
index 3d6c26919131756db591eb531cb53f86d6071745..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-valid.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing share/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing share/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/e-acsl-valid.c (with preprocessing)
-[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
- function f: precondition \valid(y) got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
deleted file mode 100644
index 6c6987459b8f35382cf162b4814d67a73001e3e5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_addr-by-val.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
deleted file mode 100644
index 5416bcc06c1764cde8f9851606aef790b17ba138..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_args.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
deleted file mode 100644
index 08a70fa93d302403de8b8e4dc4bf959cbc698a19..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_array.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
deleted file mode 100644
index 0e80917c3d153c8b123d3b1802a11b12735d2a94..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_char.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
deleted file mode 100644
index 63872161277dfbf0ebb5b2ac19593e308ce6f94e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-[kernel] Parsing tests/temporal/t_darray.c (with preprocessing)
-[kernel] tests/temporal/t_darray.c:17: User Error:
- empty initializers only allowed for GCC/MSVC
- 15
- 16 double Vertices[3][4];
- 17 double Vertices2[3][4] = {};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 18
- 19 int main(int argc, const char **argv) {
-[kernel] User Error: stopping on file "tests/temporal/t_darray.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
deleted file mode 100644
index e636757d80cf08bc6ce76558588b6d19d49165e6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_dpointer.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
deleted file mode 100644
index 0d1fede17ec74668949362f9d42a73335964b48c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_fptr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
deleted file mode 100644
index 1928ecb96d0085d762db87a850e00544a8bda1b2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_fun_lib.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
deleted file mode 100644
index 0b50d95b38f263d8b94551a2bed66f9101f29029..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_fun_ptr.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
deleted file mode 100644
index 45c2b6834f7254653cfc96bd1f7cb4f8a53ea163..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_getenv.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
deleted file mode 100644
index 33a7eb427f45fb397dce6f04cdee3d8e4de325fe..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_global_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
deleted file mode 100644
index 4246bf9d0533032254f2253d85e4129696e99379..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_labels.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
deleted file mode 100644
index 6992e96210c075574977992126484a978ab93aa2..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_lit_string.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
deleted file mode 100644
index 195b9e93c1fee84731bf7f97cb54e18760ccd095..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_local_init.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
deleted file mode 100644
index 0186cd4c1e3d0e5ac636ade4077be6f342ebe920..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_malloc-asan.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
deleted file mode 100644
index 95c70361d689b4b4e6930818e275b4b729e56723..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_malloc.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
deleted file mode 100644
index a2ea974992bd8ead8978265b8bc93ada317e795d..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_memcpy.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
deleted file mode 100644
index 3d748d198fa047070be6e22c80b86c6689f40055..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_scope.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
deleted file mode 100644
index 364bbe79ba49ad4e18fd601d0a6ae50a7f616985..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_struct.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
deleted file mode 100644
index 2cc42109513b2955f1424545ef0d5d38224f8409..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/temporal/t_while.c (with preprocessing)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index b2d3c354e9c9396a29a5fe36b6ab6343bc6e377f..cf64d538e89a29899ab61df41bfb2cff5827e309 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -46,11 +46,12 @@ module MarkerKind = struct
let kinds = Enum.dictionary ()
- let kind name = Enum.tag ~name
- ~descr:(Md.plain (String.capitalize_ascii name)) kinds
+ let kind name =
+ Enum.tag
+ ~name
+ ~descr:(Md.plain (String.capitalize_ascii name))
+ kinds
- let var = kind "variable"
- let fct = kind "function"
let expr = kind "expression"
let lval = kind "lvalue"
let decl = kind "declaration"
@@ -59,24 +60,65 @@ module MarkerKind = struct
let term = kind "term"
let prop = kind "property"
- let () = Enum.set_lookup kinds
- begin
- let open Printer_tag in
- function
- | PStmt _ -> stmt
- | PStmtStart _ -> stmt
- | PVDecl _ -> decl
- | PLval (_, _, (Var vi, NoOffset)) ->
- if Cil.isFunctionType vi.vtype then fct else var
- | PLval _ -> lval
- | PExp _ -> expr
- | PTermLval _ -> term
- | PGlobal _ -> glob
- | PIP _ -> prop
- end
-
- let data = Request.dictionary ~package
- ~name:"markerKind" ~descr:(Md.plain "Marker kind") kinds
+ let () =
+ Enum.set_lookup
+ kinds
+ (fun localizable ->
+ let open Printer_tag in
+ match localizable with
+ | PStmt _ -> stmt
+ | PStmtStart _ -> stmt
+ | PVDecl _ -> decl
+ | PLval _ -> lval
+ | PExp _ -> expr
+ | PTermLval _ -> term
+ | PGlobal _ -> glob
+ | PIP _ -> prop)
+
+ let data =
+ Request.dictionary
+ ~package
+ ~name:"markerKind"
+ ~descr:(Md.plain "Marker kind")
+ kinds
+
+ include (val data : S with type t = Printer_tag.localizable)
+end
+
+module MarkerVar = struct
+
+ let vars = Enum.dictionary ()
+
+ let kind name =
+ Enum.tag
+ ~name
+ ~descr:(Md.plain (String.capitalize_ascii name))
+ vars
+
+ let none = kind "none"
+ let var = kind "variable"
+ let fct = kind "function"
+
+ let () =
+ Enum.set_lookup
+ vars
+ (fun localizable ->
+ let open Printer_tag in
+ match localizable with
+ | PLval (_, _, (Var vi, NoOffset))
+ | PVDecl (_, _, vi)
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) ->
+ if Cil.isFunctionType vi.vtype then fct else var
+ | PGlobal (GFun _ | GFunDecl _) -> fct
+ | PLval _ | PStmt _ | PStmtStart _
+ | PExp _ | PTermLval _ | PGlobal _ | PIP _ -> none)
+
+ let data =
+ Request.dictionary
+ ~package
+ ~name:"markerVar"
+ ~descr:(Md.plain "Marker variable")
+ vars
include (val data : S with type t = Printer_tag.localizable)
end
@@ -122,8 +164,18 @@ struct
let model = States.model () in
let () =
States.column
- ~name:"kind" ~descr:(Md.plain "Marker kind")
- ~data:(module MarkerKind) ~get:fst
+ ~name:"kind"
+ ~descr:(Md.plain "Marker kind")
+ ~data:(module MarkerKind)
+ ~get:fst
+ model
+ in
+ let () =
+ States.column
+ ~name:"var"
+ ~descr:(Md.plain "Marker variable")
+ ~data:(module MarkerVar)
+ ~get:fst
model
in
let () =
@@ -284,7 +336,14 @@ let () = Request.register ~package
~kind:`GET ~name:"printFunction"
~descr:(Md.plain "Print the AST of a function")
~input:(module Kf) ~output:(module Jtext)
- (fun kf -> Jbuffer.to_json Printer.pp_global (Kernel_function.get_global kf))
+ begin fun kf ->
+ let libc = Kernel.PrintLibc.get () in
+ if not libc then Kernel.PrintLibc.set true ;
+ let global = Kernel_function.get_global kf in
+ let ast = Jbuffer.to_json Printer.pp_global global in
+ if not libc then Kernel.PrintLibc.set false ;
+ ast
+ end
module Functions =
struct
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 5c30a704fbcb1fc5e59c9b7bbcf611adc6091460..09877676a76673136ad2b7a7f7f179ec8cadfbdd 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -22,8 +22,13 @@
open Server
-let package = Package.package ~plugin:"eva"
- ~title:"Eva General Services" ~readme:"eva.md" ()
+let package =
+ Package.package
+ ~plugin:"eva"
+ ~name:"general"
+ ~title:"Eva General Services"
+ ~readme:"eva.md"
+ ()
module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..85d2df413cded868f8088cdb2d72602a095ca4ac
--- /dev/null
+++ b/src/plugins/value/api/values_request.ml
@@ -0,0 +1,366 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Server
+open Data
+open Cil_types
+module Md = Markdown
+
+let package =
+ Package.package
+ ~plugin:"eva"
+ ~name:"values"
+ ~title:"Eva Values"
+ ~readme:"eva.md"
+ ()
+
+type value =
+ { value: string;
+ alarm: bool; }
+
+type evaluation =
+ | Unreachable
+ | Evaluation of value
+
+type after =
+ | Unchanged
+ | Reduced of evaluation
+
+type before_after =
+ { before: evaluation;
+ after_instr: after option;
+ after_then: after option;
+ after_else: after option; }
+
+type values =
+ { values: before_after;
+ callstack: (Value_util.callstack * before_after) list option; }
+
+let get_value = function
+ | Unreachable -> "Unreachable"
+ | Evaluation { value } -> value
+
+let get_alarm = function
+ | Unreachable -> false
+ | Evaluation { alarm } -> alarm
+
+let get_after_value =
+ Extlib.opt_map
+ (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
+
+module CallStackId =
+ Data.Index
+ (Value_types.Callstack.Map)
+ (struct
+ let name = "eva-callstack-id"
+ end)
+
+(* This pretty-printer drops the toplevel kf, which is always the function
+ in which we are pretty-printing the expression/term *)
+let pretty_callstack fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt callsite) :: q -> begin
+ let rec aux callsite = function
+ | (kf, callsite') :: q -> begin
+ Format.fprintf fmt "%a (%a)"
+ Kernel_function.pretty kf
+ Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite);
+ match callsite' with
+ | Kglobal -> ()
+ | Kstmt callsite' ->
+ Format.fprintf fmt " â†@ ";
+ aux callsite' q
+ end
+ | _ -> assert false
+ in
+ Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
+ aux callsite q;
+ Format.fprintf fmt "@]"
+ end
+ | _ -> assert false
+
+(* This pretty-printer prints only the lists of the functions, not
+ the locations. *)
+let pretty_callstack_short fmt cs =
+ match cs with
+ | [_, Kglobal] -> ()
+ | (_kf_cur, Kstmt _callsite) :: q ->
+ Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
+ Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
+ (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
+ | _ -> assert false
+
+module CallStack = struct
+ type record
+
+ let record: record Record.signature = Record.signature ()
+
+ let id = Record.field record ~name:"id"
+ ~descr:(Md.plain "Callstack id") (module Jint)
+ let short = Record.field record ~name:"short"
+ ~descr:(Md.plain "Short name for the callstack") (module Jstring)
+ let full = Record.field record ~name:"full"
+ ~descr:(Md.plain "Full name for the callstack") (module Jstring)
+
+ module R =
+ (val
+ (Record.publish
+ ~package
+ ~name:"callstack"
+ ~descr:(Md.plain "CallStack")
+ record) : Record.S with type r = record)
+
+ type t = Value_types.callstack option
+
+ let jtype = R.jtype
+
+ let pp_callstack ~short = function
+ | None -> if short then "all" else ""
+ | Some callstack ->
+ let pp_text =
+ if short
+ then Pretty_utils.to_string ~margin:50 pretty_callstack_short
+ else Pretty_utils.to_string pretty_callstack
+ in
+ (pp_text callstack)
+
+ let id_callstack = function
+ | None -> -1
+ | Some callstack -> CallStackId.get callstack
+
+ let to_json callstack =
+ R.default |>
+ R.set id (id_callstack callstack) |>
+ R.set short (pp_callstack ~short:true callstack) |>
+ R.set full (pp_callstack ~short:false callstack) |>
+ R.to_json
+
+ let key = function
+ | None -> "all"
+ | Some callstack -> string_of_int (CallStackId.get callstack)
+end
+
+
+let consolidated = ref None
+let table = Hashtbl.create 100
+
+let iter f =
+ if Hashtbl.length table > 1
+ then Extlib.may (fun values -> f (None, values)) !consolidated;
+ Hashtbl.iter (fun key data -> f (Some key, data)) table
+
+let array =
+ let model = States.model () in
+ let () =
+ States.column
+ ~name:"callstack"
+ ~descr:(Md.plain "CallStack")
+ ~data:(module CallStack)
+ ~get:fst
+ model
+ in
+ let () =
+ States.column
+ ~name:"value_before"
+ ~descr:(Md.plain "Value inferred just before the selected point")
+ ~data:(module Jstring)
+ ~get:(fun (_, e) -> get_value e.before)
+ model
+ in
+ let () =
+ States.column
+ ~name:"alarm"
+ ~descr:(Md.plain "Did the evaluation led to an alarm?")
+ ~data:(module Jbool)
+ ~get:(fun (_, e) -> get_alarm e.before)
+ model
+ in
+ let () =
+ States.column
+ ~name:"value_after"
+ ~descr:(Md.plain "Value inferred just after the selected point")
+ ~data:(module Joption(Jstring))
+ ~get:(fun (_, e) -> get_after_value e.after_instr)
+ model
+ in
+ States.register_array
+ ~package
+ ~name:"values"
+ ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
+ ~key:(fun (cs, _) -> CallStack.key cs)
+ ~iter
+ model
+
+let update_values values =
+ Hashtbl.clear table;
+ consolidated := Some values.values;
+ let () =
+ match values.callstack with
+ | None -> ()
+ | Some by_callstack ->
+ List.iter
+ (fun (callstack, before_after) ->
+ Hashtbl.add table callstack before_after)
+ by_callstack
+ in
+ States.reload array
+
+module type S = sig
+ val evaluate: kinstr -> exp -> values
+ val lvaluate: kinstr -> lval -> values
+end
+
+module Make (Eva: Analysis.S) : S = struct
+
+ let make_before eval before =
+ let before =
+ match before with
+ | `Bottom -> Unreachable
+ | `Value state -> Evaluation (eval state)
+ in
+ { before; after_instr = None; after_then = None; after_else = None; }
+
+ let make_callstack stmt eval =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ match before with
+ | (`Bottom | `Top) -> []
+ | `Value before ->
+ let aux callstack before acc =
+ let before_after = make_before eval (`Value before) in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make_before_after eval ~before ~after =
+ match before with
+ | `Bottom ->
+ { before = Unreachable;
+ after_instr = None;
+ after_then = None;
+ after_else = None; }
+ | `Value before ->
+ let before = eval before in
+ let after_instr =
+ match after with
+ | `Bottom -> Some (Reduced Unreachable)
+ | `Value after ->
+ let after = eval after in
+ if String.equal before.value after.value
+ then Some Unchanged
+ else Some (Reduced (Evaluation after))
+ in
+ { before = Evaluation before;
+ after_instr; after_then = None; after_else = None; }
+
+ let make_instr_callstack stmt eval =
+ let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
+ let after = Eva.get_stmt_state_by_callstack ~after:true stmt in
+ match before, after with
+ | (`Bottom | `Top), _
+ | _, (`Bottom | `Top) -> []
+ | `Value before, `Value after ->
+ let aux callstack before acc =
+ let before = `Value before in
+ let after =
+ try `Value (Value_types.Callstack.Hashtbl.find after callstack)
+ with Not_found -> `Bottom
+ in
+ let before_after = make_before_after eval ~before ~after in
+ (callstack, before_after) :: acc
+ in
+ Value_types.Callstack.Hashtbl.fold aux before []
+
+ let make eval kinstr =
+ let before = Eva.get_kinstr_state ~after:false kinstr in
+ let values, callstack =
+ match kinstr with
+ | Cil_types.Kglobal ->
+ make_before eval before, None
+ | Cil_types.Kstmt stmt ->
+ match stmt.skind with
+ | Instr _ ->
+ let after = Eva.get_kinstr_state ~after:true kinstr in
+ let values = make_before_after eval ~before ~after in
+ let callstack = make_instr_callstack stmt eval in
+ values, Some callstack
+ | _ ->
+ make_before eval before, Some (make_callstack stmt eval)
+ in
+ { values; callstack; }
+
+
+ let evaluate kinstr expr =
+ let eval state =
+ let value, alarms = Eva.eval_expr state expr in
+ let alarm = not (Alarmset.is_empty alarms) in
+ let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
+ { value = str; alarm }
+ in
+ make eval kinstr
+
+ let lvaluate kinstr lval =
+ let eval state =
+ let value, alarms = Eva.copy_lvalue state lval in
+ let alarm = not (Alarmset.is_empty alarms) in
+ let flagged_value = match value with
+ | `Bottom -> Eval.Flagged_Value.bottom
+ | `Value v -> v
+ in
+ let pretty = Eval.Flagged_Value.pretty Eva.Val.pretty in
+ let str = Format.asprintf "%a" pretty flagged_value in
+ { value = str; alarm }
+ in
+ make eval kinstr
+end
+
+
+let ref_request =
+ let module Analyzer = (val Analysis.current_analyzer ()) in
+ ref (module Make (Analyzer) : S)
+
+let hook (module Analyzer: Analysis.S) =
+ ref_request := (module Make (Analyzer) : S)
+
+let () = Analysis.register_hook hook
+
+
+let update tag =
+ let module Request = (val !ref_request) in
+ match tag with
+ | Printer_tag.PExp (_kf, kinstr, expr) ->
+ update_values (Request.evaluate kinstr expr)
+ | Printer_tag.PLval (_kf, kinstr, lval) ->
+ update_values (Request.lvaluate kinstr lval)
+ | PVDecl (_kf, kinstr, varinfo) ->
+ update_values (Request.lvaluate kinstr (Var varinfo, NoOffset))
+ | _ -> ()
+
+let () =
+ Server.Request.register
+ ~package
+ ~kind:`GET
+ ~name:"getValues"
+ ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
+ ~input:(module Kernel_ast.Marker)
+ ~output:(module Junit)
+ update
diff --git a/src/plugins/value/api/values_request.mli b/src/plugins/value/api/values_request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/value/api/values_request.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)