diff --git a/Changelog b/Changelog
index 6f9defaad92614bdc2408d1181e72354b045301d..e0472fb787ea02c7da8ce95cd6f2d5469bce6d4c 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,9 @@
Open Source Release <next-release>
##################################
+o Kernel [2022-05-03] Prototype of AST comparison between two versions
+ of the same program, via the new option -ast-diff.
+- Eva [2022-05-02] Fixes stack overflow errors on very large C functions.
- Eva [2022-04-25] Improve the multidim abstract domain: it is now
more precise and more robust, it is able to infer simple array
invariants on some loops without unrolling, and has a new option
@@ -34,6 +37,10 @@ o! Kernel [2022-02-23] Remove State_selection.Static (deprecated since
integer literal constants
* Kernel [2022-02-17] Reject programs using unsupported
vector_size attribute (fixes ##2573)
+o Eva [2022-02-15] New API to run the analysis and access its results,
+ intended to replace the old API in Db.Value. It is more precise
+ as it uses all available domains to evaluate values and locations.
+ See file Eva.mli for more details.
* Kernel [2022-02-08] Reject array whose size is too big with a proper
error message instead of a crash (fixes ##2590)
o! Kernel [2022-01-19] Removed obsolete AST nodes IndexPI and Info
diff --git a/Makefile b/Makefile
index af9f1b7bef88ce2ef2c4eff555bbd034677060af..6b917cf38ef061f06e297d00a414b01557f93c12 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,6 @@ PLUGIN_BIN_DOC_LIST:=
PLUGIN_DIST_EXTERNAL_LIST:=
PLUGIN_DIST_TESTS_LIST:=
PLUGIN_DISTRIBUTED_NAME_LIST:=
-MERLIN_PACKAGES:=
PLUGIN_HEADER_SPEC_LIST :=
PLUGIN_HEADER_DIRS_LIST :=
@@ -563,6 +562,7 @@ KERNEL_CMO=\
src/kernel_services/ast_data/annotations.cmo \
src/kernel_services/ast_printing/printer.cmo \
src/kernel_internals/typing/logic_builtin.cmo \
+ src/kernel_services/ast_queries/ast_diff.cmo \
src/kernel_services/ast_printing/cabs_debug.cmo \
src/kernel_internals/parsing/lexerhack.cmo \
src/kernel_internals/parsing/clexer.cmo \
diff --git a/Makefile.generating b/Makefile.generating
index 9787f4afc4e4e93a07912a8381cd4c6d09b835c7..993a0603c970f690112f6384ec975db08bdec200 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -161,12 +161,22 @@ endif
# Merlin #
.PHONY:merlin
-.merlin merlin: share/Makefile.config Makefile.generating
+
+# hack to account for the fact that merlin and ocamlfind treat
+# differently dependencies between ppx rewriting.
+PPX_DEPENDENCIES=ppx_deriving.eq ppx_import
+
#create Merlin file
+.merlin merlin: share/Makefile.config Makefile.generating
$(PRINT_MAKING) $@
echo "FLG -c $(FLAGS) $(FRAMAC_USER_MERLIN_FLAGS)" > .merlin
- for PKG in $(LIBRARY_NAMES); do echo PKG $$PKG >> .merlin; done
- for PKG in $(LIBRARY_NAMES_GUI); do echo PKG $$PKG >> .merlin; done
+ for PKG in $(filter-out $(PPX_DEPENDENCIES),$(LIBRARY_NAMES)); \
+ do echo PKG $$PKG >> .merlin; done
+ for PKG in $(filter-out $(PPX_DEPENDENCIES),$(LIBRARY_NAMES_GUI)); \
+ do echo PKG $$PKG >> .merlin; done
+ for PKG in \
+ $(filter $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI),$(PPX_DEPENDENCIES)); \
+ do echo PKG $$PKG >> .merlin; done
for PKG in $(MERLIN_PACKAGES); do echo PKG $$PKG >> .merlin; done
echo "B lib/plugins" >> .merlin
echo "B lib/plugins/gui" >> .merlin
diff --git a/bin/check-reference-configuration.sh b/bin/check-reference-configuration.sh
index 6557c2eca7defd285aebdb24afa512ccad39385e..e91365642881b711352f863c119deecc00de901e 100755
--- a/bin/check-reference-configuration.sh
+++ b/bin/check-reference-configuration.sh
@@ -7,6 +7,17 @@ if ! type "opam" > /dev/null; then
opam="NOT"
else
opam="$(opam --version)"
+ if [[ $opam =~ ^([0-9+]).([0-9+]) ]]; then
+ major="${BASH_REMATCH[1]}"
+ minor="${BASH_REMATCH[2]}"
+ if [[ "$major" -eq 2 && "$minor" -eq 0 ]]; then
+ echo "warning: opam > 2.1 expected, got $major.$minor."
+ echo " Suggested commands may not work properly."
+ fi
+ else
+ echo "warning: unknown opam version."
+ echo " Suggested commands may not work properly."
+ fi
fi
if ! type "ocaml" > /dev/null; then
@@ -63,7 +74,6 @@ echo "All packages checked."
if [ $has_any_diffs -ne 0 ]; then
echo "Useful commands:"
echo " opam switch create ${working_ocaml}"
- echo " opam install depext"
- echo " opam depext --install$all_packages"
+ echo " opam install$all_packages"
echo " rm -f ~/.why3.conf && why3 config detect"
fi
diff --git a/configure.in b/configure.in
index 14992096643bf50419d820e9eb81198625d24ca3..e98ef587598339a0405baf03cc58c93a361943e5 100644
--- a/configure.in
+++ b/configure.in
@@ -336,6 +336,17 @@ else
AC_MSG_RESULT(found $YOJSON)
fi
+# ppx_import
+############
+
+AC_MSG_CHECKING(for ppx_import)
+PPX_IMPORT=$($OCAMLFIND query ppx_import -format %v)
+if test -z "$PPX_IMPORT"; then
+ AC_MSG_ERROR(Cannot find ppx_import via ocamlfind)
+else
+ AC_MSG_RESULT(found $PPX_IMPORT)
+fi
+
#################################################
# Check for other (optional) tools/libraries #
#################################################
diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
index 64be01e60a9cfade46cece24845addf9449f848b..04d1c97261bf1c50ddebd680e3f9f7458ddffaca 100644
--- a/devel_tools/docker/Makefile
+++ b/devel_tools/docker/Makefile
@@ -96,10 +96,11 @@ conf-graphviz.0.1 \\\
mlgmpidl.1.2.12 \\\
ocamlfind.1.8.1 \\\
ocamlgraph.1.8.8 \\\
-ppx_deriving_yojson.3.5.2 \\\
-why3.1.4.0 \\\
+ppx_deriving_yojson.3.6.1 \\\
+ppx_import.1.9.0 \\\
+why3.1.5.0 \\\
yojson.1.7.0 \\\
-zarith.1.9.1 \\\
+zarith.1.10 \\\
zmq.5.1.3 \\\
conf-python-3.1.0.0 \\\
conf-time.1|' | \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 85a742841df0fe295e65d22132756dd7788da302..e34347acdd061e025cfff74a0507b0f5dfac4d46 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -594,6 +594,8 @@ src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL
src/kernel_services/ast_queries/README.md: .ignore
src/kernel_services/ast_queries/acsl_extension.ml: CEA_LGPL
src/kernel_services/ast_queries/acsl_extension.mli: CEA_LGPL
+src/kernel_services/ast_queries/ast_diff.ml: CEA_LGPL
+src/kernel_services/ast_queries/ast_diff.mli: CEA_LGPL
src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
src/kernel_services/ast_queries/cil.ml: CIL
diff --git a/ivette/INSTALL.md b/ivette/INSTALL.md
index 243b80ae3468ca91adbad0195c8e95b4ff03ac69..db3201e0c7c338f327ed8b9001bb608663a7a2ca 100644
--- a/ivette/INSTALL.md
+++ b/ivette/INSTALL.md
@@ -3,42 +3,93 @@
Required package to be installed:
- `yarn` for node pakage management;
- `pandoc` for generating the documentation;
-- `node` version 16.x (codename: gallium)
+- `node` version 16.x;
+
+We recommand to use node v16 as a workaroung against incompatible versions of
+SSL and Webpack packages. However, under Arch Linux, the standard node v17 is
+also known to work.
+
+## Linux
+
+```sh
+$ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.34.0/install.sh | bash
+$ nvm install 16
+$ nvm use 16
+$ npm install yarn
+```
+
+Under Arch you can simply rely on the `yarn` package and its `node` standard
+dependency:
+
+```sh
+$ pacman -S yarn
+```
+
+## macOS
+
+```sh
+$ brew install yarn
+$ brew install nvm # follow instructions
+$ nvm install 16
+$ nvm use 16
+```
# Installation
+You shall have configured `frama-c` before installing Ivette. Notice that, by
+default, the installed `ivette` command will look for an installed `frama-c`
+command to run the server.
+
From the `Frama-C` main directory, simply type:
```
+$ autoconf -f
+$ ./configure
$ make -C ivette dist
+$ [sudo] make -C ivette install
```
If this is the first time you compile `ivette`, this might take some time to download
all the necessary packages and Electron binaries from the web.
-Once finished, the Ivette application is available in `ivette/dist/<platform>` directory.
+The first `make` command builds a binary distribution of Ivette for your
+architecture in `ivette/dist/<arch>` ; the second `make` command installs it on
+your system accordingly.
+
+The installed command is `<prefix>/bin/ivette` which is actually just a wrapper
+to launch the Ivette application. The Ivette application itself is installed:
+
+- **Linux:** in `<prefix>/lib/ivette/*`
+- **macOS:** in `/Applications/Ivette.app`
-# Developer Install
+# Developer Setup
Ivette can be compiled and used with different modes:
+
- `make dev` builds and start the development version with live-code-editing enabled. It uses
local binaries of Electron framework. This is _not_ a full packaged
application.
+
- `make app` pre-builds the production application. It is not _yet_ packaged and still
uses the local Electron binaries.
+
- `make dist` packages the pre-built application into a new application for the host
- operating system.
+ operating system, see Installation section above.
+
+The development and production applications can be launched from the command
+line with `Frama-C/ivette/bin/ivette` wrapper. The generated `ivette` script
+will use the local `Frama-C/bin/frama-c` binary by default, although you can
+change this behaviour by using `ivette` command-line options.
-The development and production applications can be launched from the command line
-with `Frama-C/ivette/bin/frama-c-gui` binary.
-The generated `frama-c-gui` script will use the local `Frama-C/bin/frama-c` binary by default,
-although you can change the default settings by using the following options:
+The `ivette` application and its installed or local wrappers accept the
+following command line options:
```
-frama-c-gui [ivette options] [frama-c command line]
- --cwd <dir> change the working directory used by ivette & frama-c
- --command <bin> set the frama-c server to be launched
- --socket <socket> set the IPC socket name to be used for the frama-c server
+ivette [ivette options] [frama-c command line]
+ -R|--reload re-run the last command from history (other options are discarded)
+ -C|--working <dir> change the working directory used by ivette & frama-c
+ -B|--command <bin> set the frama-c server to be launched
+ --socket <socket> set the Linux socket name to be used for the frama-c server
```
See also the [CONTRIBUTING] guide for editor configuration if you want to hack in Ivette
diff --git a/ivette/Makefile b/ivette/Makefile
index f6a0cf4f1f4d5e4dcfe9ea8b8e2687a5aca5909a..2fdd3467f40a35bb3f38e68c34ab9e0390436648 100644
--- a/ivette/Makefile
+++ b/ivette/Makefile
@@ -25,7 +25,7 @@ APP=Ivette
DOME=./src/dome
DOME_ARGS=--command $$(dirname $$0)/../../bin/frama-c
DOME_DEV=-server-debug 1
-DOME_CLI=./bin/frama-c-gui
+DOME_CLI=./bin/ivette
DOME_API=./src/frama-c
DOME_CUSTOM_ENTRIES= yes
COPYRIGHT=CEA LIST / LSL
@@ -37,7 +37,7 @@ all: pkg lint app
app: dome-app
dev: dome-dev
-dist: dome-dist
+dist: dist-dir dome-dist
lint: dome-pkg dome-templ checkcase
@echo "[Ivette] running typechecker & linter"
@@ -148,3 +148,65 @@ $(NODEBIN)/%:
# --------------------------------------------------------------------------
include $(DOME)/template/makefile
# --------------------------------------------------------------------------
+
+# --------------------------------------------------------------------------
+# --- Ivette Installation
+# --------------------------------------------------------------------------
+
+sinclude ../share/Makefile.config
+
+dist-dir:
+ @echo "Cleaning dist"
+ @rm -fr dist
+
+IVETTE_DIST=$(wildcard dist/linux-unpacked dist/mac dist/mac-arm64)
+
+ifdef LIBDIR
+ifdef BINDIR
+ifeq ($(IVETTE_DIST),dist/linux-unpacked)
+
+install:
+ @echo "Installing Ivette (Linux)"
+ @rm -fr $(LIBDIR)/ivette
+ @rm -f $(BINDIR)/ivette
+ @mv $(IVETTE_DIST) $(LIBDIR)/ivette
+ @ln -s $(LIBDIR)/ivette/ivette $(BINDIR)/ivette
+
+else ifeq ($(IVETTE_DIST:-arm64=),dist/mac)
+
+install:
+ @echo "Installing Ivette (macOS)"
+ @rm -fr /Applications/Ivette.app
+ @mv $(IVETTE_DIST)/Ivette.app /Applications/
+ @rm -fr $(IVETTE_DIST)
+ @install ivette-macos.sh $(BINDIR)/ivette
+
+else
+
+install:
+ @echo "No distribution to install"
+ @echo "use 'make dist' and retry"
+ @exit 1
+
+endif
+endif
+endif
+
+# --------------------------------------------------------------------------
+# --- Ivette Un-Installation
+# --------------------------------------------------------------------------
+
+ifdef LIBDIR
+ifdef BINDIR
+
+uninstall:
+ @echo "Uninstall Ivette"
+ @rm -fr dist
+ @rm -fr /Applications/Ivette.app
+ @rm -fr $(LIBDIR)/ivette
+ @rm -f $(BINDIR)/ivette
+
+endif
+endif
+
+# --------------------------------------------------------------------------
diff --git a/ivette/electron-builder.json b/ivette/electron-builder.json
new file mode 100644
index 0000000000000000000000000000000000000000..8a9e8291fb56caa9a9b4b279dea6261fcf265645
--- /dev/null
+++ b/ivette/electron-builder.json
@@ -0,0 +1,4 @@
+{
+ productName: "Ivette",
+ mac: { icon: "ivette.icns" }
+}
diff --git a/ivette/ivette-macos.sh b/ivette/ivette-macos.sh
new file mode 100755
index 0000000000000000000000000000000000000000..8e11dedfccca2c9f3e64980f0ceb19444f8d3ffd
--- /dev/null
+++ b/ivette/ivette-macos.sh
@@ -0,0 +1,3 @@
+#!/bin/zsh
+
+exec open -na Ivette.app --args --cwd $PWD $*
diff --git a/ivette/ivette.icns b/ivette/ivette.icns
new file mode 100644
index 0000000000000000000000000000000000000000..6e8ec524ac725709613bb0ea80900ea759b21fc5
Binary files /dev/null and b/ivette/ivette.icns differ
diff --git a/ivette/src/dome/main/dome.ts b/ivette/src/dome/main/dome.ts
index e735470e986db9d7ffbadfe6580aeeba71978384..9ab3ca18f76f7f9c695166ab8ea33a3fe241f931 100644
--- a/ivette/src/dome/main/dome.ts
+++ b/ivette/src/dome/main/dome.ts
@@ -167,6 +167,7 @@ function obtainGlobalSettings() {
type Store = { [key: string]: unknown };
interface Handle {
+ primary: boolean; // Primary window
window: BrowserWindow; // Also prevents Gc
frame: Electron.Rectangle; // Window frame
devtools: boolean; // Developper tools visible
@@ -348,6 +349,7 @@ function lookupConfig(pwd = '.') {
// --------------------------------------------------------------------------
function createBrowserWindow(
+ primary: boolean,
config: BrowserWindowConstructorOptions,
argv?: string[],
wdir?: string,
@@ -387,6 +389,7 @@ function createBrowserWindow(
const wid = webContents.id;
const handle: Handle = {
+ primary,
window: theWindow,
config: configFile,
reloaded: false,
@@ -487,23 +490,31 @@ function createPrimaryWindow() {
applyThemeSettings(globals);
// Create Window
- createBrowserWindow({ title: appName }, argv, wdir);
+ createBrowserWindow(true, { title: appName }, argv, wdir);
}
let appCount = 1;
function createSecondaryWindow(
_event: Electron.Event,
- electronArgv: string[],
+ chromiumArgv: string[],
wdir: string,
) {
- const argv = stripElectronArgv(electronArgv);
- createBrowserWindow({ title: `${appName} #${++appCount}` }, argv, wdir);
+ const argStart = "--second-instance=";
+ let argString = chromiumArgv.find(a => a.startsWith(argStart));
+ if (argString) {
+ argString = argString.substring(argStart.length);
+ const electronArgv = JSON.parse(argString);
+ const argv = stripElectronArgv(electronArgv);
+ const title = `${appName} #${++appCount}`;
+ createBrowserWindow(false, { title }, argv, wdir);
+ }
}
function createDesktopWindow() {
const wdir = app.getPath('home');
- createBrowserWindow({ title: `${appName} #${++appCount}` }, [], wdir);
+ const title = `${appName} #${++appCount}`;
+ createBrowserWindow(false, { title }, [], wdir);
}
// --------------------------------------------------------------------------
@@ -535,7 +546,8 @@ let PreferenceWindow: BrowserWindow | undefined;
function showSettingsWindow() {
if (!PreferenceWindow)
- PreferenceWindow = createBrowserWindow({
+ PreferenceWindow = createBrowserWindow(
+ false, {
title: `${appName} Settings`,
width: 256,
height: 248,
@@ -582,6 +594,11 @@ ipcMain.on('dome.app.paths', (event) => {
/** Starts the main process. */
export function start() {
+ // Workaround to recover the original commandline of a second instance
+ // after chromium messes with the argument order.
+ // See https://github.com/electron/electron/issues/20322 for more details.
+ app.commandLine.appendSwitch("second-instance", JSON.stringify(process.argv));
+
// Ensures second instance triggers the main one
if (!app.requestSingleInstanceLock()) app.quit();
@@ -614,7 +631,7 @@ export function start() {
// --------------------------------------------------------------------------
/**
- Define a custom main window menu.
+ Define a custom main window menu.
*/
export function addMenu(label: string) {
Menubar.addMenu(label);
@@ -634,9 +651,21 @@ export function setMenuItem(spec: Menubar.CustomMenuItem) {
Menubar.setMenuItem(spec);
}
-ipcMain.on('dome.ipc.menu.addmenu', (_evt, label) => addMenu(label));
-ipcMain.on('dome.ipc.menu.addmenuitem', (_evt, spec) => addMenuItem(spec));
-ipcMain.on('dome.ipc.menu.setmenuitem', (_evt, spec) => setMenuItem(spec));
+function isPrimary(evt: IpcMainEvent): boolean {
+ const h = WindowHandles.get(evt.sender.id);
+ return h ? h.primary : false;
+}
+
+ipcMain.on('dome.ipc.menu.addmenu', (evt, label) =>
+ isPrimary(evt) && Menubar.addMenu(label)
+);
+ipcMain.on('dome.ipc.menu.addmenuitem', (evt, spec) =>
+ isPrimary(evt) && Menubar.addMenuItem(spec)
+);
+ipcMain.on('dome.ipc.menu.setmenuitem', (_evt, spec) =>
+ // Always update menu items
+ Menubar.setMenuItem(spec)
+);
// --------------------------------------------------------------------------
// --- Dialogs Management
diff --git a/ivette/src/dome/main/menubar.ts b/ivette/src/dome/main/menubar.ts
index 52f4212c96f0e09a6e8a85866acf4ac1b1e5b16e..417631484b83afa11b2f56767782084e7ddf15a6 100644
--- a/ivette/src/dome/main/menubar.ts
+++ b/ivette/src/dome/main/menubar.ts
@@ -273,12 +273,15 @@ const windowMenuItemsMacos: MenuSpec = windowMenuItemsLinux.concat([
// --- Help Menu Items
// --------------------------------------------------------------------------
+let learnMoreLink = '';
+ipcMain.handle('dome.ipc.updateLearnMore', (_, link) => {
+ if (typeof link === 'string') learnMoreLink = link;
+});
+
const helpMenuItems: MenuSpec = [
{
label: 'Learn More',
- click() {
- shell.openExternal('http://electron.atom.io');
- },
+ click() { shell.openExternal(learnMoreLink); },
},
];
diff --git a/ivette/src/dome/misc/system.ts b/ivette/src/dome/misc/system.ts
index 7c726722647b4feefedce7e891b83eeb2d54b824..58c8badba810a5a07a0cabb44b89caa0b66600a8 100644
--- a/ivette/src/dome/misc/system.ts
+++ b/ivette/src/dome/misc/system.ts
@@ -537,21 +537,23 @@ export function spawn(
return new Promise((result, reject) => {
const cwd = options ? options.cwd : undefined;
- const env = options && options.env ? ({ ...process.env, ...options.env }) : undefined;
+ const opt = options ? options.env : undefined;
+ const env = // Forces 'PWD' env. variable for executing a non-shell process
+ (cwd || opt) ? { ...process.env, ...opt, 'PWD': cwd } : undefined;
const stdin = stdSpec(options && options.stdin, false);
const stdout = stdSpec(options && options.stdout, true);
const stderr = stdSpec(options && options.stderr, true);
const stdio = [stdin.io, stdout.io, stderr.io];
- const opt: Exec.ForkOptions = { cwd, env, stdio };
- const fork = options && options.fork;
+ const fopt: Exec.ForkOptions = { cwd, env, stdio };
+ const forked = options && options.fork;
const cargs = args ? args.slice() : [];
let child: Exec.ChildProcess | undefined;
- if (fork) {
+ if (forked) {
stdio.push('ipc');
- child = Exec.fork(command, cargs, opt);
+ child = Exec.fork(command, cargs, fopt);
} else {
- child = Exec.spawn(command, cargs, opt);
+ child = Exec.spawn(command, cargs, fopt);
}
if (!child) reject(new Error(
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 51eb64b19f4f5f77a58e6cb45c3ecacd0fcfc471..7fb76ae8e9dd3ad5d000e8eb6012a90cf78c1737 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -364,13 +364,15 @@ const customItemCallbacks = new Map<string, callback>();
/**
Create a new custom menu in the menu bar.
- This function can be triggered at any time, and will eventually trigger
- an update of the whole application menubar.
+
+ This function shall be called statically, although calls from _secondary_
+ windows would be ignored. It is also possible to call this function from the
+ main process.
It is also possible to call this function from the main process.
@param label - the menu title (shall be unique)
-*/
+ */
export function addMenu(label: string) {
ipcRenderer.send('dome.ipc.menu.addmenu', label);
}
@@ -399,8 +401,7 @@ export interface MenuItemProps {
onClick?: () => void;
}
-/**
- Inserts a new custom item in a menu.
+/** Inserts a new custom item in a menu.
The menu can be modified later with [[setMenuItem]].
@@ -408,15 +409,15 @@ export interface MenuItemProps {
event on all application windows. The item callback, if any, is invoked only
in the process that specify it.
- Key short cuts shall be specified with the following codes:
- - `"Cmd+<Key>"` for command (MacOS) or control (Linux) key
- - `"Alt+<Key>"` for command+option (MacOS) or alt (Linux) key
- - `"Meta+<Key>"` for command+shift (MacOS) or control+alt (Linux) key
+ Key short cuts shall be specified with the following codes: - `"Cmd+<Key>"`
+ for command (MacOS) or control (Linux) key - `"Alt+<Key>"` for command+option
+ (MacOS) or alt (Linux) key - `"Meta+<Key>"` for command+shift (MacOS) or
+ control+alt (Linux) key
- This function can be triggered at any time, and will eventually trigger
- an update of the complete application menubar.
- It is also possible to call this function from the main process.
-*/
+ This function shall be called statically, although calls from _secondary_
+ windows would be ignored. It is also possible to call this function from the
+ main process.
+ */
export function addMenuItem(props: MenuItemProps) {
if (!props.id && props.type !== 'separator') {
// eslint-disable-next-line no-console
@@ -444,10 +445,6 @@ export interface MenuItemOptions {
You shall specify `null` to remove the previously registered callback
(`undefined` callback is ignored).
- This function can be triggered at any time, and will possibly trigger
- an update of the application menubar if the properties
- can not be changed dynamically in Electron.
-
It is also possible to call this function from the main process.
*/
export function setMenuItem(options: MenuItemOptions) {
@@ -601,7 +598,7 @@ export function useCache<K, V>(r: (k: K) => V, s?: Serialize<K>): (k: K) => V {
const v = r(k);
cache.set(id, v);
return v;
- }, [ cache, r, serialize ]);
+ }, [cache, r, serialize]);
return get;
}
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 171fbe23f912103aca11d18cb28e0add4fb7d2e0..af10318d6712b108301dfc243982bd083a431163 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -116,6 +116,7 @@ Ivette.registerView({
id: 'source',
rank: 1,
label: 'Source Code',
+ defaultView: true,
layout: [
['frama-c.astview', 'frama-c.sourcecode'],
'frama-c.astinfo',
@@ -123,8 +124,18 @@ Ivette.registerView({
});
Ivette.registerView({
- id: 'pivot-table',
+ id: 'properties',
rank: 2,
+ label: 'Properties',
+ layout: [
+ ['frama-c.astview', 'frama-c.sourcecode'],
+ 'frama-c.properties',
+ ],
+});
+
+Ivette.registerView({
+ id: 'pivot-table',
+ rank: 6,
label: 'Pivot Table',
layout: [
['frama-c.pivottable'],
diff --git a/ivette/src/frama-c/menu.ts b/ivette/src/frama-c/menu.ts
index f20ed94c60fce333d5aa9c23d85c8f80d90cd604..1b1af614c3b4b3149ccc614d5534696201008436 100644
--- a/ivette/src/frama-c/menu.ts
+++ b/ivette/src/frama-c/menu.ts
@@ -31,6 +31,7 @@ import * as Services from 'frama-c/kernel/api/services';
import * as Ast from 'frama-c/kernel/api/ast';
import * as Status from 'frama-c/kernel/Status';
import * as States from 'frama-c/states';
+import { ipcRenderer } from 'electron';
const cFilter = {
name: 'C source files',
@@ -134,6 +135,7 @@ async function saveSession(): Promise<void> {
}
export function init(): void {
+ ipcRenderer.invoke('dome.ipc.updateLearnMore', 'https://frama-c.com/');
Dome.addMenuItem({
menu: 'File',
label: 'Set source files…',
diff --git a/ivette/src/frama-c/plugins/dive/index.tsx b/ivette/src/frama-c/plugins/dive/index.tsx
index ddc964318ce75e33a70bbb39883adf23e2fa9805..0f89148e3e6c418c7cbf5a00f5f61735b873525c 100644
--- a/ivette/src/frama-c/plugins/dive/index.tsx
+++ b/ivette/src/frama-c/plugins/dive/index.tsx
@@ -656,10 +656,10 @@ Ivette.registerComponent({
Ivette.registerView({
id: 'dive',
label: 'Dive Dataflow',
- rank: 2,
+ rank: 5,
layout: [
- ['frama-c.astview', 'frama-c.plugins.dive', 'frama-c.locations'],
- ['frama-c.properties', 'frama-c.console'],
+ ['frama-c.astview', 'frama-c.plugins.dive'],
+ ['frama-c.properties', 'frama-c.locations'],
],
});
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 2df245b2abe7bf7506b891b4be2c375a894f0e8a..8aeb22bb817b5b6b873944d8b6f18ab43d2c4dff 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -36,7 +36,7 @@ import './style.css';
Ivette.registerView({
id: 'summary',
- rank: 1,
+ rank: 3,
label: 'Eva Summary',
layout: [
['frama-c.plugins.eva_summary', 'frama-c.plugins.eva_coverage'],
@@ -46,11 +46,11 @@ Ivette.registerView({
Ivette.registerView({
id: 'values',
- rank: 1,
+ rank: 4,
label: 'Eva Values',
layout: [
- ['frama-c.astview', 'frama-c.plugins.values'],
- 'frama-c.properties',
+ ['frama-c.astview', 'frama-c.astinfo'],
+ 'frama-c.plugins.values',
],
});
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 00c3b7738bac9049344c90b3addc42ce9b28d34f..5f0aef4d0a9f6fd0e24d1e82978ccbda8e8b9ef6 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -914,6 +914,15 @@ interface EvaluationModeProps {
setLocPin: (loc: Location, pin: boolean) => void;
}
+Dome.addMenuItem({
+ menu: 'Edit',
+ id: 'EvaluateMenu',
+ type: 'normal',
+ label: 'Evaluate',
+ key: 'Cmd+E',
+ onClick: () => evaluateEvent.emit(),
+});
+
function useEvaluationMode(props: EvaluationModeProps): void {
const { computationState, selection, setLocPin } = props;
const handleError = (): void => { return; };
@@ -941,14 +950,6 @@ function useEvaluationMode(props: EvaluationModeProps): void {
Toolbars.RegisterMode.emit(evalMode);
return () => Toolbars.UnregisterMode.emit(evalMode);
});
- Dome.addMenuItem({
- menu: 'Edit',
- id: 'EvaluateMenu',
- type: 'normal',
- label: 'Evaluate',
- key: 'Cmd+E',
- onClick: () => evaluateEvent.emit(),
- });
React.useEffect(() => {
Dome.setMenuItem({ id: 'EvaluateMenu', enabled: true });
return () => Dome.setMenuItem({ id: 'EvaluateMenu', enabled: false });
diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index a621798462c09a889bdb455af074f4205445c2bb..e4d80bb036136405cb392510e5ec90167c29b4b3 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -379,7 +379,7 @@ export interface Configuration {
/** Process environment variables (default: `undefined`). */
env?: { [VAR: string]: string };
/** Working directory (default: current). */
- cwd?: string;
+ working?: string;
/** Server command (default: `frama-c`). */
command?: string;
/** Additional server arguments (default: empty). */
@@ -423,7 +423,7 @@ export function getConfig(): Configuration {
async function _launch(): Promise<void> {
let {
env,
- cwd,
+ working,
command = 'frama-c',
params,
sockaddr,
@@ -453,12 +453,12 @@ async function _launch(): Promise<void> {
const pid = Dome.getPID();
sockaddr = System.join(tmp, `ivette.frama-c.${pid}.io`);
}
- if (!cwd) cwd = System.getWorkingDir();
- logout = logout && System.join(cwd, logout);
- logerr = logerr && System.join(cwd, logerr);
+ if (!working) working = System.getWorkingDir();
+ logout = logout && System.join(working, logout);
+ logerr = logerr && System.join(working, logerr);
params = client.commandLine(sockaddr, params);
const options = {
- cwd,
+ cwd: working,
stdout: { path: logout, pipe: true },
stderr: { path: logerr, pipe: true },
env,
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index 996c3c0878b8d1b8ae46831698fb6e446c77c0ce..50ab35b2bf0da992b523cf338d656d6530f62b20 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -20,8 +20,6 @@
/* */
/* ************************************************************************ */
-/* eslint-disable @typescript-eslint/explicit-function-return-type */
-
// --------------------------------------------------------------------------
// --- Server Controller
// --------------------------------------------------------------------------
@@ -31,13 +29,14 @@ import * as Dome from 'dome';
import * as Json from 'dome/data/json';
import * as Settings from 'dome/data/settings';
import * as Preferences from 'ivette/prefs';
-
import * as Toolbars from 'dome/frame/toolbars';
import { IconButton } from 'dome/controls/buttons';
import { LED, LEDstatus } from 'dome/controls/displays';
import { Label, Code } from 'dome/controls/labels';
import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
+import { resolve } from 'dome/system';
+
import * as Ivette from 'ivette';
import * as Server from 'frama-c/server';
@@ -55,8 +54,8 @@ const unquote = (s: string): string =>
function dumpServerConfig(sc: Server.Configuration): string {
let buffer = '';
- const { cwd, command, sockaddr, params } = sc;
- if (cwd) buffer += `--cwd ${quote(cwd)}\n`;
+ const { working, command, sockaddr, params } = sc;
+ if (working) buffer += `--working ${quote(working)}\n`;
if (command) buffer += `--command ${quote(command)}\n`;
if (sockaddr) buffer += `--socket ${sockaddr}\n`;
if (params) {
@@ -74,22 +73,26 @@ function dumpServerConfig(sc: Server.Configuration): string {
return buffer;
}
-function buildServerConfig(argv: string[], cwd?: string) {
+function buildServerConfig(argv: string[], cwd?: string): Server.Configuration {
const params = [];
let command;
let sockaddr;
- let cwdir = cwd ? unquote(cwd) : undefined;
+ let working = cwd ? unquote(cwd) : undefined;
for (let k = 0; k < (argv ? argv.length : 0); k++) {
const v = argv[k];
switch (v) {
- case '--cwd':
+ case '-C':
+ case '--working':
+ case '--cwd': // Deprecated
k += 1;
- cwdir = unquote(argv[k]);
+ working = resolve(unquote(argv[k]));
break;
+ case '-B':
case '--command':
k += 1;
- command = unquote(argv[k]);
+ command = resolve(unquote(argv[k]));
break;
+ case '-U':
case '--socket':
k += 1;
sockaddr = argv[k];
@@ -99,18 +102,37 @@ function buildServerConfig(argv: string[], cwd?: string) {
}
}
return {
- cwd: cwdir,
+ working,
command,
sockaddr,
params,
};
}
-function buildServerCommand(cmd: string) {
+function buildServerCommand(cmd: string): Server.Configuration {
return buildServerConfig(cmd.trim().split(/[ \t\n]+/));
}
-function insertConfig(hs: string[], cfg: Server.Configuration) {
+/* -------------------------------------------------------------------------- */
+/* --- History Management --- */
+/* -------------------------------------------------------------------------- */
+
+const historySetting = 'Controller.history';
+const historyDecoder = Json.jList(Json.jString);
+
+function getHistory(): string[] {
+ return Settings.getLocalStorage(historySetting, historyDecoder, []);
+}
+
+function setHistory(hs: string[]): void {
+ Settings.setLocalStorage(historySetting, hs);
+}
+
+function useHistory(): [string[], ((hs: string[]) => void)] {
+ return Settings.useLocalStorage(historySetting, historyDecoder, []);
+}
+
+function insertConfig(hs: string[], cfg: Server.Configuration): string[] {
const cmd = dumpServerConfig(cfg).trim();
const newhs =
hs.map((h) => h.trim())
@@ -127,9 +149,7 @@ function insertConfig(hs: string[], cfg: Server.Configuration) {
let reloadCommand: string | undefined;
Dome.reload.on(() => {
- const [lastCmd] = Settings.getLocalStorage(
- 'Controller.history', Json.jList(Json.jString), [],
- );
+ const [lastCmd] = getHistory();
reloadCommand = lastCmd;
});
@@ -138,7 +158,13 @@ Dome.onCommand((argv: string[], cwd: string) => {
if (reloadCommand) {
cfg = buildServerCommand(reloadCommand);
} else {
- cfg = buildServerConfig(argv, cwd);
+ const hs = getHistory();
+ if (argv.find((v) => v === '--reload' || v === '-R')) {
+ cfg = buildServerCommand(hs[0]);
+ } else {
+ cfg = buildServerConfig(argv, cwd);
+ setHistory(insertConfig(hs, cfg));
+ }
}
Server.setConfig(cfg);
Server.start();
@@ -148,7 +174,7 @@ Dome.onCommand((argv: string[], cwd: string) => {
// --- Server Control
// --------------------------------------------------------------------------
-export const Control = () => {
+export const Control = (): JSX.Element => {
const status = Server.useStatus();
let play = { enabled: false, onClick: () => { /* do nothing */ } };
@@ -199,17 +225,15 @@ export const Control = () => {
const editor = new RichTextBuffer();
-const RenderConsole = () => {
+const RenderConsole = (): JSX.Element => {
const scratch = React.useRef([] as string[]);
const [cursor, setCursor] = React.useState(-1);
const [isEmpty, setEmpty] = React.useState(true);
const [noTrash, setNoTrash] = React.useState(true);
- const [history, setHistory] = Settings.useLocalStorage(
- 'Controller.history', Json.jList(Json.jString), [],
- );
+ const [history, setHistory] = useHistory();
React.useEffect(() => {
- const callback = () => {
+ const callback = (): void => {
const cmd = editor.getValue().trim();
setEmpty(cmd === '');
setNoTrash(noTrash && cmd === history[0]);
@@ -223,7 +247,7 @@ const RenderConsole = () => {
Server.buffer.setMaxlines(maxLines);
});
- const doReload = () => {
+ const doReload = (): void => {
const cfg = Server.getConfig();
const hst = insertConfig(history, cfg);
const cmd = hst[0];
@@ -234,7 +258,7 @@ const RenderConsole = () => {
setCursor(0);
};
- const doSwitch = () => {
+ const doSwitch = (): void => {
if (cursor < 0) doReload();
else {
editor.clear();
@@ -243,7 +267,7 @@ const RenderConsole = () => {
}
};
- const doExec = () => {
+ const doExec = (): void => {
const cfg = buildServerCommand(editor.getValue());
const hst = insertConfig(history, cfg);
setHistory(hst);
@@ -253,9 +277,9 @@ const RenderConsole = () => {
Server.restart();
};
- const doMove = (target: number) => {
+ const doMove = (target: number): (undefined | (() => void)) => {
if (0 <= target && target < history.length && target !== cursor)
- return () => {
+ return (): void => {
const cmd = editor.getValue();
const pad = scratch.current;
pad[cursor] = cmd;
@@ -267,7 +291,7 @@ const RenderConsole = () => {
return undefined;
};
- const doRemove = () => {
+ const doRemove = (): void => {
const n = history.length;
if (n <= 1) doReload();
else {
@@ -361,7 +385,6 @@ Ivette.registerView({
id: 'console',
rank: -1,
label: 'Console',
- defaultView: true,
layout: 'frama-c.console',
});
@@ -369,7 +392,7 @@ Ivette.registerView({
// --- Status
// --------------------------------------------------------------------------
-export const Status = () => {
+export const Status = (): JSX.Element => {
const status = Server.useStatus();
const pending = Server.getPending();
let led: LEDstatus = 'inactive';
@@ -434,7 +457,7 @@ export const Status = () => {
// --- Server Stats
// --------------------------------------------------------------------------
-export const Stats = () => {
+export const Stats = (): (null | JSX.Element) => {
Server.useStatus();
const pending = Server.getPending();
return pending > 0 ? <Code>{pending} rq.</Code> : null;
diff --git a/nix/default.nix b/nix/default.nix
index 5bd4d181773a37483950d211d9759ab67b7cff4b..d9f8349f5d7db3034a05fff70433d66e6ed7a9e5 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -9,9 +9,9 @@ let mydir = builtins.getEnv("PWD");
};
opamPackages =
[ "ocamlfind" "zarith" "ocamlgraph" "yojson" "zmq"
- "ppx_deriving" "ppx_deriving_yojson"
+ "ppx_import" "ppx_deriving" "ppx_deriving_yojson"
"coq=8.13.0" "alt-ergo=2.2.0"
- "why3=1.4.0" "why3-coq=1.4.0"
+ "why3=1.5.0" "why3-coq=1.5.0"
"menhir=20211012"
"easy-format=1.3.2"
];
diff --git a/opam/opam b/opam/opam
index b7c3f147d041645e31f22f9a08626b5a440b6ff6..4c6a1fa77fe2003a2cc26bbf6cd9510e17119e2f 100644
--- a/opam/opam
+++ b/opam/opam
@@ -120,7 +120,7 @@ depends: [
"ocaml" { >= "4.08.1" }
"ocamlfind" # needed beyond build stage, used by -load-module
"ocamlgraph" { >= "1.8.8" }
- "why3" { >= "1.4.0" & < "1.5~" }
+ "why3" { >= "1.5.0" }
"yojson" {>= "1.6.0"}
"zarith" {>= "1.5"}
]
diff --git a/reference-configuration.md b/reference-configuration.md
index f7e6d6ae2f052e2597e66c66e354803f956b4a7b..df8c90259b25650348bcf916304d871158e1ef1b 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -7,17 +7,17 @@ support libraries (notably gtksourceview). lablgtk3 should be preferred.
- OCaml 4.08.1
- alt-ergo.2.2.0 (for wp, optional)
-- apron.v0.9.12 (for eva, optional)
+- apron.v0.9.13 (for eva, optional)
- coq.8.13.0 (for wp, optional)
- lablgtk3.3.1.1 + lablgtk3-sourceview3.3.1.1 | lablgtk.2.18.11
-- mlgmpidl.1.2.12 (for eva, optional)
+- mlgmpidl.1.2.14 (for eva, optional)
- ocamlfind.1.8.1
- ocamlgraph.1.8.8
-- ppx_deriving_yojson.3.5.2 (for mdr, optional)
-- why3.1.4.0
+- ppx_deriving_yojson.3.6.1 (for mdr, optional)
+- ppx_import.1.9.1
+- why3.1.5.0
- yojson.1.7.0
-- zarith.1.9.1
-- zmq.5.1.3 (for server, optional)
+- zarith.1.12
[^gcc-10]: As mentioned in this [OCaml PR](https://github.com/ocaml/ocaml/issues/9144)
gcc 10 changed its default linking conventions to make them more stringent,
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 505153e2f1f6a9204002f5b82a59d777febce816..c6d808f04e906cb195778fae19e2a20e7a9070a1 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -199,7 +199,8 @@ ENABLE_EVA ?=@ENABLE_EVA@
#bytes is part of the stdlib, but is used as a transitional package.
LIBRARY_NAMES := \
- findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray
+ findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray \
+ ppx_import ppx_deriving.eq
ifeq ($(HAS_LANDMARKS),yes)
LIBRARY_NAMES += landmarks landmarks-ppx
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c7551b0733be41b396abf71790e09045a5c16ef7
--- /dev/null
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -0,0 +1,1622 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 Cil_types
+
+module Orig_project =
+ State_builder.Option_ref(Project.Datatype)(
+ struct
+ let name = "Ast_diff.OrigProject"
+ let dependencies = []
+ end)
+
+type 'a correspondance =
+ [ `Same of 'a (** symbol with identical definition has been found. *)
+ | `Not_present (** no correspondance *)
+ ]
+
+module Correspondance_input =
+struct
+ type 'a t = 'a correspondance
+ let name a = Type.name a ^ " correspondance"
+ let module_name = "Correspondance"
+ let structural_descr _ = Structural_descr.t_abstract
+ let reprs x = [ `Not_present; `Same x]
+ let mk_equal eq x y =
+ match x,y with
+ | `Same x, `Same y -> eq x y
+ | `Not_present, `Not_present -> true
+ | `Same _, `Not_present
+ | `Not_present, `Same _ -> false
+ let mk_compare cmp x y =
+ match x,y with
+ | `Not_present, `Not_present -> 0
+ | `Not_present, `Same _ -> -1
+ | `Same x, `Same y -> cmp x y
+ | `Same _, `Not_present -> 1
+ let mk_hash h = function
+ | `Same x -> 117 * h x
+ | `Not_present -> 43
+ let map f = function
+ | `Same x -> `Same (f x)
+ | `Not_present -> `Not_present
+ let mk_internal_pretty_code pp prec fmt = function
+ | `Not_present -> Format.pp_print_string fmt "`Not_present"
+ | `Same x ->
+ let pp fmt = Format.fprintf fmt "`Same %a" (pp Type.Call) x in
+ Type.par prec Call fmt pp
+ let mk_pretty pp fmt = function
+ | `Not_present -> Format.pp_print_string fmt "N/A"
+ | `Same x -> Format.fprintf fmt " => %a" pp x
+ let mk_varname v = function
+ | `Not_present -> "x"
+ | `Same x -> v x ^ "_c"
+ let mk_mem_project mem query = function
+ | `Not_present -> false
+ | `Same x -> mem query x
+end
+
+module Correspondance = Datatype.Polymorphic(Correspondance_input)
+
+(* for kernel function, we are a bit more precise than a yes/no answer.
+ More precisely, we check whether a function has the same spec,
+ the same body, and whether its callees have changed (provided
+ the body itself is identical, otherwise, there's no point in checking
+ the callees.
+*)
+type partial_correspondance =
+ [ `Spec_changed (* body and callees haven't changed *)
+ | `Body_changed (* spec hasn't changed *)
+ | `Callees_changed (* spec and body haven't changed *)
+ | `Callees_spec_changed (* body hasn't changed *)
+ ]
+
+type body_correspondance =
+ [ `Body_changed
+ | `Callees_changed
+ | `Same_body
+ ]
+
+let (<=>) res (cmp,x,y) = if res <> 0 then res else cmp x y
+
+let compare_pc pc1 pc2 =
+ match pc1, pc2 with
+ | `Spec_changed, `Spec_changed -> 0
+ | `Spec_changed, _ -> -1
+ | _, `Spec_changed -> 1
+ | `Body_changed, `Body_changed -> 0
+ | `Body_changed, _ -> -1
+ | _, `Body_changed -> 1
+ | `Callees_changed, `Callees_changed -> 0
+ | `Callees_changed, _ -> -1
+ | _, `Callees_changed -> 1
+ | `Callees_spec_changed, `Callees_spec_changed -> 0
+
+let string_of_pc = function
+ | `Spec_changed -> "Spec_changed"
+ | `Body_changed -> "Body_changed"
+ | `Callees_changed -> "Callees_changed"
+ | `Callees_spec_changed -> "Callees_spec_changed"
+
+let pretty_pc fmt =
+ let open Format in
+ function
+ | `Spec_changed -> pp_print_string fmt "(spec changed)"
+ | `Body_changed -> pp_print_string fmt "(body changed)"
+ | `Callees_changed -> pp_print_string fmt "(callees changed)"
+ | `Callees_spec_changed -> pp_print_string fmt "(callees and spec changed)"
+
+type 'a code_correspondance =
+ [ 'a correspondance
+ | `Partial of 'a * partial_correspondance
+ ]
+
+module Code_correspondance_input =
+struct
+ type 'a t = 'a code_correspondance
+ let name a = Type.name a ^ " code_correspondance"
+ let module_name = "Code_correspondance"
+ let structural_descr _ = Structural_descr.t_abstract
+ let reprs = Correspondance_input.reprs
+ let mk_equal eq x y =
+ match x,y with
+ | `Partial(x,pc), `Partial(x',pc') -> eq x x' && (compare_pc pc pc' = 0)
+ | `Partial _, _ | _, `Partial _ -> false
+ | (#correspondance as c), (#correspondance as c') ->
+ Correspondance_input.mk_equal eq c c'
+
+ let mk_compare cmp x y =
+ match x,y with
+ | `Partial(x,pc), `Partial(x',pc') ->
+ cmp x x' <=> (compare_pc,pc,pc')
+ | `Partial _, `Same _ -> -1
+ | `Same _, `Partial _ -> 1
+ | `Partial _, `Not_present -> 1
+ | `Not_present, `Partial _ -> -1
+ | (#correspondance as c), (#correspondance as c') ->
+ Correspondance_input.mk_compare cmp c c'
+
+ let mk_hash hash = function
+ | `Partial (x,_) -> 57 * hash x
+ | #correspondance as x -> Correspondance_input.mk_hash hash x
+
+ let map f = function
+ | `Partial(x,pc) -> `Partial(f x,pc)
+ | (#correspondance as x) -> Correspondance_input.map f x
+
+ let mk_internal_pretty_code pp prec fmt = function
+ | `Partial (x,flags) ->
+ let pp fmt =
+ Format.fprintf fmt "`Partial (%a,%s)"
+ (pp Type.Call) x (string_of_pc flags)
+ in
+ Type.par prec Call fmt pp
+ | #correspondance as x ->
+ Correspondance_input.mk_internal_pretty_code pp prec fmt x
+
+ let mk_pretty pp fmt = function
+ | `Partial(x,flags) ->
+ Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
+ | #correspondance as x -> Correspondance_input.mk_pretty pp fmt x
+
+ let mk_varname f = function
+ | `Partial (x,_) -> f x ^ "_pc"
+ | #correspondance as x -> Correspondance_input.mk_varname f x
+
+ let mk_mem_project f p = function
+ | `Partial (x,_) -> f p x
+ | #correspondance as x -> Correspondance_input.mk_mem_project f p x
+end
+
+module Code_correspondance = Datatype.Polymorphic(Code_correspondance_input)
+
+module Info(I: sig val name: string end) =
+ (struct
+ let name = "Ast_diff." ^ I.name
+ let dependencies = [ Ast.self; Orig_project.self ]
+ let size = 43
+ end)
+
+(* Map of symbols under analysis, in case of recursion.
+ Note that this can only happen with aggregate types, logic
+ types, and function (both C and ACSL). Other symbols must be
+ correctly ordered in a well-formed AST
+*)
+type is_same_env =
+ {
+ compinfo: compinfo Cil_datatype.Compinfo.Map.t;
+ kernel_function: kernel_function Kernel_function.Map.t;
+ local_vars: varinfo Cil_datatype.Varinfo.Map.t;
+ logic_info: logic_info Cil_datatype.Logic_info.Map.t;
+ logic_type_info: logic_type_info Cil_datatype.Logic_type_info.Map.t;
+ logic_local_vars: logic_var Cil_datatype.Logic_var.Map.t;
+ logic_type_vars: string Datatype.String.Map.t;
+ (* goto targets pairs are checked afterwards, so that forward gotos
+ do not interrupt the linear visit.
+ We thus collect them in the environment.
+ *)
+ goto_targets: (stmt * stmt) list;
+ }
+
+module type Correspondance_table = sig
+ include State_builder.Hashtbl
+ val pretty_data: Format.formatter -> data -> unit
+end
+
+module Build(H:Datatype.S_with_collections)(D:Datatype.S):
+ Correspondance_table with type key = H.t and type data = D.t =
+struct
+ include
+ State_builder.Hashtbl(H.Hashtbl)(D)
+ (Info(struct let name = "Ast_diff." ^ D.name end))
+ let pretty_data = D.pretty
+end
+
+module Build_correspondance(H:Datatype.S_with_collections) =
+ Build(H)(Correspondance.Make(H))
+
+module Build_code_correspondance(H:Datatype.S_with_collections) =
+ Build(H)(Code_correspondance.Make(H))
+
+module Varinfo = Build_correspondance(Cil_datatype.Varinfo)
+
+module Compinfo = Build_correspondance(Cil_datatype.Compinfo)
+
+module Enuminfo = Build_correspondance(Cil_datatype.Enuminfo)
+
+module Enumitem = Build_correspondance(Cil_datatype.Enumitem)
+
+module Typeinfo = Build_correspondance(Cil_datatype.Typeinfo)
+
+module Stmt = Build_code_correspondance(Cil_datatype.Stmt)
+
+module Logic_info = Build_correspondance(Cil_datatype.Logic_info)
+
+module Logic_type_info = Build_correspondance(Cil_datatype.Logic_type_info)
+
+module Logic_ctor_info = Build_correspondance(Cil_datatype.Logic_ctor_info)
+
+module Fieldinfo = Build_correspondance(Cil_datatype.Fieldinfo)
+
+module Model_info = Build_correspondance(Cil_datatype.Model_info)
+
+module Logic_var = Build_correspondance(Cil_datatype.Logic_var)
+
+module Kf = Kernel_function
+
+module Kernel_function = Build_code_correspondance(Kernel_function)
+
+module Fundec = Build_correspondance(Cil_datatype.Fundec)
+
+let make_correspondance candidate has_same_spec code_corres =
+ match has_same_spec, code_corres with
+ | false, `Body_changed -> `Not_present
+ | false, `Callees_changed ->
+ `Partial(candidate,`Callees_spec_changed)
+ | false, `Same_body ->
+ `Partial(candidate, `Spec_changed)
+ | true, `Same_body ->
+ `Same candidate
+ | true, ((`Body_changed|`Callees_changed) as c) ->
+ `Partial(candidate, c)
+
+let (&&>) (res,env) f =
+ match res with
+ | `Body_changed -> `Body_changed, env
+ | `Same_body -> f env
+ | `Callees_changed ->
+ let res', env = f env in
+ match res' with
+ | `Body_changed -> `Body_changed, env
+ | `Same_body | `Callees_changed -> `Callees_changed, env
+
+let (&&&) (res, env) f = if res then f env else false, env
+
+let empty_env =
+ { compinfo = Cil_datatype.Compinfo.Map.empty;
+ kernel_function = Kf.Map.empty;
+ local_vars = Cil_datatype.Varinfo.Map.empty;
+ logic_info = Cil_datatype.Logic_info.Map.empty;
+ logic_type_info = Cil_datatype.Logic_type_info.Map.empty;
+ logic_local_vars = Cil_datatype.Logic_var.Map.empty;
+ logic_type_vars = Datatype.String.Map.empty;
+ goto_targets = []
+ }
+
+let add_locals f f' env =
+ let add_one env v v' =
+ { env with local_vars = Cil_datatype.Varinfo.Map.add v v' env.local_vars }
+ in
+ List.fold_left2 add_one env f f'
+
+(* local static variables are in fact global. As soon as we have determined
+ that they have a correspondance, we add them to the global bindings *)
+let add_statics l l' =
+ let add_one v v' = Varinfo.add v (`Same v') in
+ List.iter2 add_one l l'
+
+let add_logic_vars p p' env =
+ let add_one env lv lv' =
+ { env with
+ logic_local_vars =
+ Cil_datatype.Logic_var.Map.add lv lv' env.logic_local_vars }
+ in
+ List.fold_left2 add_one env p p'
+
+let add_logic_info v v' env =
+ { env with logic_info = Cil_datatype.Logic_info.Map.add v v' env.logic_info }
+
+let logic_type_vars_env l l' env =
+ if List.length l = List.length l' then begin
+ let logic_type_vars =
+ List.fold_left2 (fun env s s' -> Datatype.String.Map.add s s' env)
+ env.logic_type_vars l l'
+ in
+ true, { env with logic_type_vars }
+ end else false, env
+
+let formals_correspondance f f' =
+ let add_one v v' = Varinfo.add v (`Same v') in
+ List.iter2 add_one f f'
+
+let logic_prms_correspondance p p' =
+ let add_one lv lv' =
+ Logic_var.add lv (`Same lv') in
+ List.iter2 add_one p p'
+
+(** TODO: use location info to detect potential renaming.
+ Requires some information about syntactic diff. *)
+let find_candidate_type ?loc:_loc ti =
+ if Globals.Types.mem_type Logic_typing.Typedef ti.tname then begin
+ match Globals.Types.global Logic_typing.Typedef ti.tname with
+ | GType(ti,_) -> Some ti
+ | g ->
+ Kernel.fatal
+ "Expected typeinfo instead of %a" Cil_datatype.Global.pretty g
+ end else None
+
+let find_candidate_compinfo ?loc:_loc ci =
+ let su = if ci.cstruct then Logic_typing.Struct else Logic_typing.Union in
+ if Globals.Types.mem_type su ci.cname then begin
+ match Globals.Types.find_type su ci.cname with
+ | TComp(ci', _) -> Some ci'
+ | t ->
+ Kernel.fatal
+ "Expected compinfo instead of %a"
+ Printer.pp_typ t
+ end else None
+
+let find_candidate_enuminfo ?loc:_loc ei =
+ if Globals.Types.mem_type Logic_typing.Enum ei.ename then begin
+ match Globals.Types.find_type Logic_typing.Enum ei.ename with
+ | TEnum(ei,_) -> Some ei
+ | t ->
+ Kernel.fatal
+ "Expected enuminfo instead of %a"
+ Printer.pp_typ t
+ end else None
+
+let find_candidate_varinfo ?loc:_loc vi where =
+ try
+ Some (Globals.Vars.find_from_astinfo vi.vname where)
+ with Not_found -> None
+
+let find_candidate_func ?loc:_loc kf =
+ try
+ Some (Globals.Functions.find_by_name (Kf.get_name kf))
+ with Not_found -> None
+
+let find_candidate_logic_type ?loc:_loc ti =
+ try
+ Some (Logic_env.find_logic_type ti.lt_name)
+ with Not_found -> None
+
+let is_same_opt f o o' env =
+ match o, o' with
+ | None, None -> true
+ | Some v, Some v' -> f v v' env
+ | _ -> false
+
+let is_same_opt_env f o o' env =
+ match o, o' with
+ | None, None -> true, env
+ | Some v, Some v' -> f v v' env
+ | _ -> false, env
+
+let is_same_pair f1 f2 (x1,x2) (y1,y2) env = f1 x1 y1 env && f2 x2 y2 env
+
+let rec is_same_list f l l' env =
+ match l, l' with
+ | [], [] -> true
+ | h::t, h'::t' -> f h h' env && is_same_list f t t' env
+ | _ -> false
+
+let rec is_same_list_env f l l' env =
+ match l, l' with
+ | [], [] -> true, env
+ | h::t, h'::t' -> f h h' env &&& is_same_list_env f t t'
+ | _ -> false, env
+
+let get_original_kf vi =
+ let selection = State_selection.of_list
+ [Kernel_function.self; Annotations.funspec_state; Globals.Functions.self]
+ in
+ Project.on ~selection (Orig_project.get()) Globals.Functions.get vi
+
+let check_goto_targets env =
+ let check_one (s,s') =
+ match Stmt.find s with
+ | `Not_present -> false
+ | `Same s'' | `Partial (s'',_) ->
+ (* From the goto point of view, what matters is that the targets
+ themselves have a correspondance. If they're e.g. calls to a
+ function that has itself changed, or blocks whose content has
+ changed, it has already been detected when comparing the targets,
+ and will be dealt with accordingly as the fundec level. *)
+ Cil_datatype.Stmt.equal s' s''
+ | exception Not_found -> false
+ in
+ if List.for_all check_one env.goto_targets then `Same_body, env
+ else `Body_changed, env
+
+let is_matching_fieldinfo fi fi' =
+ match Fieldinfo.find fi with
+ | `Not_present -> false
+ | `Same fi'' -> Cil_datatype.Fieldinfo.equal fi' fi''
+ | exception Not_found ->
+ Kernel.fatal "Unbound field %a in AST diff"
+ Cil_datatype.Fieldinfo.pretty fi
+
+let is_matching_model_info mf mf' =
+ match Model_info.find mf with
+ | `Not_present -> false
+ | `Same mf'' -> Cil_datatype.Model_info.equal mf' mf''
+ | exception Not_found ->
+ Kernel.fatal "Unbound model field %a in AST diff"
+ Cil_datatype.Model_info.pretty mf
+
+let is_matching_logic_type_var a a' env =
+ match Datatype.String.Map.find_opt a env.logic_type_vars with
+ | None -> false
+ | Some a'' -> Datatype.String.equal a' a''
+
+module Unop = struct
+ type t = [%import: Cil_types.unop] [@@deriving eq]
+end
+
+module Binop = struct
+ type t = [%import: Cil_types.binop] [@@deriving eq]
+end
+
+module Ikind = struct
+ type t = [%import: Cil_types.ikind] [@@deriving eq]
+end
+
+module Fkind = struct
+ type t = [%import: Cil_types.fkind] [@@deriving eq]
+end
+
+module Predicate_kind = struct
+ type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
+end
+
+module Logic_builtin_label = struct
+ type t = [%import: Cil_types.logic_builtin_label] [@@deriving eq]
+end
+
+module Relation = struct
+ type t = [%import: Cil_types.relation] [@@deriving eq]
+end
+
+module Termination_kind = struct
+ type t = [%import: Cil_types.termination_kind] [@@deriving eq]
+end
+
+let is_same_behavior_set l l' =
+ Datatype.String.Set.(equal (of_list l) (of_list l'))
+
+let are_same_cd_clauses l l' =
+ let module StringSetSet = Set.Make(Datatype.String.Set) in
+ let of_list l =
+ StringSetSet.of_list (List.map Datatype.String.Set.of_list l)
+ in
+ StringSetSet.equal (of_list l) (of_list l')
+
+let is_same_logic_label l l' _env =
+ match l, l' with
+ | StmtLabel s, StmtLabel s' ->
+ (* Contrarily to labels in goto statement, C labels in the logic can only
+ refer to previous statements thanks to ACSL typing rules. Hence, we can
+ directly check the Stmt table without resorting to deferred check by
+ updating env.goto_targets
+ *)
+ (match Stmt.find !s with
+ | `Not_present -> false
+ | `Same s'' | `Partial(s'',_) ->
+ Cil_datatype.Stmt.equal !s' s''
+ | exception Not_found -> false)
+ | FormalLabel s, FormalLabel s' -> Datatype.String.equal s s'
+ | BuiltinLabel l, BuiltinLabel l' -> Logic_builtin_label.equal l l'
+ | (StmtLabel _ | FormalLabel _ | BuiltinLabel _), _ -> false
+
+let rec is_same_predicate p p' env =
+ (* names are semantically irrelevant. *)
+ is_same_predicate_node p.pred_content p'.pred_content env
+
+and is_same_predicate_node p p' env =
+ match p, p' with
+ | Pfalse, Pfalse -> true
+ | Ptrue, Ptrue -> true
+ | Papp(p,labs,args), Papp(p',labs',args') ->
+ is_matching_logic_info p p' env &&
+ is_same_list is_same_logic_label labs labs' env &&
+ is_same_list is_same_term args args' env
+ | Pseparated t, Pseparated t' -> is_same_list is_same_term t t' env
+ | Prel (r,t1,t2), Prel(r',t1',t2') ->
+ Relation.equal r r' && is_same_term t1 t1' env && is_same_term t2 t2' env
+ | Pand(p1,p2), Pand(p1',p2')
+ | Por(p1,p2), Por(p1',p2')
+ | Pxor(p1,p2), Pxor(p1',p2')
+ | Pimplies(p1,p2), Pimplies(p1',p2')
+ | Piff(p1,p2), Piff(p1',p2') ->
+ is_same_predicate p1 p1' env && is_same_predicate p2 p2' env
+ | Pnot p, Pnot p' -> is_same_predicate p p' env
+ | Pif(t,p1,p2), Pif(t',p1',p2') ->
+ is_same_term t t' env &&
+ is_same_predicate p1 p1' env &&
+ is_same_predicate p2 p2' env
+ | Plet(v,p), Plet(v',p') ->
+ if is_same_logic_info v v' env then begin
+ let env = add_logic_info v v' env in
+ let env = add_logic_vars [v.l_var_info] [v'.l_var_info] env in
+ is_same_predicate p p' env
+ end else false
+ | Pforall(q,p), Pforall(q',p')
+ | Pexists(q,p), Pexists(q',p') ->
+ if is_same_list is_same_logic_var q q' env then begin
+ let env = add_logic_vars q q' env in
+ is_same_predicate p p' env
+ end else false
+ | Pat(p,l), Pat(p',l') ->
+ is_same_predicate p p' env && is_same_logic_label l l' env
+ | Pobject_pointer(l,t), Pobject_pointer(l',t')
+ | Pvalid_read(l,t), Pvalid_read(l',t')
+ | Pvalid(l,t), Pvalid(l',t')
+ | Pinitialized(l,t), Pinitialized(l',t')
+ | Pdangling(l,t), Pdangling(l',t')
+ | Pallocable(l,t), Pallocable(l',t')
+ | Pfreeable(l,t), Pfreeable(l',t') ->
+ is_same_logic_label l l' env && is_same_term t t' env
+ | Pfresh(l1,l2,p,s), Pfresh(l1',l2',p',s') ->
+ is_same_logic_label l1 l1' env &&
+ is_same_logic_label l2 l2' env &&
+ is_same_term p p' env &&
+ is_same_term s s' env
+ | Pvalid_function(t), Pvalid_function(t') -> is_same_term t t' env
+ | (Pfalse | Ptrue | Papp _ | Pseparated _ | Prel _ | Pand _ | Por _ | Pxor _
+ | Pimplies _ | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
+ | Pat _ | Pobject_pointer _ | Pvalid_read _ | Pvalid _ | Pinitialized _
+ | Pdangling _ | Pallocable _ | Pfreeable _ | Pfresh _
+ | Pvalid_function _), _ -> false
+
+and is_same_logic_constant c c' env =
+ match c,c' with
+ | LEnum ei, LEnum ei' ->
+ (match enumitem_correspondance ei env with
+ | `Same ei'' -> Cil_datatype.Enumitem.equal ei' ei''
+ | `Not_present -> false)
+ | LEnum _, _ | _, LEnum _ -> false
+ | (Integer _ | LStr _ | LWStr _ | LChr _ | LReal _), _ ->
+ Cil_datatype.Logic_constant.equal c c'
+
+and is_same_term t t' env =
+ is_same_term_node t.term_node t'.term_node env
+
+and is_same_term_node t t' env =
+ match t,t' with
+ | TConst c, TConst c' -> is_same_logic_constant c c' env
+ | TLval lv, TLval lv' -> is_same_term_lval lv lv' env
+ | TSizeOf t, TSizeOf t'
+ | TAlignOf t, TAlignOf t' -> is_same_type t t' env
+ | TSizeOfE t, TSizeOfE t'
+ | TAlignOfE t, TAlignOfE t' -> is_same_term t t' env
+ | TSizeOfStr s, TSizeOfStr s' -> String.length s = String.length s'
+ | TUnOp(op,t), TUnOp(op',t') -> Unop.equal op op' && is_same_term t t' env
+ | TBinOp(op,t1,t2), TBinOp(op',t1',t2') ->
+ Binop.equal op op' && is_same_term t1 t1' env && is_same_term t2 t2' env
+ | TCastE(typ,term), TCastE(typ',term') ->
+ is_same_type typ typ' env && is_same_term term term' env
+ | TAddrOf lv, TAddrOf lv'
+ | TStartOf lv, TStartOf lv' -> is_same_term_lval lv lv' env
+ | Tapp(f,labs,args), Tapp(f',labs',args') ->
+ is_matching_logic_info f f' env &&
+ is_same_list is_same_logic_label labs labs' env &&
+ is_same_list is_same_term args args' env
+ | Tlambda(q,t), Tlambda(q',t') ->
+ if is_same_list is_same_logic_var q q' env then begin
+ let env = add_logic_vars q q' env in
+ is_same_term t t' env
+ end else false
+ | TDataCons(c,args), TDataCons(c',args') ->
+ is_matching_logic_ctor c c' env &&
+ is_same_list is_same_term args args' env
+ | Tif(c,t1,t2), Tif(c',t1',t2') ->
+ is_same_term c c' env &&
+ is_same_term t1 t1' env &&
+ is_same_term t2 t2' env
+ | Tat(t,l), Tat(t',l') ->
+ is_same_term t t' env && is_same_logic_label l l' env
+ | Tbase_addr(l,t), Tbase_addr(l',t')
+ | Toffset(l,t), Toffset(l',t')
+ | Tblock_length(l,t), Tblock_length(l',t') ->
+ is_same_logic_label l l' env && is_same_term t t' env
+ | Tnull, Tnull -> true
+ | TLogic_coerce(typ,t), TLogic_coerce(typ',t') ->
+ is_same_logic_type typ typ' env && is_same_term t t' env
+ | TUpdate(a,o,v), TUpdate(a',o',v') ->
+ is_same_term a a' env &&
+ is_same_term_offset o o' env &&
+ is_same_term v v' env
+ | Ttypeof t, Ttypeof t' -> is_same_term t t' env
+ | Ttype t, Ttype t' -> is_same_type t t' env
+ | Tempty_set, Tempty_set -> true
+ | Tunion l, Tunion l'
+ | Tinter l, Tinter l' -> is_same_list is_same_term l l' env
+ | Tcomprehension(t,q,p), Tcomprehension(t',q',p') ->
+ if is_same_list is_same_logic_var q q' env then begin
+ let env = add_logic_vars q q' env in
+ is_same_term t t' env && is_same_opt is_same_predicate p p' env
+ end else false
+ | Trange(l,u), Trange(l',u') ->
+ is_same_opt is_same_term l l' env && is_same_opt is_same_term u u' env
+ | Tlet(v,t), Tlet(v',t') ->
+ if is_same_logic_info v v' env then begin
+ let env = add_logic_info v v' env in
+ let env = add_logic_vars [v.l_var_info] [v'.l_var_info] env in
+ is_same_term t t' env
+ end else false
+ | (TConst _ | TLval _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
+ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
+ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _ | Tbase_addr _
+ | Toffset _ | Tblock_length _ | Tnull | TLogic_coerce _ | TUpdate _
+ | Ttypeof _ | Ttype _ | Tempty_set | Tunion _ | Tinter _ | Tcomprehension _
+ | Tlet _ | Trange _), _ -> false
+
+and is_same_term_lval (lh,lo) (lh',lo') env =
+ is_same_term_lhost lh lh' env && is_same_term_offset lo lo' env
+
+and is_same_term_lhost lh lh' env =
+ match lh, lh' with
+ | TVar lv, TVar lv' -> is_matching_logic_var lv lv' env
+ | TResult _, TResult _ -> true
+ | TMem p, TMem p' -> is_same_term p p' env
+ | (TVar _ | TResult _ | TMem _), _ -> false
+
+and is_matching_logic_var lv lv' env =
+ match lv.lv_origin, lv'.lv_origin with
+ | Some vi, Some vi' -> is_matching_varinfo vi vi' env
+ | None, None ->
+ (match Cil_datatype.Logic_var.Map.find_opt lv env.logic_local_vars with
+ | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+ | None ->
+ (match Logic_var.find lv with
+ | `Not_present -> false
+ | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+ | exception Not_found ->
+ if lv.lv_name = "\\exit_status" && lv'.lv_name = "\\exit_status"
+ then begin Logic_var.add lv (`Same lv'); true end
+ else begin
+ match logic_var_correspondance lv env with
+ | None -> false
+ | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+ end))
+ | _ -> false
+
+and logic_var_correspondance lv env =
+ match find_candidate_logic_var lv env with
+ | None -> None
+ | Some lv' -> Logic_var.add lv (`Same lv'); Some lv'
+
+and is_same_term_offset lo lo' env =
+ match lo, lo' with
+ | TNoOffset, TNoOffset -> true
+ | TField(f,o), TField(f',o') ->
+ is_matching_fieldinfo f f' && is_same_term_offset o o' env
+ | TModel(f,o), TModel(f',o') ->
+ is_matching_model_info f f' && is_same_term_offset o o' env
+ | TIndex(i,o), TIndex(i',o') ->
+ is_same_term i i' env && is_same_term_offset o o' env
+ | (TNoOffset | TField _ | TModel _ | TIndex _), _ -> false
+
+and is_same_toplevel_predicate p p' env =
+ Predicate_kind.equal p.tp_kind p'.tp_kind &&
+ is_same_predicate p.tp_statement p'.tp_statement env
+
+and is_same_identified_predicate p p' env =
+ is_same_toplevel_predicate p.ip_content p'.ip_content env
+
+and is_same_identified_term t t' env =
+ is_same_term t.it_content t'.it_content env
+
+and is_same_post_cond (k,p) (k',p') env =
+ Termination_kind.equal k k' && is_same_identified_predicate p p' env
+
+and is_same_deps d d' env =
+ match d,d' with
+ | FromAny, FromAny -> true
+ | From l, From l' -> is_same_list is_same_identified_term l l' env
+ | (FromAny | From _), _ -> false
+
+and is_same_from (t,f) (t',f') env =
+ is_same_identified_term t t' env && is_same_deps f f' env
+
+and is_same_assigns a a' env =
+ match a,a' with
+ | WritesAny, WritesAny -> true
+ | Writes l, Writes l' -> is_same_list is_same_from l l' env
+ | (WritesAny | Writes _), _ -> false
+
+and is_same_allocation a a' env =
+ match a,a' with
+ | FreeAllocAny, FreeAllocAny -> true
+ | FreeAlloc(f,a), FreeAlloc(f',a') ->
+ is_same_list is_same_identified_term f f' env &&
+ is_same_list is_same_identified_term a a' env
+ | (FreeAllocAny | FreeAlloc _),_ -> false
+
+and is_same_behavior b b' env =
+ is_same_list is_same_identified_predicate b.b_requires b'.b_requires env &&
+ is_same_list is_same_identified_predicate b.b_assumes b'.b_assumes env &&
+ is_same_list is_same_post_cond b.b_post_cond b'.b_post_cond env &&
+ is_same_assigns b.b_assigns b'.b_assigns env &&
+ is_same_allocation b.b_allocation b'.b_allocation env
+(* TODO: also consider ACSL extensions, with the help of the plugins
+ that handle them. *)
+
+and is_same_variant (v,m) (v',m') env =
+ is_same_term v v' env && is_same_opt is_matching_logic_info m m' env
+
+and is_same_loop_pragma p p' env =
+ match p, p' with
+ | Unroll_specs l, Unroll_specs l'
+ | Widen_hints l, Widen_hints l'
+ | Widen_variables l, Widen_variables l' ->
+ is_same_list is_same_term l l' env
+ | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
+
+and is_same_slice_pragma p p' env =
+ match p, p' with
+ | SPexpr t, SPexpr t' -> is_same_term t t' env
+ | SPctrl, SPctrl -> true
+ | SPstmt, SPstmt -> true
+ | (SPexpr _ | SPctrl | SPstmt), _ -> false
+
+and is_same_impact_pragma p p' env =
+ match p, p' with
+ | IPexpr t, IPexpr t' -> is_same_term t t' env
+ | IPstmt, IPstmt -> true
+ | (IPexpr _ | IPstmt), _ -> false
+
+and is_same_pragma p p' env =
+ match p,p' with
+ | Loop_pragma p, Loop_pragma p' -> is_same_loop_pragma p p' env
+ | Slice_pragma p, Slice_pragma p' -> is_same_slice_pragma p p' env
+ | Impact_pragma p, Impact_pragma p' -> is_same_impact_pragma p p' env
+ | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
+
+and are_same_behaviors bhvs bhvs' env =
+ let treat_one_behavior acc b =
+ match List.partition (fun b' -> b.b_name = b'.b_name) acc with
+ | [], _ -> raise Exit
+ | [b'], acc ->
+ if is_same_behavior b b' env then acc else raise Exit
+ | _ ->
+ Kernel.fatal "found several behaviors with the same name %s" b.b_name
+ in
+ try
+ match List.fold_left treat_one_behavior bhvs' bhvs with
+ | [] -> true
+ | _ -> (* new behaviors appeared: spec has changed. *) false
+ with Exit -> false
+
+and is_same_funspec s s' env =
+ are_same_behaviors s.spec_behavior s'.spec_behavior env &&
+ is_same_opt is_same_variant s.spec_variant s'.spec_variant env &&
+ is_same_opt is_same_identified_predicate
+ s.spec_terminates s'.spec_terminates env &&
+ are_same_cd_clauses s.spec_complete_behaviors s'.spec_complete_behaviors &&
+ are_same_cd_clauses s.spec_disjoint_behaviors s'.spec_disjoint_behaviors
+
+and is_same_code_annotation a a' env =
+ match a.annot_content, a'.annot_content with
+ | AAssert (bhvs, p), AAssert(bhvs',p') ->
+ is_same_behavior_set bhvs bhvs' && is_same_toplevel_predicate p p' env
+ | AStmtSpec (bhvs, s), AStmtSpec(bhvs', s') ->
+ is_same_behavior_set bhvs bhvs' && is_same_funspec s s' env
+ | AInvariant (bhvs, is_loop, p), AInvariant(bhvs', is_loop', p') ->
+ is_same_behavior_set bhvs bhvs' && is_loop = is_loop' &&
+ is_same_toplevel_predicate p p' env
+ | AVariant v, AVariant v' -> is_same_variant v v' env
+ | AAssigns(bhvs, a), AAssigns(bhvs', a') ->
+ is_same_behavior_set bhvs bhvs' && is_same_assigns a a' env
+ | AAllocation(bhvs, a), AAllocation(bhvs',a') ->
+ is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
+ | APragma p, APragma p' -> is_same_pragma p p' env
+ | AExtended _, AExtended _ -> true (*TODO: checks also for extended clauses*)
+ | (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
+ | AAllocation _ | APragma _ | AExtended _), _ -> false
+
+and is_same_logic_type t t' env =
+ match t,t' with
+ | Ctype t, Ctype t' -> is_same_type t t' env
+ | Ltype (t,prms), Ltype (t',prms') ->
+ is_matching_logic_type_info t t' env &&
+ is_same_list is_same_logic_type prms prms' env
+ | Lvar s, Lvar s' -> is_matching_logic_type_var s s' env
+ | Linteger, Linteger -> true
+ | Lreal, Lreal -> true
+ | Larrow(args,rt), Larrow(args', rt') ->
+ is_same_list is_same_logic_type args args' env &&
+ is_same_logic_type rt rt' env
+ | (Ctype _ | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _),_ -> false
+
+and is_same_inductive_case (_,labs,tprms,p) (_,labs',tprms',p') env =
+ let res, env =
+ (is_same_list is_same_logic_label labs labs' env, env) &&&
+ logic_type_vars_env tprms tprms'
+ in
+ res && is_same_predicate p p' env
+
+and is_same_logic_body b b' env =
+ match b,b' with
+ | LBnone, LBnone -> true
+ | LBreads l, LBreads l' ->
+ is_same_list is_same_identified_term l l' env
+ | LBterm t, LBterm t' -> is_same_term t t' env
+ | LBpred p, LBpred p' -> is_same_predicate p p' env
+ | LBinductive l, LBinductive l' ->
+ is_same_list is_same_inductive_case l l' env
+ | (LBnone | LBreads _ | LBterm _ | LBpred _ | LBinductive _), _ -> false
+
+and is_same_logic_ctor_info c c' env =
+ (* we rely on order in the type declaration to match constructors,
+ not on names. *)
+ is_same_list is_same_logic_type c.ctor_params c'.ctor_params env
+
+and is_same_logic_type_def d d' env =
+ match d,d' with
+ | LTsum l, LTsum l' ->
+ if is_same_list is_same_logic_ctor_info l l' env then begin
+ List.iter2 (fun c c' -> Logic_ctor_info.add c (`Same c')) l l';
+ true
+ end else begin
+ List.iter (fun c -> Logic_ctor_info.add c `Not_present) l;
+ false
+ end
+ | LTsyn t, LTsyn t' -> is_same_logic_type t t' env
+ | (LTsum _ | LTsyn _), _ -> false
+
+and is_same_logic_info li li' env =
+ let res,env =
+ (is_same_list is_same_logic_label li.l_labels li'.l_labels env, env) &&&
+ logic_type_vars_env li.l_tparams li'.l_tparams &&&
+ logic_vars_env li.l_profile li'.l_profile
+ in
+ res && is_same_opt is_same_logic_type li.l_type li'.l_type env &&
+ is_same_logic_body li.l_body li'.l_body env
+
+and is_same_logic_type_info ti ti' env =
+ let res,env =
+ (Cil_datatype.Attributes.equal ti.lt_attr ti'.lt_attr, env) &&&
+ logic_type_vars_env ti.lt_params ti'.lt_params
+ in
+ res && is_same_opt is_same_logic_type_def ti.lt_def ti'.lt_def env
+
+and is_same_model_info mi mi' env =
+ is_same_type mi.mi_base_type mi'.mi_base_type env &&
+ is_same_logic_type mi.mi_field_type mi'.mi_field_type env &&
+ Cil_datatype.Attributes.equal mi.mi_attr mi'.mi_attr
+
+and is_same_type t t' env =
+ match t, t' with
+ | TVoid a, TVoid a' -> Cil_datatype.Attributes.equal a a'
+ | TInt (ik,a), TInt(ik',a') ->
+ Ikind.equal ik ik' && Cil_datatype.Attributes.equal a a'
+ | TFloat (fk,a), TFloat(fk', a') ->
+ Fkind.equal fk fk' && Cil_datatype.Attributes.equal a a'
+ | TBuiltin_va_list a, TBuiltin_va_list a' ->
+ Cil_datatype.Attributes.equal a a'
+ | TPtr(t,a), TPtr(t',a') ->
+ is_same_type t t' env && Cil_datatype.Attributes.equal a a'
+ | TArray(t,s,a), TArray(t',s',a') ->
+ is_same_type t t' env &&
+ is_same_opt is_same_exp s s' env &&
+ Cil_datatype.Attributes.equal a a'
+ | TFun(rt,l,var,a), TFun(rt', l', var', a') ->
+ is_same_type rt rt' env &&
+ is_same_opt (is_same_list is_same_formal) l l' env &&
+ (var = var') &&
+ Cil_datatype.Attributes.equal a a'
+ | TNamed(t,a), TNamed(t',a') ->
+ let correspondance = typeinfo_correspondance t env in
+ (match correspondance with
+ | `Not_present -> false
+ | `Same t'' -> Cil_datatype.Typeinfo.equal t' t'') &&
+ Cil_datatype.Attributes.equal a a'
+ | TComp(c,a), TComp(c', a') ->
+ let correspondance = compinfo_correspondance c env in
+ (match correspondance with
+ | `Not_present -> false
+ | `Same c'' -> Cil_datatype.Compinfo.equal c' c'') &&
+ Cil_datatype.Attributes.equal a a'
+ | TEnum(e,a), TEnum(e',a') ->
+ let correspondance = enuminfo_correspondance e env in
+ (match correspondance with
+ | `Not_present -> false
+ | `Same e'' -> Cil_datatype.Enuminfo.equal e' e'') &&
+ Cil_datatype.Attributes.equal a a'
+ | (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _ | TPtr _ | TArray _
+ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false
+
+and is_same_compinfo ci ci' env =
+ ci.cstruct = ci'.cstruct &&
+ Cil_datatype.Attributes.equal ci.cattr ci'.cattr &&
+ is_same_opt (is_same_list is_same_fieldinfo) ci.cfields ci'.cfields env
+
+and is_same_enuminfo ei ei' env =
+ Cil_datatype.Attributes.equal ei.eattr ei'.eattr &&
+ Ikind.equal ei.ekind ei'.ekind &&
+ is_same_list is_same_enumitem ei.eitems ei'.eitems env
+
+and is_same_fieldinfo fi fi' env =
+ (* we don't compare names: it's the order in which they appear in the
+ definition of the aggregate that counts. *)
+ fi.forder = fi'.forder &&
+ is_same_type fi.ftype fi'.ftype env &&
+ is_same_opt (fun x y _ -> x = y) fi.fbitfield fi'.fbitfield env &&
+ Cil_datatype.Attributes.equal fi.fattr fi'.fattr
+
+and is_same_enumitem ei ei' env = is_same_exp ei.eival ei'.eival env
+
+and is_same_formal (_,t,a) (_,t',a') env =
+ is_same_type t t' env && Cil_datatype.Attributes.equal a a'
+
+and is_same_compound_init (o,i) (o',i') env =
+ is_same_offset o o' env && is_same_init i i' env
+
+and is_same_init i i' env =
+ match i, i' with
+ | SingleInit e, SingleInit e' -> is_same_exp e e' env
+ | CompoundInit (t,l), CompoundInit (t', l') ->
+ is_same_type t t' env &&
+ (is_same_list is_same_compound_init) l l' env
+ | (SingleInit _ | CompoundInit _), _ -> false
+
+and is_same_initinfo i i' env = is_same_opt is_same_init i.init i'.init env
+
+and is_same_local_init i i' env =
+ match i, i' with
+ | AssignInit i, AssignInit i' ->
+ if is_same_init i i' env then `Same_body
+ else `Body_changed
+ | (ConsInit(c,args,Plain_func), ConsInit(c',args',Plain_func))
+ | (ConsInit(c,args,Constructor),ConsInit(c',args',Constructor)) ->
+ if is_same_varinfo c c' env &&
+ is_same_list is_same_exp args args' env
+ then begin
+ match gfun_correspondance c env with
+ | `Partial _ | `Not_present -> `Callees_changed
+ | `Same _ -> `Same_body
+ end else `Body_changed
+ | (AssignInit _| ConsInit _), _ -> `Body_changed
+
+and is_same_constant c c' env =
+ match c,c' with
+ | CEnum ei, CEnum ei' ->
+ (match enumitem_correspondance ei env with
+ | `Same ei'' -> Cil_datatype.Enumitem.equal ei' ei''
+ | `Not_present -> false)
+ | CEnum _, _ | _, CEnum _ -> false
+ | (CInt64 _ | CStr _ | CWStr _ | CChr _ | CReal _), _ ->
+ Cil_datatype.Constant.equal c c'
+
+and is_same_exp e e' env =
+ match e.enode, e'.enode with
+ | Const c, Const c' -> is_same_constant c c' env
+ | Lval lv, Lval lv' -> is_same_lval lv lv' env
+ | SizeOf t, SizeOf t' -> is_same_type t t' env
+ | SizeOfE e, SizeOfE e' -> is_same_exp e e' env
+ | SizeOfStr s, SizeOfStr s' -> String.length s = String.length s'
+ | AlignOf t, AlignOf t' -> is_same_type t t' env
+ | AlignOfE e, AlignOfE e' -> is_same_exp e e' env
+ | UnOp(op,e,t), UnOp(op',e',t') ->
+ Unop.equal op op' && is_same_exp e e' env && is_same_type t t' env
+ | BinOp(op,e1,e2,t), BinOp(op',e1',e2',t') ->
+ Binop.equal op op' && is_same_exp e1 e1' env && is_same_exp e2 e2' env
+ && is_same_type t t' env
+ | CastE(t,e), CastE(t',e') -> is_same_type t t' env && is_same_exp e e' env
+ | AddrOf lv, AddrOf lv' -> is_same_lval lv lv' env
+ | StartOf lv, StartOf lv' -> is_same_lval lv lv' env
+ | (Const _ | Lval _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
+ | AlignOfE _ | UnOp _ | BinOp _ | CastE _ | AddrOf _ | StartOf _),_-> false
+
+and is_same_lval lv lv' env =
+ is_same_pair is_same_lhost is_same_offset lv lv' env
+
+and is_same_lhost h h' env =
+ match h, h' with
+ | Var vi, Var vi' -> is_matching_varinfo vi vi' env
+ | Mem p, Mem p' -> is_same_exp p p' env
+ | (Var _ | Mem _), _ -> false
+
+and is_matching_varinfo vi vi' env =
+ if vi.vglob then begin
+ match gvar_correspondance vi env with
+ | `Not_present -> false
+ | `Same vi'' -> Cil_datatype.Varinfo.equal vi' vi''
+ end else begin
+ try
+ let vi'' = Cil_datatype.Varinfo.Map.find vi env.local_vars in
+ Cil_datatype.Varinfo.equal vi' vi''
+ with Not_found ->
+ Kernel.fatal "Unbound variable %a in AST diff"
+ Cil_datatype.Varinfo.pretty vi
+ end
+
+and is_same_offset o o' env =
+ match o, o' with
+ | NoOffset, NoOffset -> true
+ | Field (i,o), Field(i',o') ->
+ is_matching_fieldinfo i i' && is_same_offset o o' env
+ | Index(i,o), Index(i',o') ->
+ is_same_exp i i' env && is_same_offset o o' env
+ | (NoOffset | Field _ | Index _), _ -> false
+
+and is_same_extended_asm a a' env =
+ let is_same_out (_,c,l) (_,c',l') env =
+ Datatype.String.equal c c' && is_same_lval l l' env
+ and is_same_in (_,c,e) (_,c',e') env =
+ Datatype.String.equal c c' && is_same_exp e e' env
+ in
+ let res =
+ is_same_list is_same_out a.asm_outputs a'.asm_outputs env &&
+ is_same_list is_same_in a.asm_inputs a'.asm_inputs env &&
+ is_same_list
+ (fun s1 s2 _ -> Datatype.String.equal s1 s2)
+ a.asm_clobbers a'.asm_clobbers env
+ &&
+ List.length a.asm_gotos = List.length a'.asm_gotos
+ in
+ let bind s s' env =
+ (true, { env with goto_targets = (!s,!s') :: env.goto_targets})
+ in
+ (res, env) &&& is_same_list_env bind a.asm_gotos a'.asm_gotos
+
+and is_same_instr i i' env: body_correspondance*is_same_env =
+ match i, i' with
+ | Set(lv,e,_), Set(lv',e',_) ->
+ if is_same_lval lv lv' env && is_same_exp e e' env then
+ `Same_body, env
+ else
+ `Body_changed, env
+ | Call(lv,f,args,_), Call(lv',f',args',_) ->
+ if is_same_opt is_same_lval lv lv' env &&
+ is_same_list is_same_exp args args' env
+ then begin
+ match f.enode, f'.enode with
+ | Lval(Var f,NoOffset), Lval(Var f', NoOffset) ->
+ (match gfun_correspondance f env with
+ | `Partial _ | `Not_present -> `Callees_changed, env
+ | `Same f'' ->
+ if Cil_datatype.Varinfo.equal f' (Kf.get_vi f'') then
+ `Same_body, env
+ else
+ `Callees_changed, env)
+ | _ -> `Callees_changed, env
+ (* by default, we consider that indirect call might have changed *)
+ end else `Body_changed, env
+ | Local_init(v,i,_), Local_init(v',i',_) ->
+ if is_same_varinfo v v' env then begin
+ let env = add_locals [v] [v'] env in
+ let res = is_same_local_init i i' env in
+ res, env
+ end else `Body_changed, env
+ | Asm(a,c,e,_), Asm(a',c',e',_) ->
+ let res =
+ Cil_datatype.Attributes.equal a a' &&
+ is_same_list (fun s1 s2 _ -> Datatype.String.equal s1 s2) c c' env
+ in
+ let (res,env) = (res,env) &&& is_same_opt_env is_same_extended_asm e e' in
+ if res then `Same_body, env else `Body_changed, env
+ | Skip _, Skip _ -> `Same_body, env
+ | Code_annot _, Code_annot _ ->
+ (* should not be present in normalized AST *)
+ Kernel.fatal "Unexpected Code_annot instruction in normalized AST"
+ | _ -> `Body_changed, env
+
+and is_same_instr_list l l' env =
+ match l, l' with
+ | [], [] -> `Same_body, env
+ | [], _ | _, [] -> `Body_changed, env
+ | i::tl, i'::tl' ->
+ is_same_instr i i' env &&> is_same_instr_list tl tl'
+
+and same_switch_labels l l' env =
+ let l = List.filter Cil.is_case_label l in
+ let l' = List.filter Cil.is_case_label l' in
+ let is_same_label lab lab' =
+ match lab, lab' with
+ | (Label _ as l, _) | (_, (Label _ as l)) ->
+ Kernel.fatal "Label %a should have been filtered beforehand"
+ Printer.pp_label l
+ | Case(e,_), Case(e', _) -> is_same_exp e e' env
+ | Default _, Default _ -> true
+ | (Case _ | Default _), _ -> false
+ in
+ let exist_same_label l lab = List.exists (is_same_label lab) l in
+ (* it is not sufficient to ensure that any case label present in the original
+ also exists in the new AST: we also must check that no new label was
+ introduced that would change the cfg for this case.
+ *)
+ List.for_all (exist_same_label l') l &&
+ List.for_all (exist_same_label l) l'
+
+and is_same_stmt s s' env =
+ let selection =
+ State_selection.with_codependencies Annotations.code_annot_state
+ in
+ let annots =
+ Project.on ~selection (Orig_project.get()) Annotations.code_annot s
+ in
+ let annots' = Annotations.code_annot s' in
+ let annot_res = is_same_list is_same_code_annotation annots annots' env in
+ let code_res, env =
+ if s.ghost = s'.ghost && Cil_datatype.Attributes.equal s.sattr s'.sattr &&
+ same_switch_labels s.labels s'.labels env
+ then
+ begin
+ match s.skind,s'.skind with
+ | Instr i, Instr i' -> is_same_instr i i' env
+ | Return (r,_), Return(r', _) ->
+ if is_same_opt is_same_exp r r' env then `Same_body, env
+ else `Body_changed, env
+ | Goto (s,_), Goto(s',_) ->
+ `Same_body, { env with goto_targets = (!s,!s') :: env.goto_targets }
+ | Break _, Break _ -> `Same_body, env
+ | Continue _, Continue _ -> `Same_body, env
+ | If(e,b1,b2,_), If(e',b1',b2',_) ->
+ if is_same_exp e e' env then begin
+ is_same_block b1 b1' env &&>
+ is_same_block b2 b2'
+ end else `Body_changed, env
+ | Switch(e,b,_,_), Switch(e',b',_,_) ->
+ if is_same_exp e e' env then begin
+ is_same_block b b' env
+ end else `Body_changed, env
+ | Loop(_,b,_,_,_), Loop(_,b',_,_,_) ->
+ is_same_block b b' env
+ | Block b, Block b' ->
+ is_same_block b b' env
+ | UnspecifiedSequence l, UnspecifiedSequence l' ->
+ let b = Cil.block_from_unspecified_sequence l in
+ let b' = Cil.block_from_unspecified_sequence l' in
+ is_same_block b b' env
+ | Throw (e,_), Throw (e',_) ->
+ if is_same_opt (is_same_pair is_same_exp is_same_type) e e' env then
+ `Same_body, env
+ else `Body_changed, env
+ | TryCatch (b,c,_), TryCatch(b',c',_) ->
+ let rec is_same_catch_list l l' env =
+ match l, l' with
+ | [], [] -> `Same_body, env
+ | [],_ | _, [] -> `Body_changed, env
+ | (bind, b) :: tl, (bind', b') :: tl' ->
+ is_same_binder bind bind' env &&>
+ is_same_block b b' &&>
+ is_same_catch_list tl tl'
+ in
+ is_same_block b b' env &&> is_same_catch_list c c'
+ | TryFinally(b1,b2,_), TryFinally(b1',b2',_) ->
+ is_same_block b1 b1' env &&>
+ (is_same_block b2 b2')
+ | TryExcept(b1,(h,e),b2,_), TryExcept(b1',(h',e'),b2',_) ->
+ if is_same_exp e e' env then begin
+ is_same_block b1 b1' env &&>
+ is_same_instr_list h h' &&>
+ is_same_block b2 b2'
+ end else `Body_changed, env
+ | _ -> `Body_changed, env
+ end else `Body_changed, env
+ in
+ let res = make_correspondance s' annot_res code_res in
+ Stmt.add s res; code_res, env
+
+(* is_same_block will return its modified environment in order
+ to update correspondance table with respect to locals, in case
+ the body of the enclosing function is unchanged. *)
+and is_same_block b b' env =
+ let local_decls = List.filter (fun x -> not x.vdefined) b.blocals in
+ let local_decls' = List.filter (fun x -> not x.vdefined) b'.blocals in
+ if is_same_list is_same_varinfo b.bstatics b'.bstatics env &&
+ Cil_datatype.Attributes.equal b.battrs b'.battrs
+ then begin
+ let res, env = is_same_list_env varinfo_env local_decls local_decls' env in
+ if res then begin
+ add_statics b.bstatics b'.bstatics;
+ let rec is_same_stmts l l' env =
+ match l, l' with
+ | [], [] -> `Same_body,env
+ | [], _ | _, [] -> `Body_changed, env
+ | s :: tl, s' :: tl' ->
+ is_same_stmt s s' env &&> (is_same_stmts tl tl')
+ in
+ is_same_stmts b.bstmts b'.bstmts env
+ end else `Body_changed, env
+ end else `Body_changed, env
+
+and is_same_binder b b' env =
+ match b, b' with
+ | Catch_exn(v,conv), Catch_exn(v', conv') ->
+ if is_same_varinfo v v' env then begin
+ let env = add_locals [v] [v'] env in
+ let rec is_same_conv l l' env =
+ match l, l' with
+ | [], [] -> `Same_body, env
+ | [], _ | _, [] -> `Body_changed, env
+ | (v,b)::tl, (v',b')::tl' ->
+ if is_same_varinfo v v' env then begin
+ let env = add_locals [v] [v'] env in
+ is_same_block b b' env &&>
+ (is_same_conv tl tl')
+ end else `Body_changed, env
+ in
+ is_same_conv conv conv' env
+ end else `Body_changed, env
+ | Catch_all, Catch_all -> `Same_body, env
+ | (Catch_exn _ | Catch_all), _ -> `Body_changed, env
+
+(* correspondance of formals is supposed to have already been checked,
+ and formals mapping to have been put in the local env
+*)
+and is_same_fundec f f' env: body_correspondance =
+ (* The goto_targets field of [env] accumulates visited goto targets to be
+ verified after the function body. If the given environment is not empty,
+ resets this field for this function. *)
+ let env = { env with goto_targets = [] } in
+ let res, env =
+ is_same_block f.sbody f'.sbody env &&>
+ check_goto_targets
+ in
+ (* Since we add the locals only if the body is the same,
+ we have explored all nodes, and added all locals bindings.
+ Otherwise, is_same_block would have returned `Body_changed.
+ Hence [Not_found] cannot be raised. *)
+ let add_local v =
+ let v' = Cil_datatype.Varinfo.Map.find v env.local_vars in
+ Varinfo.add v (`Same v')
+ in
+ (match res with
+ | `Same_body | `Callees_changed ->
+ List.iter add_local f.slocals
+ | `Body_changed -> ());
+ res
+
+and is_same_varinfo vi vi' env =
+ is_same_type vi.vtype vi'.vtype env &&
+ Cil_datatype.Attributes.equal vi.vattr vi'.vattr
+
+and varinfo_env vi vi' env =
+ if is_same_varinfo vi vi' env then true, add_locals [vi] [vi'] env
+ else false, env
+
+and is_same_logic_var lv lv' env =
+ is_same_logic_type lv.lv_type lv'.lv_type env &&
+ Cil_datatype.Attributes.equal lv.lv_attr lv'.lv_attr
+
+and logic_vars_env l l' env =
+ if is_same_list is_same_logic_var l l' env then
+ true, add_logic_vars l l' env
+ else
+ false, env
+
+and find_candidate_logic_var ?loc:_loc lv env =
+ let candidates = Logic_env.find_all_logic_functions lv.lv_name in
+ match List.find_opt (fun li -> li.l_profile = []) candidates with
+ | None -> None
+ | Some li ->
+ if is_same_logic_var lv li.l_var_info env then
+ Some li.l_var_info
+ else None
+
+(* because of overloading, we have to check for a corresponding profile,
+ leading to potentially recursive calls to is_same_* functions. *)
+and find_candidate_logic_info ?loc:_loc li env =
+ let candidates = Logic_env.find_all_logic_functions li.l_var_info.lv_name in
+ let find_one li' =
+ let res, env = logic_type_vars_env li.l_tparams li'.l_tparams env in
+ res && is_same_list is_same_logic_var li.l_profile li'.l_profile env
+ && is_same_opt is_same_logic_type li.l_type li'.l_type env
+ in
+ List.find_opt find_one candidates
+
+and find_candidate_model_info ?loc:_loc mi env =
+ let candidates = Logic_env.find_all_model_fields mi.mi_name in
+ let find_one mi' =
+ is_same_type mi.mi_base_type mi'.mi_base_type env
+ in
+ List.find_opt find_one candidates
+
+and typeinfo_correspondance ?loc ti env =
+ let add ti =
+ match find_candidate_type ?loc ti with
+ | None -> `Not_present
+ | Some ti' ->
+ let res = is_same_type ti.ttype ti'.ttype env in
+ if res then `Same ti' else `Not_present
+ in
+ Typeinfo.memo add ti
+
+and compinfo_correspondance ?loc ci env =
+ let add ci =
+ match find_candidate_compinfo ?loc ci with
+ | None -> `Not_present
+ | Some ci' ->
+ let env' =
+ {env with compinfo = Cil_datatype.Compinfo.Map.add ci ci' env.compinfo}
+ in
+ let res = is_same_compinfo ci ci' env' in
+ if res then begin
+ (match ci.cfields, ci'.cfields with
+ | Some fl, Some fl' ->
+ (* by definition, if is_same_compinfo returns true,
+ we have the same number of fields in ci and ci'. *)
+ List.iter2 (fun fi fi' -> Fieldinfo.add fi (`Same fi')) fl fl'
+ | _ -> ());
+ `Same ci'
+ end else begin
+ (* fields are considered different, even if it might be possible
+ to consider that the beginning of the struct hasn't changed. *)
+ (match ci.cfields with
+ | Some fl -> List.iter (fun fi -> Fieldinfo.add fi `Not_present) fl
+ | None -> ());
+ `Not_present
+ end
+ in
+ match Cil_datatype.Compinfo.Map.find_opt ci env.compinfo with
+ | Some ci' -> `Same ci'
+ | None -> Compinfo.memo add ci
+
+and enuminfo_correspondance ?loc ei env =
+ let add ei =
+ match find_candidate_enuminfo ?loc ei with
+ | None -> `Not_present
+ | Some ei' ->
+ if is_same_enuminfo ei ei' env then begin
+ (* add items correspondance. By definition, we have
+ the same number of items here. *)
+ List.iter2 (fun ei ei' -> Enumitem.add ei (`Same ei'))
+ ei.eitems ei'.eitems;
+ `Same ei'
+ end else begin
+ (* consider that all items are different.
+ Might be refined at some point. *)
+ List.iter (fun ei -> Enumitem.add ei `Not_present) ei.eitems;
+ `Not_present
+ end
+ in
+ Enuminfo.memo add ei
+
+and enumitem_correspondance ?loc:_loc ei _env = Enumitem.find ei
+
+and gvar_correspondance ?loc vi env =
+ let add vi =
+ match find_candidate_varinfo ?loc vi Cil_types.VGlobal with
+ | None when Cil.isFunctionType vi.vtype ->
+ begin
+ match gfun_correspondance ?loc vi env with
+ | `Same kf' -> `Same (Kf.get_vi kf')
+ | `Partial(kf',_) ->
+ (* a partial match at kf level is still the
+ identity for the underlying varinfo *)
+ `Same (Kf.get_vi kf')
+ | `Not_present -> `Not_present
+ end
+ | None -> `Not_present
+ | Some vi' ->
+ if is_same_varinfo vi vi' env
+ then
+ let selection = State_selection.singleton Globals.Vars.self in
+ let init =
+ Project.on ~selection (Orig_project.get()) Globals.Vars.find vi
+ in
+ let init' = Globals.Vars.find vi' in
+ let res = is_same_initinfo init init' env in
+ if res then `Same vi' else `Not_present
+ else `Not_present
+ in
+ Varinfo.memo add vi
+
+and gfun_correspondance ?loc vi env =
+ (* NB: we also take care of the correspondance between the underlying varinfo,
+ in case we have to refer to it directly, e.g. as an AddrOf argument.
+ *)
+ let kf = get_original_kf vi in
+ let add kf =
+ match find_candidate_func ?loc kf with
+ | None -> Varinfo.add vi `Not_present; `Not_present
+ | Some kf' ->
+ let formals = Kf.get_formals kf in
+ let formals' = Kf.get_formals kf' in
+ let res, env =
+ (is_same_type (Kf.get_return_type kf) (Kf.get_return_type kf') env, env)
+ &&& is_same_list_env varinfo_env formals formals'
+ in
+ if res then begin
+ (* from a variable point of view, e.g. if we take its address,
+ they are similar *)
+ Varinfo.add vi (`Same (Kf.get_vi kf'));
+ (* we only add formals to global correspondance tables if some
+ part of the kf is unchanged (otherwise, we can't reuse information
+ about the formals anyways). Hence, we only add them into the local
+ env for now. *)
+ let env =
+ { env with kernel_function = Kf.Map.add kf kf' env.kernel_function }
+ in
+ let same_spec = is_same_funspec kf.spec kf'.spec env in
+ let same_body =
+ match (Kf.has_definition kf, Kf.has_definition kf') with
+ | false, false -> `Same_body
+ | false, true | true, false -> `Body_changed
+ | true, true ->
+ is_same_fundec (Kf.get_definition kf) (Kf.get_definition kf') env
+ in
+ let res = make_correspondance kf' same_spec same_body in
+ (match res with
+ | `Not_present -> ()
+ | `Same _ | `Partial _ -> formals_correspondance formals formals');
+ res
+ end else begin
+ (* signatures do not match, we consider that pointers
+ are not equivalent. *)
+ Varinfo.add vi `Not_present;
+ `Not_present
+ end
+ in
+ match Kf.Map.find_opt kf env.kernel_function with
+ | Some kf' -> `Same kf'
+ | None -> Kernel_function.memo add kf
+
+and is_matching_logic_info li li' env =
+ match Cil_datatype.Logic_info.Map.find_opt li env.logic_info with
+ | None ->
+ (match Logic_info.find li with
+ | `Not_present -> false
+ | `Same li'' -> Cil_datatype.Logic_info.equal li' li''
+ | exception Not_found ->
+ begin
+ let res = logic_info_correspondance li env in
+ Logic_info.add li res;
+ match res with
+ | `Not_present -> false
+ | `Same li'' -> Cil_datatype.Logic_info.equal li' li''
+ end)
+ | Some li'' -> Cil_datatype.Logic_info.equal li' li''
+
+and logic_info_correspondance ?loc li env =
+ let add li =
+ match find_candidate_logic_info ?loc li env with
+ | None -> `Not_present
+ | Some li' ->
+ let env =
+ { env with
+ logic_info=Cil_datatype.Logic_info.Map.add li li' env.logic_info }
+ in
+ let res = is_same_logic_info li li' env in
+ if res then begin
+ logic_prms_correspondance li.l_profile li'.l_profile;
+ `Same li'
+ end else `Not_present
+ in
+ match Cil_datatype.Logic_info.Map.find_opt li env.logic_info with
+ | Some li' -> `Same li'
+ | None -> Logic_info.memo add li
+
+and is_matching_logic_ctor c c' env =
+ match Logic_ctor_info.find c with
+ | `Not_present -> false
+ | `Same c'' -> Cil_datatype.Logic_ctor_info.equal c' c''
+ | exception Not_found ->
+ let ty = c.ctor_type in
+ let res = logic_type_correspondance ty env in
+ Logic_type_info.add ty res;
+ if not (Logic_ctor_info.mem c) then
+ Kernel.fatal "Unbound logic type constructor %a in AST diff"
+ Cil_datatype.Logic_ctor_info.pretty c;
+ is_matching_logic_ctor c c' env
+
+and is_matching_logic_type_info t t' env =
+ match Logic_type_info.find t with
+ | `Not_present -> false
+ | `Same t'' -> Cil_datatype.Logic_type_info.equal t' t''
+ | exception Not_found ->
+ (match Cil_datatype.Logic_type_info.Map.find_opt t env.logic_type_info with
+ | Some t'' -> Cil_datatype.Logic_type_info.equal t' t''
+ | None ->
+ let res = logic_type_correspondance t env in
+ Logic_type_info.add t res;
+ (match res with
+ | `Same t'' -> Cil_datatype.Logic_type_info.equal t' t''
+ | `Not_present -> false))
+
+and logic_type_correspondance ?loc ti env =
+ let add ti =
+ match find_candidate_logic_type ?loc ti with
+ | None -> `Not_present
+ | Some ti' ->
+ let env =
+ { env with
+ logic_type_info =
+ Cil_datatype.Logic_type_info.Map.add ti ti' env.logic_type_info }
+ in
+ let res = is_same_logic_type_info ti ti' env in
+ (* In case of a sum type, the constructors table
+ is updated by is_same_logic_type_info. *)
+ if res then `Same ti' else `Not_present
+ in
+ match Cil_datatype.Logic_type_info.Map.find_opt ti env.logic_type_info with
+ | Some ti' -> `Same ti'
+ | None -> Logic_type_info.memo add ti
+
+let model_info_correspondance ?loc mi =
+ let add mi =
+ match find_candidate_model_info ?loc mi empty_env with
+ | None -> `Not_present
+ | Some mi' ->
+ let res = is_same_model_info mi mi' empty_env in
+ if res then `Same mi' else `Not_present
+ in
+ Model_info.memo add mi
+
+let rec gannot_correspondance =
+ function
+ | Dfun_or_pred (li,loc) ->
+ ignore (logic_info_correspondance ~loc li empty_env)
+
+ | Dvolatile _ -> ()
+ (* reading and writing function themselves will be checked elsewhere. *)
+
+ | Daxiomatic(_,l,_,_) ->
+ List.iter gannot_correspondance l
+ | Dtype (ti,loc) -> ignore (logic_type_correspondance ~loc ti empty_env)
+ | Dlemma _ -> ()
+ (* TODO: we currently do not have any appropriate structure for
+ storing information about lemmas. *)
+ | Dinvariant(li, loc) ->
+ ignore (logic_info_correspondance ~loc li empty_env)
+ | Dtype_annot(li,loc) ->
+ ignore (logic_info_correspondance ~loc li empty_env)
+ | Dmodel_annot (mi,loc) ->
+ ignore (model_info_correspondance ~loc mi)
+ | Dextended _ -> ()
+(* TODO: provide mechanism for extension themselves
+ to give relevant information. *)
+
+let global_correspondance g =
+ match g with
+ | GType (ti,loc) -> ignore (typeinfo_correspondance ~loc ti empty_env)
+ | GCompTag(ci,loc) | GCompTagDecl(ci,loc) ->
+ ignore (compinfo_correspondance ~loc ci empty_env)
+ | GEnumTag(ei,loc) | GEnumTagDecl(ei,loc) ->
+ ignore (enuminfo_correspondance ~loc ei empty_env)
+ | GVar(vi,_,loc) | GVarDecl(vi,loc) ->
+ ignore (gvar_correspondance ~loc vi empty_env)
+ | GFunDecl(_,vi,loc) -> ignore (gfun_correspondance ~loc vi empty_env)
+ | GFun(f,loc) -> ignore (gfun_correspondance ~loc f.svar empty_env)
+ | GAnnot (g,_) -> gannot_correspondance g
+ | GAsm _ | GPragma _ | GText _ -> ()
+
+
+let compare_ast () =
+ let prj = Orig_project.get () in
+ let ast = Project.on prj Ast.get () in
+ Cil.iterGlobals ast global_correspondance
+
+let compare_from_prj prj =
+ Orig_project.set prj;
+ compare_ast ()
+
+let prepare_project () =
+ if Kernel.AstDiff.get () then begin
+ let orig = Project.create_by_copy ~last:false
+ ("orig_" ^ Project.get_name (Project.current()))
+ in
+ Orig_project.set orig
+ end
+
+let () = Cmdline.run_after_configuring_stage prepare_project
+
+let compute_diff _ =
+ if Kernel.AstDiff.get () then begin
+ Ast.compute (); compare_ast ()
+ end
+
+let () = Cmdline.run_after_setting_files compute_diff
diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f40887842305a56d7080ae01b67af66146018c0d
--- /dev/null
+++ b/src/kernel_services/ast_queries/ast_diff.mli
@@ -0,0 +1,127 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Compute diff information from an existing project.
+
+ @since Frama-C+dev
+*)
+
+open Cil_types
+
+(** the original project from which a diff is computed. *)
+module Orig_project: State_builder.Option_ref with type data = Project.t
+
+(** possible correspondances between new items and original ones. *)
+type 'a correspondance =
+ [ `Same of 'a (** symbol with identical definition has been found. *)
+ | `Not_present (** no correspondance *)
+ ]
+
+(** for kernel function, we are a bit more precise than a yes/no answer.
+ More precisely, we check whether a function has the same spec,
+ the same body, and whether its callees have changed (provided
+ the body itself is identical, otherwise, there's no point in checking
+ the callees.
+*)
+type partial_correspondance =
+ [ `Spec_changed (** body and callees haven't changed *)
+ | `Body_changed (** spec hasn't changed *)
+ | `Callees_changed (** spec and body haven't changed *)
+ | `Callees_spec_changed (** body hasn't changed *)
+ ]
+
+type 'a code_correspondance =
+ [ 'a correspondance
+ | `Partial of 'a * partial_correspondance
+ ]
+
+module type Correspondance_table = sig
+ include State_builder.Hashtbl
+ val pretty_data: Format.formatter -> data -> unit
+end
+
+(** varinfos correspondances *)
+module Varinfo:
+ Correspondance_table
+ with type key = varinfo and type data = varinfo correspondance
+
+module Compinfo:
+ Correspondance_table
+ with type key = compinfo and type data = compinfo correspondance
+
+module Enuminfo:
+ Correspondance_table
+ with type key = enuminfo and type data = enuminfo correspondance
+
+module Enumitem:
+ Correspondance_table
+ with type key = enumitem and type data = enumitem correspondance
+
+module Typeinfo:
+ Correspondance_table
+ with type key = typeinfo and type data = typeinfo correspondance
+
+module Stmt:
+ Correspondance_table
+ with type key = stmt and type data = stmt code_correspondance
+
+module Logic_info:
+ Correspondance_table
+ with type key = logic_info and type data = logic_info correspondance
+
+module Logic_type_info:
+ Correspondance_table
+ with type key = logic_type_info and type data = logic_type_info correspondance
+
+module Logic_ctor_info:
+ Correspondance_table
+ with type key = logic_ctor_info and type data = logic_ctor_info correspondance
+
+module Fieldinfo:
+ Correspondance_table
+ with type key = fieldinfo and type data = fieldinfo correspondance
+
+module Model_info:
+ Correspondance_table
+ with type key = model_info and type data = model_info correspondance
+
+module Logic_var:
+ Correspondance_table
+ with type key = logic_var and type data = logic_var correspondance
+
+module Kernel_function:
+ Correspondance_table
+ with type key = kernel_function
+ and type data = kernel_function code_correspondance
+
+module Fundec:
+ Correspondance_table
+ with type key = fundec and type data = fundec correspondance
+
+(** performs a comparison of AST between the current and the original
+ project, which must have been set beforehand.
+*)
+val compare_ast: unit-> unit
+
+(** [compare_from_prj prj] sets [prj] as the original project
+ and fill the tables. *)
+val compare_from_prj: Project.t -> unit
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index bbee2f5bcc4a4bd554a6836df84f1fbdcca20f1e..31b139bdd6bd451ebf2f4fedcb10d11c8cb89481 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -737,7 +737,7 @@ module Label = struct
let reprs =
[ Label("", Location.unknown, false); Default Location.unknown ]
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt l = !pretty_ref fmt l
let varname = Datatype.undefined
let hash = function
| Default _ -> 7
@@ -1334,7 +1334,7 @@ module Builtin_logic_info = struct
let equal i1 i2 = i1.bl_name = i2.bl_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt li = !pretty_ref fmt li
let varname = Datatype.undefined
end)
end
@@ -1352,7 +1352,7 @@ module Logic_type_info = struct
let hash t = Hashtbl.hash t.lt_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt lt = !pretty_ref fmt lt
let varname = Datatype.undefined
end)
end
@@ -1372,7 +1372,7 @@ module Logic_ctor_info = struct
let hash t = Hashtbl.hash t.ctor_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt c = !pretty_ref fmt c
let varname = Datatype.undefined
end)
end
@@ -1387,7 +1387,7 @@ module Initinfo = struct
{ init = None } ::
List.map (fun t -> { init = Some (CompoundInit(t, [])) }) Typ.reprs
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt i = !pretty_ref fmt i
let varname = Datatype.undefined
end)
end
@@ -1413,7 +1413,7 @@ module Logic_info = struct
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt li = !pretty_ref fmt li
let varname _ = "logic_varinfo"
end)
end
@@ -1498,7 +1498,7 @@ module Logic_info_structural = struct
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt li = !Logic_info.pretty_ref fmt li
let varname _ = "logic_varinfo"
end)
end
@@ -2085,7 +2085,7 @@ module Logic_constant = struct
let hash = hash_logic_constant
let copy = Datatype.undefined
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt lc = !pretty_ref fmt lc
let varname _ = "lconst"
end)
end
@@ -2129,7 +2129,7 @@ module Identified_term = struct
{ it_id = x.it_id; it_content = Term.copy x.it_content }
let hash x = x.it_id
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt t = !pretty_ref fmt t
let varname _ = "id_term"
end)
end
@@ -2154,7 +2154,7 @@ module Term_lhost = struct
let hash = hash_fct hash_tlhost
let copy = Datatype.undefined
let internal_pretty_code = Datatype.undefined
- let pretty = !pretty_ref
+ let pretty fmt h = !pretty_ref fmt h
let varname = Datatype.undefined
end)
end
@@ -2658,7 +2658,7 @@ module Fundec = struct
let equal v1 v2 = v1.svar.vid = v2.svar.vid
let rehash = Datatype.identity
let copy = Datatype.undefined
- let pretty = Datatype.undefined
+ let pretty fmt f = !pretty_ref fmt f
let internal_pretty_code = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 79d3b8c13ee0971dcb5998151e3518a3ed9e62bf..057ba6786496350a2e133b771f3ee7e68feccc7f 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -821,6 +821,17 @@ module EagerLoadSources =
in memory"
end)
+let () = Parameter_customize.set_group inout_source
+let () = Parameter_customize.do_not_projectify ()
+module AstDiff =
+ False
+ (struct
+ let option_name = "-ast-diff"
+ let module_name = "AstDiff"
+ let help = "creates a new project and computes a diff of the AST \
+ from the current one"
+ end)
+
(* ************************************************************************* *)
(** {2 Save/Load} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c0c5520fecd00d44fd7af902841648e080d9164e..28f166f0a9e829e848fabb05321a332484a2a476 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -334,6 +334,9 @@ module CodeOutput : sig
val output: (Format.formatter -> unit) -> unit
end
+(** Behavior of option "-ast-diff" *)
+module AstDiff: Parameter_sig.Bool
+
(** Behavior of option "-add-symbolic-path"
@since Neon-20140301
@modify 23.0-Vanadium inversed argument order (now uses path:name) *)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index c0070248e9f622d3f4a594834412f326ffa02341..35da51d54ec8b3402b08cfd97bf2c2e572d07d2c 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -132,7 +132,14 @@ let insert base path_name =
Instead of forcing the user to always provide resolved paths, we
currently choose to never resolve them.
Note that, in rare situations (e.g. some Docker images), PWD does not
- exist in the environment, so in that case, we fallback to Sys.getcwd. *)
+ exist in the environment, so in that case, we fallback to Sys.getcwd.
+
+ REMARK[LC]: when the Frama-C binary is directly invoked by Node without
+ going through a shell script wrapper like ./bin/frama-c, the environment
+ variable "PWD" is _no more_ synchronized with Sys.getcwd.
+ This problem has been solved in `Dome.spawn()` by forcing the `PWD`
+ environement variable accordingly.
+*)
let cwd = insert dummy (try Sys.getenv "PWD" with Not_found -> Sys.getcwd ())
type existence =
diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml
index 07056a2b7f00edc1f7a00a5b171f084d91a4b140..db672f0228d6a349ca46f52ba1e7e3809087b2b7 100644
--- a/src/libraries/utils/wto.ml
+++ b/src/libraries/utils/wto.ml
@@ -153,8 +153,12 @@ module Make(N:sig
this loop with the lowest level. This vertex is also the deepest in the
stack and the neareast vertex from the root that is below [vertex] in
the spanning tree built by the DFS);
- - [partition] is returned completed. *)
- let rec visit ~pref state vertex partition =
+ - [partition] is returned completed.
+
+ A tail-recursive implementation of this function is now used to avoid
+ stack overflow errors on very large functions. This function is kept
+ for documentation purposes, as it is simpler and more readable. *)
+ let rec _visit ~pref state vertex partition =
match DFN.find state.dfn vertex with
(* The vertex is already in the partition *)
| Invisible -> NoLoop, partition (* skip it *)
@@ -171,7 +175,7 @@ module Make(N:sig
(* Visit all its successors *)
let succs = state.succs vertex in
let (loop,partition) = List.fold_left (fun (loop,partition) succ ->
- let (loop',partition) = visit ~pref state succ partition in
+ let (loop',partition) = _visit ~pref state succ partition in
let loop = min_loop loop loop' in
(loop,partition)
) (NoLoop,partition) succs
@@ -211,7 +215,7 @@ module Make(N:sig
(* Restart the component analysis *)
let component = List.fold_left
(fun component succ ->
- let (loop,component) = visit ~pref state succ component in
+ let (loop,component) = _visit ~pref state succ component in
(* Since we reset the component we should have no loop *)
assert (loop = NoLoop);
component
@@ -224,12 +228,123 @@ module Make(N:sig
be added during the second visit of the SCC. *)
(loop,partition)
+
+ (* Types for the tail-recursive function of [visit]. *)
+
+ (* Whether to apply [min_loop] at the end of the visit of a vertex. *)
+ type kind = Default | MinLoop
+
+ (* [visit] contains two recursive calls; its tail-recursive version is split
+ into several steps accordingly. For the visit of a vertex, this type
+ indicates the step that must be done. *)
+ type step =
+ | Start of kind
+ (* Starts the visit of a vertex. If [kind] = [MinLoop], then apply
+ [min_loop] between the previous and the resulting loop. *)
+ | Continue
+ (* Resumes the visit of a vertex after the first recursive call. *)
+ | End of N.t partition
+ (* Ends the visit of a vertex after the second recursive call. *)
+ | Min_loop of loop
+ (* Apply [Min_loop] between [loop] (from the previous result) and the
+ current loop. *)
+
+ (* The list of steps that must be done, with their related vertex. It starts
+ with [init, Start Default] and grows for each original recursive call. *)
+ type continuation = (N.t * step) list
+
+ (** Tail-recursive version of the [visit] function above. *)
+ let tail_recursive_visit ~pref state vertex partition =
+ (* Visit according to the next step to be done. *)
+ let rec visit (cont: continuation) (loop, partition) =
+ match cont with
+ | [] -> loop, partition
+ | (vertex, step) :: cont ->
+ match step with
+ | Start kind ->
+ let cont =
+ if kind = MinLoop then (vertex, Min_loop loop) :: cont else cont
+ in
+ visit_first cont vertex partition
+ | Continue ->
+ visit_second cont vertex loop partition
+ | End partition' ->
+ assert (loop = NoLoop);
+ let r = NoLoop, Component (vertex, partition) :: partition' in
+ visit cont r
+ | Min_loop loop' ->
+ let r = min_loop loop' loop, partition in
+ visit cont r
+
+ (* Visits all successors of [vertex], then continue with [next] and the
+ [continuation]. The status of [vertex] is first set to [status]. *)
+ and visit_succs continuation next (vertex, status) kind acc =
+ let succs = state.succs vertex in
+ DFN.replace state.dfn vertex status;
+ let list = List.map (fun v -> v, Start kind) succs in
+ visit (list @ (vertex, next) :: continuation) (NoLoop, acc)
+
+ and visit_first continuation vertex partition =
+ match DFN.find state.dfn vertex with
+ (* The vertex is already in the partition *)
+ | Invisible ->
+ visit continuation (NoLoop, partition) (* skip it *)
+ (* The vertex have been visited but is not yet in the partition *)
+ | Parent i ->
+ visit continuation (Loop (vertex,i), partition) (* we are in a loop *)
+ (* The vertex have not been visited yet *)
+ | exception Not_found ->
+ (* Put the current vertex into the stack *)
+ Stack.push vertex state.stack;
+ (* Number it and mark it as visited *)
+ let n = state.num + 1 in
+ state.num <- n;
+ (* Visit all its successors. *)
+ visit_succs continuation Continue (vertex, Parent n) MinLoop partition
+
+ and visit_second continuation vertex loop partition =
+ match loop with
+ (* We are not in a loop. Add the vertex to the partition *)
+ | NoLoop ->
+ let _ = Stack.pop state.stack in
+ DFN.replace state.dfn vertex Invisible;
+ visit continuation (NoLoop,Node(vertex)::partition)
+ (* We are in a loop and the current vertex is the head of this loop *)
+ | Loop(head,_) when N.equal head vertex ->
+ (* Unmark all vertices in the loop, and, if pref is given, try to
+ return a better head *)
+ let rec reset_SCC best_head =
+ (* pop until vertex *)
+ let element = Stack.pop state.stack in
+ DFN.remove state.dfn element;
+ if not (N.equal element vertex) then begin
+ (* the strict is important because we are conservative *)
+ let best_head =
+ if pref best_head element < 0 then element else best_head
+ in
+ reset_SCC best_head
+ end
+ else
+ best_head
+ in
+ let best_head = reset_SCC vertex in
+ let vertex = if N.equal best_head vertex then vertex else best_head in
+ (* Makes [vertex] invisible and visits all its successors. *)
+ visit_succs continuation (End partition) (vertex, Invisible) Default []
+ | _ ->
+ (* [vertex] is part of a strongly connected component but is not the
+ head. Do not update partition; the vertex will
+ be added during the second visit of the SCC. *)
+ visit continuation (loop, partition)
+ in
+ visit [vertex, Start Default] (NoLoop, partition)
+
type pref = N.t -> N.t -> int
let partition ~pref ~init ~succs =
let state = {dfn = DFN.create 17; num = 0; succs;
stack = Stack.create () } in
- let loop,component = visit ~pref state init [] in
+ let loop,component = tail_recursive_visit ~pref state init [] in
assert (loop = NoLoop);
component
diff --git a/src/plugins/value/domains/multidim/abstract_structure.ml b/src/plugins/value/domains/multidim/abstract_structure.ml
index 39540bf0c84060a113139d23bf694cb07e45a46c..2dec7b6004d652c25f0822f0447bbbb0198bc9a7 100644
--- a/src/plugins/value/domains/multidim/abstract_structure.ml
+++ b/src/plugins/value/domains/multidim/abstract_structure.ml
@@ -256,7 +256,7 @@ struct
let pick (m : t) =
match Map.choose_opt m with
- | None -> Kernel.fatal "The disjunction should never be empty"
+ | None -> assert false (* the disjunction should never be empty *)
| Some (k,s) -> k,s,Map.remove k m
let pretty fmt (m : t) =
diff --git a/src/plugins/value/domains/multidim/segmentation.ml b/src/plugins/value/domains/multidim/segmentation.ml
index f8781b9f2f554bbb65b7b31096616fa5da4e4603..1b0c1ec71614c26f8c5008ae75f2c6f3f01dcfbf 100644
--- a/src/plugins/value/domains/multidim/segmentation.ml
+++ b/src/plugins/value/domains/multidim/segmentation.ml
@@ -292,7 +292,7 @@ struct
match Int_val.min_int (to_int_val ~oracle b) with
| Some l -> `Value l
| None ->
- Kernel.warning ~current:true "cannot retrieve a lower bound for %a"
+ Self.warning ~current:true "cannot retrieve a lower bound for %a"
pretty b;
`Top
@@ -300,7 +300,7 @@ struct
match Int_val.max_int (to_int_val ~oracle b) with
| Some u -> `Value u
| None ->
- Kernel.warning ~current:true "cannot retrieve an upper bound for %a"
+ Self.warning ~current:true "cannot retrieve an upper bound for %a"
pretty b;
`Top
@@ -870,7 +870,7 @@ struct
| `Value m -> m
| `Bottom -> assert false
| `Top ->
- Kernel.warning ~current:true
+ Self.warning ~current:true
"failed to introduce %a inside the array segmentation"
Bound.pretty b;
m
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 395f3faead128c1f7ea7edff039dbd19ef888a2c..0355202d2b37b706e0f4203780ac6ecb77ba80d9 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
Plugin WP <next-release>
########################
+- WP [2022-05-06] Upgrade to Why3 1.5
- WP [2022-02-28] New option -wp-fct-timeout, used to customize the
provers timeout per function
- WP [2022-02-02] New option -wp-smoke-dead-local-init, smoke tests on
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 6053d614cd0a5021adc3d0ed24c637bc4c8d78d8..f375c1e28c1f4fe5e61b43b944fdc31bf8b3fc28 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -629,15 +629,16 @@ let smp_leq_improved f a b =
else raise Not_found
let smp_leq_with_land a b =
- try
- let es = match_fun f_land a in
- let a1,_ = match_list_head match_positive_or_null_integer es in
- if F.decide (F.e_leq (e_zint a1) b)
- then e_true
- else raise Not_found
- with Not_found ->
+ let es = match_fun f_land a in
+ let a1,_ = match_list_head match_positive_or_null_integer es in
+ if F.decide (F.e_leq (e_zint a1) b)
+ then e_true
+ else raise Not_found
+(* Disabled rule :
+ with Not_found ->
(* a <= 0 && 0 <= (x&y) ==> a <= (x & y) *)
smp_leq_improved f_land a b
+*)
let smp_eq_with_land a b =
let es = match_fun f_land a in
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 44ab3d0f7f41c3a5b67289e40192f687657f0ffe..314769066fb4a6cd8edb0a31f0dd036445ba7c5f 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -39,13 +39,19 @@ let option_qual =
let why3_failure msg =
Pretty_utils.ksfprintf failwith msg
-module Env = WpContext.Index(struct
+type why3_conf = {
+ env : Why3.Env.env ;
+ libdir : string ;
+ datadir : string ;
+}
+
+module Conf = WpContext.Index(struct
include Datatype.Unit
type key = unit
- type data = Why3.Env.env
+ type data = why3_conf
end)
-let get_why3_env = Env.memoize
+let get_why3_conf = Conf.memoize
begin fun () ->
let config = Why3Provers.config () in
let main = Why3.Whyconf.get_main config in
@@ -53,12 +59,14 @@ let get_why3_env = Env.memoize
(WpContext.directory () :> string)::
((Wp_parameters.Share.get_dir ~mode:`Must_exist "why3") :> string)::
(Why3.Whyconf.loadpath main) in
- Why3.Env.create_env ld
+ let libdir = Why3.Whyconf.libdir main in
+ let datadir = Why3.Whyconf.datadir main in
+ { env = Why3.Env.create_env ld ; libdir ; datadir }
end
type context = {
mutable th : Why3.Theory.theory_uc;
- env: Why3.Env.env;
+ conf: why3_conf;
}
type convert = {
@@ -120,14 +128,14 @@ let fold_map map fold = function
let empty_context name : context = {
th = Why3.Theory.create_theory (Why3.Ident.id_fresh name);
- env = get_why3_env ();
+ conf = get_why3_conf ();
}
let empty_cnv ?(polarity=`NoPolarity) (ctx:context) : convert = {
th = ctx.th;
subst = Lang.F.Tmap.empty;
pool = Lang.F.pool ();
- env = ctx.env;
+ env = ctx.conf.env;
polarity;
incomplete_symbols = Hashtbl.create 3;
incomplete_types = Hashtbl.create 3;
@@ -779,7 +787,7 @@ class visitor (ctx:context) c =
(if import then "import" else "")
Why3.Pp.(print_list (Why3.Pp.constant_string ".") string) file
thy name ;
- let thy = Why3.Env.read_theory ctx.env file thy in
+ let thy = Why3.Env.read_theory ctx.conf.env file thy in
let th = ctx.th in
let th = Why3.Theory.open_scope th name in
let th = Why3.Theory.use_export th thy in
@@ -1153,7 +1161,7 @@ type prover_call = {
mutable killed : bool ;
}
-let ping_prover_call p =
+let ping_prover_call ~libdir p =
match Why3.Call_provers.query_call p.call with
| NoUpdates
| ProverStarted ->
@@ -1170,7 +1178,7 @@ let ping_prover_call p =
Wp_parameters.debug ~dkey
"Hard Kill (late why3server timeout)" ;
p.interrupted <- true ;
- Why3.Call_provers.interrupt_call p.call ;
+ Why3.Call_provers.interrupt_call ~libdir p.call ;
end
in Task.Wait 100
| InternalFailure exn ->
@@ -1205,7 +1213,8 @@ let ping_prover_call p =
VCS.pp_result r;
Task.Return (Task.Result r)
-let call_prover_task ~timeout ~steps prover call =
+let call_prover_task ~timeout ~steps ~conf prover call =
+ let libdir = conf.libdir in
Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %d, steps %d@."
Why3.Whyconf.print_prover prover
(Why3.Opt.get_def (-1) timeout)
@@ -1220,9 +1229,9 @@ let call_prover_task ~timeout ~steps prover call =
let ping = function
| Task.Kill ->
pcall.killed <- true ;
- Why3.Call_provers.interrupt_call call ;
+ Why3.Call_provers.interrupt_call ~libdir call ;
Task.Yield
- | Task.Coin -> ping_prover_call pcall
+ | Task.Coin -> ping_prover_call ~libdir pcall
in
Task.async ping
@@ -1243,7 +1252,7 @@ let digest wpo drv prover task =
end
in Digest.file file |> Digest.to_hex
-let batch pconf driver ?script ~timeout ~steplimit prover task =
+let batch pconf driver ~conf ?script ~timeout ~steplimit prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
let memlimit = Why3.Whyconf.memlimit (Why3.Whyconf.get_main (Why3Provers.config ())) in
@@ -1261,8 +1270,8 @@ let batch pconf driver ?script ~timeout ~steplimit prover task =
let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
let inplace = if script <> None then Some true else None in
let call = Why3.Driver.prove_task_prepared ?old:script ?inplace
- ~command ~limit driver task in
- call_prover_task ~timeout ~steps prover call
+ ~command ~limit ~libdir:conf.libdir ~datadir:conf.datadir driver task in
+ call_prover_task ~conf ~timeout ~steps prover call
(* -------------------------------------------------------------------------- *)
(* --- Interactive Prover (Coq) --- *)
@@ -1295,20 +1304,23 @@ let updatescript ~script driver task =
let d_new = Digest.file script in
if String.equal d_new d_old then Extlib.safe_remove backup
-let editor ~script ~merge wpo pconf driver prover task =
+let editor ~script ~merge ~conf wpo pconf driver prover task =
Task.sync editor_mutex
begin fun () ->
Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
Cache.clear_result ~digest:(digest wpo driver) prover task ;
if merge then updatescript ~script driver task ;
let command = editor_command pconf in
- let call = Why3.Call_provers.call_editor ~command script in
- call_prover_task ~timeout:None ~steps:None pconf.prover call
+ let call =
+ Why3.Call_provers.call_editor
+ ~command ~datadir:conf.datadir ~libdir:conf.libdir script
+ in
+ call_prover_task ~conf ~timeout:None ~steps:None pconf.prover call
end
-let compile ~script ~timeout wpo pconf driver prover task =
+let compile ~script ~timeout ~conf wpo pconf driver prover task =
let digest = digest wpo driver in
- let runner = batch pconf driver ~script in
+ let runner = batch ~conf pconf driver ~script in
Cache.get_result ~digest ~runner ~timeout ~steplimit:None prover task
let prepare ~mode wpo driver task =
@@ -1329,33 +1341,34 @@ let prepare ~mode wpo driver task =
let interactive ~mode wpo pconf driver prover task =
let time = Wp_parameters.InteractiveTimeout.get () in
let timeout = if time <= 0 then None else Some time in
+ let conf = get_why3_conf () in
match prepare ~mode wpo driver task with
| None -> Task.return VCS.unknown
| Some (script, merge) ->
match mode with
| VCS.Batch ->
- compile ~script ~timeout wpo pconf driver prover task
+ compile ~script ~timeout ~conf wpo pconf driver prover task
| VCS.Update ->
if merge then updatescript ~script driver task ;
- compile ~script ~timeout wpo pconf driver prover task
+ compile ~script ~timeout ~conf wpo pconf driver prover task
| VCS.Edit ->
let open Task in
- editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
- compile ~script ~timeout wpo pconf driver prover task
+ editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+ compile ~script ~timeout ~conf wpo pconf driver prover task
| VCS.Fix ->
let open Task in
- compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+ compile ~script ~timeout ~conf wpo pconf driver prover task >>= fun r ->
if VCS.is_valid r then return r else
- editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
- compile ~script ~timeout wpo pconf driver prover task
+ editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+ compile ~script ~timeout ~conf wpo pconf driver prover task
| VCS.FixUpdate ->
let open Task in
if merge then updatescript ~script driver task ;
- compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+ compile ~script ~timeout ~conf wpo pconf driver prover task >>= fun r ->
if VCS.is_valid r then return r else
let merge = false in
- editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
- compile ~script ~timeout wpo pconf driver prover task
+ editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+ compile ~script ~timeout ~conf wpo pconf driver prover task
(* -------------------------------------------------------------------------- *)
(* --- Prove WPO --- *)
@@ -1373,8 +1386,8 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
if Wp_parameters.Generate.get ()
then Task.return VCS.no_result (* Only generate *)
else
- let env = WpContext.on_context context get_why3_env () in
- let drv , pconf , task = prover_task env prover task in
+ let conf = WpContext.on_context context get_why3_conf () in
+ let drv , pconf , task = prover_task conf.env prover task in
if is_trivial task then
Task.return VCS.valid
else
@@ -1383,7 +1396,7 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
else
Cache.get_result
~digest:(digest wpo drv)
- ~runner:(batch pconf drv ?script:None)
+ ~runner:(batch ~conf pconf drv ?script:None)
~timeout ~steplimit prover task
with exn ->
if Wp_parameters.has_dkey dkey_api then
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 3808c2909095b05c7af9415ce7f47e2085947f0c..bf1f7aeaeee5ee9305a2d56a58abcb875acb0ebf 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -37,12 +37,33 @@ let tactical_step step =
(* Note: the provided name is used in the GUi for the subgoal title *)
("Removed Step", Conditions.Have Lang.F.p_true)
-module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
+module Filtered =
+struct
+ type t =
+ | Fun of Lang.Fun.t
+ | Other of Lang.F.term
+
+ let of_term t =
+ match Lang.F.repr t with
+ | Qed.Logic.Fun(f, _) -> Fun f
+ | _ -> Other t
+
+ let pretty fmt = function
+ | Fun f -> Format.fprintf fmt "%a(...)" Lang.Fun.pretty f
+ | Other t -> Lang.F.pp_term fmt t
+
+ let compare a b =
+ match a, b with
+ | Fun a, Fun b -> Lang.Fun.compare a b
+ | Other a, Other b -> Lang.F.compare a b
+ | Fun _, _ -> 1
+ | _, Fun _ -> -1
+
+ let equal a b = 0 = compare a b
+end
-let pp_filtered fmt t =
- match Lang.F.repr t with
- | Qed.Logic.Fun(f,_) -> Format.fprintf fmt "%a(...)" Lang.Fun.pretty f
- | _ -> Lang.F.pp_term fmt t
+module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
+module Filteredset = Qed.Listset.Make(Filtered)
let tactical_inside step remove =
@@ -56,12 +77,17 @@ let tactical_inside step remove =
| Type p | Have p | When p | Core p | Init p ->
let ps = Lang.F.e_props @@ collect p in
let kept = TermLset.diff ps remove in
+ let removed =
+ let add s e = Filteredset.add (Filtered.of_term e) s in
+ List.fold_left add Filteredset.empty remove
+ in
let feedback =
+ let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
Format.asprintf "Filtered: %a"
- (Pretty_utils.pp_list ~sep:", " pp_filtered) remove
+ (Pretty_utils.pp_list ~sep:", " pp) removed
in
let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
- Tactical.replace_single ~at:step.id (feedback, cond)
+ removed, Tactical.replace_single ~at:step.id (feedback, cond)
| _ -> raise Not_found
end
@@ -83,8 +109,18 @@ let collect_remove m = function
let fold_selection s seq =
let m = List.fold_left collect_remove Smap.empty s in
- "Filtered mutiple selection",
- Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+ let tactical s l (acc_rm, seq) =
+ let rm, op = tactical_inside s l in
+ Filteredset.union rm acc_rm, snd @@ op seq
+ in
+ let removed, seq = Smap.fold tactical m ([], seq) in
+ let feedback =
+ let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
+ Format.asprintf "Filtered: %a"
+ (Pretty_utils.pp_list ~sep:", " pp) removed
+ in
+ feedback, seq
+
let process (f: sequent -> string * sequent) s = [ f s ]
@@ -101,7 +137,7 @@ class clear =
Applicable(process @@ tactical_step step)
| Inside(Step step, remove) ->
begin
- try Applicable(process @@ tactical_inside step [remove])
+ try Applicable(process @@ snd @@ tactical_inside step [remove])
with Not_found -> Not_applicable
end
| Multi es ->
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index f72efde27b4351668c9ad6f5d474747613b8ed08..a30d3798e06589c1e4ed673a63cda1e608de72bf 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -113,27 +113,29 @@ let unfolds_from_list phis es =
let unfolds_from_smap phis m =
Smap.map (fun _s es -> unfolds_from_list phis es) m
+module Unfoldedset = Qed.Listset.Make(Lang.Fun)
+
let tactical_inside step unfolds sequent =
if Lang.F.Tmap.is_empty unfolds
then raise Not_found
else match step.condition with
| Type p | Have p | When p | Core p | Init p ->
- let unfolded = ref [] in
+ let unfolded = ref Unfoldedset.empty in
let subst t =
let result = Lang.F.Tmap.find t unfolds in
begin match F.repr t with
- | Qed.Logic.Fun(f,_) -> unfolded := f :: !unfolded
+ | Qed.Logic.Fun(f,_) -> unfolded := Unfoldedset.add f !unfolded
| _ -> ()
end ;
result
in
let p = condition step @@ Lang.p_subst subst p in
- let unfolded = List.sort_uniq Lang.Fun.compare !unfolded in
let feedback =
- Format.asprintf "Unfolded: %a"
- (Pretty_utils.pp_list ~sep:", " Lang.Fun.pretty) unfolded
+ let pp fmt f = Format.fprintf fmt "'%a'" Lang.Fun.pretty f in
+ Format.asprintf "Unfold %a"
+ (Pretty_utils.pp_list ~sep:", " pp) !unfolded
in
- snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
+ !unfolded, snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
| _ -> raise Not_found
let tactical_goal unfolds (seq, g) =
@@ -144,12 +146,21 @@ let tactical_goal unfolds (seq, g) =
seq, Lang.p_subst subst g
let fold_selection goal_unfolds step_unfolds sequent =
- "Unfolded multiple selection",
+ let tactical s l (acc_unfolded, seq) =
+ let unfolded, seq = tactical_inside s l seq in
+ Unfoldedset.union unfolded acc_unfolded, seq
+ in
+ let unfolded, seq = Smap.fold tactical step_unfolds ([], sequent) in
+ let feedback =
+ let pp fmt f = Format.fprintf fmt "'%a'" Lang.Fun.pretty f in
+ Format.asprintf "Unfold %a"
+ (Pretty_utils.pp_list ~sep:", " pp) unfolded
+ in
let add_goal = match goal_unfolds with
| None -> Extlib.id
| Some goal_unfolds -> tactical_goal goal_unfolds
in
- add_goal @@ Smap.fold tactical_inside step_unfolds sequent
+ feedback, add_goal seq
let process (f: sequent -> string * sequent) s = [ f s ]
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 425f3df70fe94de264fd1e941535ffcd4c14e45e..9e529fc7c44f60f8bfd71fb04f74271d5573bcc8 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -91,6 +91,12 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
Some (id , implies ?assumes p)
else None
+let normalize_decreases (d, li) =
+ let module L = NormAtLabels in
+ let at_pre e = Logic_const.tat (e, BuiltinLabel Pre) in
+ let labels = L.labels_fct_pre in
+ (at_pre @@ L.preproc_term labels d, li)
+
let normalize_froms tk froms =
let module L = NormAtLabels in
let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
@@ -246,12 +252,13 @@ let get_terminates_hyp kf =
let check_variant_relation = function
| (_, None) -> ()
- | (_, Some rel) ->
- Wp_parameters.hypothesis ~once:true
+ | ({ term_loc }, Some rel) ->
+ Wp_parameters.hypothesis
+ ~source:(fst term_loc) ~once:true
"'%a' relation must be well-founded" Cil_printer.pp_logic_info rel
let get_decreases_goal kf =
- let defined t = WpPropId.mk_decrease_id kf Kglobal t, t in
+ let defined t = WpPropId.mk_decrease_id kf Kglobal t, normalize_decreases t in
match Annotations.decreases ~populate:false kf with
| None -> None
| Some v -> check_variant_relation v ; Some (defined v)
@@ -348,7 +355,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| Writes froms -> Writes (normalize_froms Normal froms)
in
let terminates = get_terminates_hyp kf in
- let decreases = get_decreases_hyp kf in
+ let decreases = Option.map normalize_decreases @@ get_decreases_hyp kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ee6d749805a8fb90468fd8eb263e8b22a4cc6ca5..110ef26efaed4f63b55589df6495d57071948a0d 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1162,7 +1162,7 @@ struct
| (caller_d, rel), Some (callee_d,_ ) ->
let rel caller callee = match rel with
| None ->
- p_and (p_leq e_zero callee) (p_lt callee caller)
+ p_and (p_leq e_zero caller) (p_lt callee caller)
| Some rel ->
(L.in_frame call_f (L.call_pred call_e))
rel [] [caller ; callee]
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 8df1b3908a149065d28db136450806405afc82dc..010a5beef14a3a671c0bdc352dbf5ae391bf7659 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -56,15 +56,15 @@ case $WHY3VERSION in
AC_MSG_RESULT([not found!])
plugin_disable(wp,[why3 not found])
;;
- 0.* | 1.[[0123]].*)
- AC_MSG_RESULT([found $WHY3VERSION: requires 1.4.0+])
+ 0.* | 1.[[01234]].*)
+ AC_MSG_RESULT([found $WHY3VERSION: requires 1.5.0+])
plugin_disable(wp,[non-supported why3 $WHY3VERSION])
;;
- 1.4.*)
+ 1.5.*)
AC_MSG_RESULT([found $WHY3VERSION: ok])
;;
*)
- AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.4.0+)])
+ AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.5.0+)])
;;
esac
fi
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 0033fe47bf1468749bc80c1fa958a8ebb601297a..4ae48410ed5e5b8e6a7bb8e302698328ab627e62 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -214,6 +214,10 @@ let preproc_annot labels p =
let visitor = new norm_at labels in
Visitor.visitFramacPredicate visitor p
+let preproc_term labels t =
+ let visitor = new norm_at labels in
+ Visitor.visitFramacTerm visitor t
+
(** @raise LabelError if there is a label in [p] that is incompatible
* with the [labels] translation *)
let preproc_assigns labels asgns =
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index dfa2f0962e42c72ebf47b3d4e9453987416a19c4..73e5c5ca0be2074e063955cf51a19497f891895f 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -42,6 +42,7 @@ val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> labe
val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
+val preproc_term : label_mapping -> term -> term
val preproc_annot : label_mapping -> predicate -> predicate
val preproc_assigns : label_mapping -> from list -> from list
val has_postassigns : assigns -> bool
diff --git a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
index e2ecb2158690c4c94a95668c87a9268fd4ee92e2..ad74ce62fd60dd44ff2ec66b030b29c1b9d017f1 100644
--- a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
+++ b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
@@ -1,60 +1,60 @@
File "spec_memory.why", line 24, characters 4-56:
-Verification condition check_valid_rd.
+Goal check_valid_rd.
Prover result is: Valid.
File "spec_memory.why", line 27, characters 4-56:
-Verification condition check_valid.
+Goal check_valid.
Prover result is: Valid.
File "spec_memory.why", line 30, characters 4-62:
-Verification condition invalid_spec.
+Goal invalid_spec.
Prover result is: Valid.
File "spec_memory.why", line 34, characters 4-76:
-Verification condition invalid_null_spec.
+Goal invalid_null_spec.
Prover result is: Valid.
File "spec_memory.why", line 38, characters 4-51:
-Verification condition invalid_null.
+Goal invalid_null.
Prover result is: Valid.
File "spec_memory.why", line 42, characters 4-79:
-Verification condition invalid_empty.
+Goal invalid_empty.
Prover result is: Valid.
File "spec_memory.why", line 46, characters 4-59:
-Verification condition valid_rd_null.
+Goal valid_rd_null.
Prover result is: Valid.
File "spec_memory.why", line 49, characters 4-59:
-Verification condition valid_rw_null.
+Goal valid_rw_null.
Prover result is: Valid.
File "spec_memory.why", line 52, characters 4-34:
-Verification condition valid_obj_null.
+Goal valid_obj_null.
Prover result is: Valid.
File "spec_memory.why", line 56, characters 4-77:
-Verification condition INC_P.
+Goal INC_P.
Prover result is: Valid.
File "spec_memory.why", line 60, characters 4-169:
-Verification condition INC_A.
+Goal INC_A.
Prover result is: Valid.
File "spec_memory.why", line 67, characters 4-63:
-Verification condition INC_1.
+Goal INC_1.
Prover result is: Valid.
File "spec_memory.why", line 71, characters 4-64:
-Verification condition INC_2.
+Goal INC_2.
Prover result is: Valid.
File "spec_memory.why", line 75, characters 4-161:
-Verification condition INC_3.
+Goal INC_3.
Prover result is: Valid.
File "spec_memory.why", line 82, characters 4-178:
-Verification condition INC_4.
+Goal INC_4.
Prover result is: Valid.
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index b01d3e9c63ef85cdfcb16c2ae11da55dc0141dc7..efd2e9f9df793726354d9a57d5856a32742bedf2 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -57,7 +57,7 @@ end
let m3 = set m2 (shift_sint32 a 3) (get m2 a2) in
0 <= i1 ->
0 <= i ->
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
i1 <= 9 ->
i <= 9 ->
linked t ->
diff --git a/src/plugins/wp/tests/wp_acsl/decreases.i b/src/plugins/wp/tests/wp_acsl/decreases.i
index b4d482fe2e6de2726ac360465942eae7a6a6f128..c264819eb94cff0ae29c3bde85d226946495dea0 100644
--- a/src/plugins/wp/tests/wp_acsl/decreases.i
+++ b/src/plugins/wp/tests/wp_acsl/decreases.i
@@ -111,3 +111,15 @@ void mw2(unsigned x){
(void)fact(x); // no verification of decreases here
}
+
+// Recursion with side-effect
+
+int x ;
+
+//@ decreases x ;
+void se(void){
+ if (x > 0){
+ x -- ;
+ se();
+ }
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index 58865eff22dc2d0733b3c82c8270a883ca4ae487..2067e2fba853bee466f0b264d6e023006ef6e01b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -75,13 +75,13 @@ theory A_Occ
(* use Chunk *)
- Q_empty :
+ axiom Q_empty :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
(* use Compound *)
- Q_is :
+ axiom Q_is :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in
@@ -91,7 +91,7 @@ theory A_Occ
is_sint32 v ->
is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t
- Q_isnt :
+ axiom Q_isnt :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in
@@ -154,7 +154,7 @@ end
forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
i3 <= i1 ->
i < i3 ->
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
is_sint32_chunk t ->
is_uint32 i3 ->
is_uint32 i1 ->
@@ -233,14 +233,14 @@ theory A_Occ1
(* use Chunk1 *)
- Q_empty1 :
+ axiom Q_empty1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
t <=' f ->
is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
(* use Compound1 *)
- Q_is1 :
+ axiom Q_is1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in
@@ -250,7 +250,7 @@ theory A_Occ1
is_sint321 v ->
is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t
- Q_isnt1 :
+ axiom Q_isnt1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in
@@ -315,7 +315,7 @@ end
let x = (- 1) +' i1 in
not get1 t (shift_sint321 a x) = i2 ->
i <' i1 ->
- region1 (base1 a) <=' 0 ->
+ region1 (a.base1) <=' 0 ->
i1 <=' 1000 ->
is_sint32_chunk1 t ->
is_uint321 i1 ->
@@ -392,14 +392,14 @@ theory A_Occ2
(* use Chunk2 *)
- Q_empty2 :
+ axiom Q_empty2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
t <='' f ->
is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
(* use Compound2 *)
- Q_is2 :
+ axiom Q_is2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in
@@ -409,7 +409,7 @@ theory A_Occ2
is_sint322 v ->
is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t
- Q_isnt2 :
+ axiom Q_isnt2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
index 61a3435b5bbc033d1871b398ddf626f180645976..65805aa212de29ff538de8e68b6cd7ea4bc82640 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
@@ -122,7 +122,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 12
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index 1c0241e1df554d73e7532ba44337a17271391de2..84ff1f41b857153c800622b41c6622c7af1a46e0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -2,11 +2,14 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -21,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -49,7 +52,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
Assume { Type: is_sint32(n). (* Else *) Have: n != 0. }
-Prove: 0 < n.
+Prove: 0 <= n.
------------------------------------------------------------
------------------------------------------------------------
@@ -117,7 +120,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -127,14 +130,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
@@ -154,7 +157,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -176,7 +179,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -197,14 +200,14 @@ Prove: true.
Goal Recursion variant (1/2):
Call Effect at line 91
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 92
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
@@ -240,3 +243,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index 503c417688228f6147615930e14def6d47a18997..f45e5a772fee6d25d380583944f4b4417991a2f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -2,11 +2,14 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -21,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -48,14 +51,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
-Assume {
- Type: is_sint32(n).
- (* Goal *)
- When: 0 <= n.
- (* Else *)
- Have: n != 0.
-}
-Prove: 0 < n.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -129,7 +125,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -139,14 +135,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
@@ -166,7 +162,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -188,7 +184,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -215,7 +211,7 @@ Assume {
(* Then *)
Have: x != 0.
}
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
@@ -257,3 +253,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 982b66a1342f47f627b60d988b9cc4890a35b48a..4469b4881435e5e65c5c1203e12cd5c46261760d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -138,42 +138,42 @@ end
forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin:int) (end1:int) =
+ addr) (begin1:int) (end1:int) =
forall i:int.
- begin <= i ->
+ begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin:int) (i:int) (j:int) (end1:int) =
+ (begin1:int) (i:int) (j:int) (end1:int) =
((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin <= i) /\
+ begin1 <= i) /\
i < j) /\
j < end1) /\
(forall i1:int.
not i1 = i ->
not j = i1 ->
- begin <= i1 ->
+ begin1 <= i1 ->
i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, end1:int.
- P_same_array mint mint1 a b begin end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_same_array mint mint1 a b begin1 end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, i:int, j:int, end1:int.
- P_swap mint mint1 a b begin i j end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_swap mint mint1 a b begin1 i j end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
- addr, b:addr, c:addr, begin:int, end1:int.
- P_same_elements mint mint1 b c begin end1 ->
- P_same_elements mint1 mint2 a b begin end1 ->
- P_same_elements mint mint2 a c begin end1
+ addr, b:addr, c:addr, begin1:int, end1:int.
+ P_same_elements mint mint1 b c begin1 end1 ->
+ P_same_elements mint1 mint2 a b begin1 end1 ->
+ P_same_elements mint mint2 a c begin1 end1
goal wp_goal :
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
index 67a25621bb869debb0266cef37f13f481f8aa753..fa26e5047b49c275c7402b281b9632446b4fd3d9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
@@ -22,13 +22,14 @@
predicate P_RP int
- P_RP_def : forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
+ axiom P_RP_def :
+ forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
function L_F (i:int) : int = 2 * i
function L_RF int : int
- L_RF_def :
+ axiom L_RF_def :
forall i:int. L_RF i = (if i <= 0 then 0 else L_F i + L_RF ((- 1) + i))
goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index eb82e6b610d5fb5de77eb82ff7b6f44706de6d8d..35ee39d24887322fed5fb20fc1901f30dae31203 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -120,13 +120,13 @@ theory Compound
Init_S1_X1 (get init (shiftfield_F1_X_a p))
(get init (shiftfield_F1_X_b p)) (get init (shiftfield_F1_X_c p))
- Q_Load_S1_X_update_Mchar0 :
+ axiom Q_Load_S1_X_update_Mchar0 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
separated p 3 q 1 ->
Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_eqmem_Mchar0 :
+ axiom Q_Load_S1_X_eqmem_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
@@ -135,21 +135,21 @@ theory Compound
eqmem mchar mchar1 q n ->
Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_havoc_Mchar0 :
+ axiom Q_Load_S1_X_havoc_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr
[Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
separated p 3 q n ->
- Load_S1_X p (havoc mchar1 mchar q n) mint mint1
- = Load_S1_X p mchar mint mint1
+ Load_S1_X p (havoc mchar1 mchar q n) mint mint1 =
+ Load_S1_X p mchar mint mint1
- Q_Load_S1_X_update_Mint1 :
+ axiom Q_Load_S1_X_update_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
separated p 3 q 1 ->
Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_eqmem_Mint1 :
+ axiom Q_Load_S1_X_eqmem_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
@@ -158,21 +158,21 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_havoc_Mint1 :
+ axiom Q_Load_S1_X_havoc_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
separated p 3 q n ->
- Load_S1_X p mchar (havoc mint2 mint1 q n) mint
- = Load_S1_X p mchar mint1 mint
+ Load_S1_X p mchar (havoc mint2 mint1 q n) mint =
+ Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_update_Mint2 :
+ axiom Q_Load_S1_X_update_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
separated p 3 q 1 ->
Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_eqmem_Mint2 :
+ axiom Q_Load_S1_X_eqmem_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
@@ -181,28 +181,28 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_havoc_Mint2 :
+ axiom Q_Load_S1_X_havoc_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
separated p 3 q n ->
- Load_S1_X p mchar mint (havoc mint2 mint1 q n)
- = Load_S1_X p mchar mint mint1
+ Load_S1_X p mchar mint (havoc mint2 mint1 q n) =
+ Load_S1_X p mchar mint mint1
- Q_Load_Init_S1_X_update_Init0 :
+ axiom Q_Load_Init_S1_X_update_Init0 :
forall init:addr -> bool, p:addr, q:addr, v:bool
[Load_Init_S1_X p (set init q v)].
separated p 3 q 1 ->
Load_Init_S1_X p (set init q v) = Load_Init_S1_X p init
- Q_Load_Init_S1_X_eqmem_Init0 :
+ axiom Q_Load_Init_S1_X_eqmem_Init0 :
forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
[Load_Init_S1_X p init, eqmem init init1 q n| Load_Init_S1_X p init1,
eqmem init init1 q n].
included p 3 q n ->
eqmem init init1 q n -> Load_Init_S1_X p init1 = Load_Init_S1_X p init
- Q_Load_Init_S1_X_havoc_Init0 :
+ axiom Q_Load_Init_S1_X_havoc_Init0 :
forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
[Load_Init_S1_X p (havoc init1 init q n)].
separated p 3 q n ->
@@ -271,7 +271,7 @@ end
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
addr -> int, a:addr, x:S1_X.
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
IsS1_X x ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index d9bd70618f767ce264637cc140e5ee6199eadd5d..484dd6e31ec2b96eeb5bc83bfc02f60bb486c818 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
@@ -75,7 +77,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 80
Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
index 62e79688690128fd49abbc91e54a2e4c560df53d..a87bf3324219a0f849a14aee28f61793d56182f3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
@@ -2,14 +2,17 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -36,8 +39,9 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 17 / 26
- Qed: 6
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 18 / 27
+ Qed: 7
Alt-Ergo: 11 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 63e3fba1f7426ce524df7c0e5c5f319d6f557091..f18fe8e1bdfe5c40aead8f912bb2e0cfdcc05743 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -2,14 +2,17 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -17,7 +20,7 @@
[wp] [Alt-Ergo] Goal typed_fails_facto_gen_variant : Unsuccess
[wp] [Qed] Goal typed_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fact_i_terminates_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_fact_i_variant : Valid
+[wp] [Qed] Goal typed_fact_i_variant : Valid
[wp] [Qed] Goal typed_fails_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_i_terminates_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fails_fact_i_variant : Unsuccess
@@ -36,16 +39,17 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 18 / 26
- Qed: 7
- Alt-Ergo: 11 (unsuccess: 8)
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 19 / 27
+ Qed: 9
+ Alt-Ergo: 10 (unsuccess: 8)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fact 1 1 2 100%
fails_fact - - 1 0.0%
facto_gen - 1 1 100%
fails_facto_gen - - 1 0.0%
- fact_i 1 2 3 100%
+ fact_i 2 1 3 100%
fails_fact_i 1 - 3 33.3%
m2 - 2 2 100%
m1 - 1 1 100%
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index cf90d39ba3fc26032ba408a35e80cd1c1badb88a..cb8634fd614c650bd783d59986c144dc533969fa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index fe74a260b12b87a301e7cc4bbddfbdc4cc00bd2c..c8d3f169d3faade2e0c503923e59a7f7ccb141d4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -59,19 +59,19 @@ theory Compound
function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0
- Q_Load_S2_A_update_Mint0 :
+ axiom Q_Load_S2_A_update_Mint0 :
forall mint:addr -> int, p:addr, q:addr, v:int
[Load_S2_A p (set mint q v)].
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
- Q_Load_S2_A_eqmem_Mint0 :
+ axiom Q_Load_S2_A_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
eqmem mint mint1 q n].
included p 1 q n ->
eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
- Q_Load_S2_A_havoc_Mint0 :
+ axiom Q_Load_S2_A_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p (havoc mint1 mint q n)].
separated p 1 q n ->
@@ -104,8 +104,8 @@ end
let a3 = Load_S2_A a t in
let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
not x = i ->
- region (base a1) <= 0 ->
- region (base a) <= 0 ->
+ region (a1.base) <= 0 ->
+ region (a.base) <= 0 ->
is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3
end
[wp] 1 goal generated
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 2e738afb004c169c4707afb644b505700e014741..8c36850543d3af2d512bfb7f864d20b326ef757c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -24,17 +24,18 @@ Prove: true.
Goal Loop assigns (file issue_751.i, line 8) (2/2):
Effect at line 11
Let x = land(3840, R).
-Let x_1 = j - 1.
+Let x_1 = lsr(x, 8).
+Let x_2 = j - 1.
Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_1).
+ Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_2) /\ is_sint32(x_1).
(* Heap *)
Type: (region(Data_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: !invalid(Malloc_0, shift_sint32(Data_0, x_1), 1).
+ When: !invalid(Malloc_0, shift_sint32(Data_0, x_2), 1).
(* Pre-condition *)
Have: (0 < x) /\ (x <= 2303).
(* Invariant 'RANGE' *)
- Have: (0 < j) /\ (j <= (1 + lsr(x, 8))).
+ Have: (0 < j) /\ (j <= (1 + x_1)).
(* Then *)
Have: j <= (x / 256).
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 973a39e45fa5af1ba55ed02d29a1bfe1666b0a7a..25cdbf437dc4817a633ae894932889549b4a583c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -101,42 +101,42 @@ end
P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node
predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin:int) (end1:int) =
+ addr) (begin1:int) (end1:int) =
forall i:int.
- begin <= i ->
+ begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin:int) (i:int) (j:int) (end1:int) =
+ (begin1:int) (i:int) (j:int) (end1:int) =
((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin <= i) /\
+ begin1 <= i) /\
i < j) /\
j < end1) /\
(forall i1:int.
not i1 = i ->
not j = i1 ->
- begin <= i1 ->
+ begin1 <= i1 ->
i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, end1:int.
- P_same_array mint mint1 a b begin end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_same_array mint mint1 a b begin1 end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, i:int, j:int, end1:int.
- P_swap mint mint1 a b begin i j end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_swap mint mint1 a b begin1 i j end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
- addr, b:addr, c:addr, begin:int, end1:int.
- P_same_elements mint mint1 b c begin end1 ->
- P_same_elements mint1 mint2 a b begin end1 ->
- P_same_elements mint mint2 a c begin end1
+ addr, b:addr, c:addr, begin1:int, end1:int.
+ P_same_elements mint mint1 b c begin1 end1 ->
+ P_same_elements mint1 mint2 a b begin1 end1 ->
+ P_same_elements mint mint2 a c begin1 end1
goal wp_goal :
forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 70fd22d935e3729b93f16fb6b817a9b65b97d11a..29f604c34eaf0c3f72c10cc6cee353d6b77e173e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -74,7 +74,7 @@ end
goal wp_goal :
forall t:addr -> int, i:int, a:addr.
let x = get t (shift_sint32 a i) in
- region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+ region (a.base) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
end
[wp] 1 goal generated
------------------------------------------------------------
@@ -162,7 +162,7 @@ end
goal wp_goal :
forall t:addr1 -> int, i:int, a:addr1.
let x = get1 t (shift_sint321 a i) in
- region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
+ region1 (a.base1) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
end
[wp] 1 goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index fc2bd44fdd5bf6ac2dc4cfe36213ff7ff1950c6a..bdae904b176d5799a42a2c3f84f8b6190c311e27 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -2,5 +2,5 @@
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.2.0
-2. The Why3 platform, version 1.4.0
+2. The Why3 platform, version 1.5.0
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index ff97bc71c534b5b33638bfe120f1c0de928f8e66..16921421e1bdbcb0a10f13b41d0179b4f67afae7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -74,7 +74,7 @@ end
goal wp_goal :
forall t:addr -> int, i:int, a:addr.
let x = get t (shift_sint32 a i) in
- region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+ region (a.base) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
end
[wp] [Alt-Ergo] Goal typed_f_ensures : Unsuccess
[wp] Proved goals: 0 / 1
@@ -154,7 +154,7 @@ end
goal wp_goal :
forall t:addr1 -> int, i:int, a:addr1.
let x = get1 t (shift_sint321 a i) in
- region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
+ region1 (a.base1) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
end
[wp] [Alt-Ergo] Goal typed_ref_f_ensures : Unsuccess
[wp] Proved goals: 0 / 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index 7af1209d3c472e1e717ba1dcdf4090b5f4b641ba..9c2a626fc58df6e504db7003ad19ac459f55babc 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -51,7 +51,7 @@
typed_clear_in_step_check subgoal:
Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
- Assume { (* Filtered: P_P(...) *) Have: P_Q /\ P_R. }
+ Assume { (* Filtered: 'P_P(...)' *) Have: P_Q /\ P_R. }
Prove: P_S(42).
------------------------------------------------------------
@@ -77,7 +77,7 @@
typed_clear_in_step_check subgoal:
Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
- Assume { (* Filtered: P_Q(...) *) Have: P_R. }
+ Assume { (* Filtered: 'P_Q(...)' *) Have: P_R. }
Prove: P_S(42).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index 324a789c9b982c3478ddd70178df49f3c1c4adc5..268995c9ffb2bf6b68baaf179a0d0a43b0f371ee 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -103,61 +103,61 @@ theory Compound
(Array_uint32 (shiftfield_F1_S_a p) 5 mint)
(Array_sint64 (shiftfield_F1_S_b p) 5 mint2)
- Q_Array_uint32_access :
+ axiom Q_Array_uint32_access :
forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_uint32 p n mint) i].
0 <= i ->
i < n -> get (Array_uint32 p n mint) i = get mint (shift_uint32 p i)
- Q_Array_uint32_update_Mint0 :
+ axiom Q_Array_uint32_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_uint32 p n (set mint q v)].
not q = p -> Array_uint32 p n (set mint q v) = Array_uint32 p n mint
- Q_Array_uint32_eqmem_Mint0 :
+ axiom Q_Array_uint32_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_uint32 p n mint, eqmem mint mint1 q n1| Array_uint32 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_uint32 p n mint1 = Array_uint32 p n mint
- Q_Array_uint32_havoc_Mint0 :
+ axiom Q_Array_uint32_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_uint32 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
- Q_Array_sint64_access :
+ axiom Q_Array_sint64_access :
forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_sint64 p n mint) i].
0 <= i ->
i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p i)
- Q_Array_sint64_update_Mint0 :
+ axiom Q_Array_sint64_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_sint64 p n (set mint q v)].
not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint
- Q_Array_sint64_eqmem_Mint0 :
+ axiom Q_Array_sint64_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint
- Q_Array_sint64_havoc_Mint0 :
+ axiom Q_Array_sint64_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint64 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
- Q_Load_S1_S_update_Mint0 :
+ axiom Q_Load_S1_S_update_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
separated p 11 q 1 ->
Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2
- Q_Load_S1_S_eqmem_Mint0 :
+ axiom Q_Load_S1_S_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint mint2 mint3,
eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
@@ -166,21 +166,21 @@ theory Compound
eqmem mint mint1 q n ->
Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3
- Q_Load_S1_S_havoc_Mint0 :
+ axiom Q_Load_S1_S_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
separated p 11 q n ->
- Load_S1_S p (havoc mint1 mint q n) mint2 mint3
- = Load_S1_S p mint mint2 mint3
+ Load_S1_S p (havoc mint1 mint q n) mint2 mint3 =
+ Load_S1_S p mint mint2 mint3
- Q_Load_S1_S_update_Mint1 :
+ axiom Q_Load_S1_S_update_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
separated p 11 q 1 ->
Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint
- Q_Load_S1_S_eqmem_Mint1 :
+ axiom Q_Load_S1_S_eqmem_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint3 mint1 mint,
eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
@@ -189,21 +189,21 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint
- Q_Load_S1_S_havoc_Mint1 :
+ axiom Q_Load_S1_S_havoc_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
separated p 11 q n ->
- Load_S1_S p mint3 (havoc mint2 mint1 q n) mint
- = Load_S1_S p mint3 mint1 mint
+ Load_S1_S p mint3 (havoc mint2 mint1 q n) mint =
+ Load_S1_S p mint3 mint1 mint
- Q_Load_S1_S_update_Mint2 :
+ axiom Q_Load_S1_S_update_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
separated p 11 q 1 ->
Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2
- Q_Load_S1_S_eqmem_Mint2 :
+ axiom Q_Load_S1_S_eqmem_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint1 mint mint2,
eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
@@ -212,13 +212,13 @@ theory Compound
eqmem mint2 mint3 q n ->
Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2
- Q_Load_S1_S_havoc_Mint2 :
+ axiom Q_Load_S1_S_havoc_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
separated p 11 q n ->
- Load_S1_S p mint1 mint (havoc mint3 mint2 q n)
- = Load_S1_S p mint1 mint mint2
+ Load_S1_S p mint1 mint (havoc mint3 mint2 q n) =
+ Load_S1_S p mint1 mint mint2
end
[wp:print-generated]
theory WP
@@ -246,7 +246,7 @@ end
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int.
let a1 = Load_S1_S a t t2 t1 in
let a2 = Load_S1_S a t (set t2 (shiftfield_F1_S_f a) i) t1 in
- region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
+ region (a.base) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
end
[wp] 1 goal generated
------------------------------------------------------------
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
new file mode 100644
index 0000000000000000000000000000000000000000..4f5db3d6867a1bd94ba7e9073d5e5b384cdd4d78
--- /dev/null
+++ b/tests/syntax/ast_diff_1.i
@@ -0,0 +1,96 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ OPT: -then -ast-diff ast_diff_2.i
+*/
+int X;
+int Y=3;
+
+int f(int x) {
+ if (x <= 0)
+ X = 0;
+ else
+ X = x;
+ return X;
+}
+
+/*@ requires Y > 0;
+ ensures X > 0;
+ assigns X;
+*/
+int g() {
+ X = Y;
+ return X;
+}
+
+/*@ requires X > 0;
+ ensures X > 0;
+ assigns X;
+*/
+int h() {
+ if (Y > 0)
+ X = Y;
+ return Y;
+}
+
+/*@ requires \is_finite(x);
+ requires \is_finite(y);
+ assigns \nothing;
+ ensures \true != \false;
+*/
+int use_logic_builtin(double x, float y);
+
+int has_static_local(void) {
+ static int x = 0;
+ x++;
+ return x;
+}
+
+/*@ exits \exit_status == 1; */
+int decl(void);
+
+int used_in_decl;
+
+int decl() {
+ used_in_decl++;
+ return used_in_decl;
+}
+
+void (*ptr_func)(void);
+
+extern void i(void);
+
+void (*ptr_func)(void) = &i;
+
+/*@ type nat = Zero | Succ(nat); */
+
+/*@ logic nat succ(nat n) = Succ(n); */
+
+/*@ ensures succ(Zero) == Succ(Zero); */
+extern void i(void);
+
+void local_var_use(int v, int a[][v]) {
+ int x;
+ int y [sizeof(x)];
+}
+
+struct s;
+
+extern struct s s;
+
+enum e;
+
+struct s* use_s() { enum e* x; return &s; }
+
+void with_goto_changed(int c) {
+ if (c) goto L1;
+ X++;
+ L1: X++;
+ L2: X++;
+}
+
+void with_goto_unchanged(int c) {
+ if (c) goto L1;
+ X++;
+ L1: X++;
+ L2: X++;
+}
diff --git a/tests/syntax/ast_diff_1.ml b/tests/syntax/ast_diff_1.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fd43df597f6eb2b8a04e96c5db8600afcd28a6f1
--- /dev/null
+++ b/tests/syntax/ast_diff_1.ml
@@ -0,0 +1,27 @@
+include Plugin.Register(
+ struct
+ let name = "AST diff test"
+ let shortname = "AST diff test"
+ let help = "Show results of AST diff computation"
+ end)
+
+let show_var vi c =
+ result "Variable %a: %a"
+ Cil_datatype.Varinfo.pretty vi
+ Ast_diff.Varinfo.pretty_data c
+
+let show_fun kf c =
+ result "Function %a: %a"
+ Kernel_function.pretty kf
+ Ast_diff.Kernel_function.pretty_data c
+
+let show_correspondances () =
+ if Kernel.AstDiff.get () then begin
+ result "Showing correspondances between %s and %s"
+ (Project.get_name (Ast_diff.Orig_project.get()))
+ (Project.get_name (Project.current()));
+ Ast_diff.Varinfo.iter show_var;
+ Ast_diff.Kernel_function.iter show_fun;
+ end
+
+let () = Db.Main.extend show_correspondances
diff --git a/tests/syntax/ast_diff_2.i b/tests/syntax/ast_diff_2.i
new file mode 100644
index 0000000000000000000000000000000000000000..9f6b60d8dce7a6a02858b0796b3ca74dd91cc289
--- /dev/null
+++ b/tests/syntax/ast_diff_2.i
@@ -0,0 +1,89 @@
+/* run.config
+ DONTRUN: main test is in ast_diff_1.i
+*/
+int X;
+int Y=4;
+
+int f(int x) {
+ if (x <= 0)
+ X = 0;
+ else
+ X = x;
+ return X;
+}
+
+/*@ requires Y > 0;
+ ensures X > 0;
+ assigns X;
+*/
+int g() {
+ X = Y;
+ return X;
+}
+
+/*@ requires X > 0;
+ ensures X > 0;
+ assigns X;
+*/
+int h() {
+ if (Y > 0)
+ X = Y;
+ return Y;
+}
+
+/*@ requires \is_finite(x);
+ requires \is_finite(y);
+ assigns \nothing;
+ ensures \true != \false;
+*/
+int use_logic_builtin(double x, float y);
+
+int has_static_local(void) {
+ static int y = 0;
+ y++;
+ return y;
+}
+
+int used_in_decl;
+
+/*@ exits \exit_status == 1; */
+int decl() {
+ used_in_decl++;
+ return used_in_decl;
+}
+
+extern void i(void);
+
+void (*ptr_func)(void) = &i;
+
+/*@ type nat = Zero | Succ(nat); */
+
+/*@ logic nat succ(nat n) = Succ(n); */
+
+/*@ ensures succ(Zero) == Succ(Zero); */
+extern void i(void);
+
+void local_var_use(int w, int q[][w]) {
+ int z;
+ int t [sizeof(z)];
+}
+
+extern struct s s;
+
+enum e;
+
+struct s* use_s() { enum e* x; return &s; }
+
+void with_goto_changed(int c) {
+ if (c) goto L2;
+ X++;
+ L1: X++;
+ L2: X++;
+}
+
+void with_goto_unchanged(int c) {
+ if (c) goto L1;
+ X++;
+ L1: X++;
+ L2: X++;
+}
diff --git a/tests/syntax/oracle/ast_diff_1.res.oracle b/tests/syntax/oracle/ast_diff_1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7bf1eac2f1efc9d09c809869b7562cc0b0fa57f1
--- /dev/null
+++ b/tests/syntax/oracle/ast_diff_1.res.oracle
@@ -0,0 +1,42 @@
+[kernel] Parsing ast_diff_1.i (no preprocessing)
+[kernel] Parsing ast_diff_2.i (no preprocessing)
+[AST diff test] Showing correspondances between orig_default and default
+[AST diff test] Variable i: => i
+[AST diff test] Variable local_var_use: => local_var_use
+[AST diff test] Variable v: => w
+[AST diff test] Variable a: => q
+[AST diff test] Variable x: => z
+[AST diff test] Variable y: => t
+[AST diff test] Variable s: => s
+[AST diff test] Variable use_s: => use_s
+[AST diff test] Variable x: => x
+[AST diff test] Variable with_goto_changed: => with_goto_changed
+[AST diff test] Variable X: => X
+[AST diff test] Variable Y: N/A
+[AST diff test] Variable c: => c
+[AST diff test] Variable f: => f
+[AST diff test] Variable with_goto_unchanged: => with_goto_unchanged
+[AST diff test] Variable x: => x
+[AST diff test] Variable c: => c
+[AST diff test] Variable g: => g
+[AST diff test] Variable has_static_local_x: => has_static_local_y
+[AST diff test] Variable __retres: => __retres
+[AST diff test] Variable h: => h
+[AST diff test] Variable use_logic_builtin: => use_logic_builtin
+[AST diff test] Variable x: => x
+[AST diff test] Variable y: => y
+[AST diff test] Variable has_static_local: => has_static_local
+[AST diff test] Variable decl: => decl
+[AST diff test] Variable used_in_decl: => used_in_decl
+[AST diff test] Variable ptr_func: => ptr_func
+[AST diff test] Function i: => i
+[AST diff test] Function local_var_use: => local_var_use
+[AST diff test] Function use_s: => use_s
+[AST diff test] Function with_goto_changed: -> with_goto_changed (body changed)
+[AST diff test] Function f: => f
+[AST diff test] Function with_goto_unchanged: => with_goto_unchanged
+[AST diff test] Function g: N/A
+[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function use_logic_builtin: => use_logic_builtin
+[AST diff test] Function has_static_local: => has_static_local
+[AST diff test] Function decl: => decl