diff --git a/.gitignore b/.gitignore
index 0d9cfe2b2ecfb4a609ee6d1c3a813c24a3756795..acdc5c997665e5661db8da87369e862623fe424f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -30,6 +30,9 @@ frama_c_journal.ml
/distributed
_build
*.install
+*.coverage
+_coverage
+_bisect
# This file is generated (on need) during configure
/src/plugins/dune
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2e7790a93c5eaf8613644d465fb0e625d541cdb7..2ff2614dc5c9652ab60434fece031bad25a8f044 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -129,36 +129,54 @@ ivette:
################################################################################
### TESTS
+.build_template: &coverage_artifacts
+ artifacts:
+ name: coverage-$CI_JOB_NAME
+ paths:
+ - _bisect/*.tar.xz
+ expire_in: 24h
+
+.build_template: &coverage
+ variables:
+ OUT: "_bisect"
+ <<: *coverage_artifacts
+
check-ts-api:
stage: tests
script:
- ./nix/build-proxy.sh ts-api
+ <<: *coverage
e-acsl-tests:
stage: tests
script:
- ./nix/build-proxy.sh e-acsl-tests
+ <<: *coverage
e-acsl-dev-tests:
stage: tests
script:
- ./nix/build-proxy.sh e-acsl-dev-tests
+ <<: *coverage
allow_failure: true
.build_template: &eva_template
stage: tests
script:
- ./nix/build-proxy.sh eva-$CONFIG-tests
+ <<: *coverage_artifacts
eva-default-tests:
variables:
CONFIG: "default"
+ OUT: "_bisect"
<<: *eva_template
.build_template: &eva_domains
parallel:
matrix:
- - CONFIG: [
+ - OUT: "_bisect"
+ CONFIG: [
"apron",
"bitwise",
"equality",
@@ -171,40 +189,24 @@ eva-default-tests:
eva-domains:
<<: *eva_template
<<: *eva_domains
- only:
- variables:
- - $CI_COMMIT_BRANCH =~ /.*[-_\/.][Ee]va[-_\/.].*/
- - $CI_COMMIT_BRANCH =~ /^[Ee]va[-_\/.].*/
- - $CI_COMMIT_BRANCH =~ /.*[-_\/.][Ee]va$/
-
-eva-domains-nightly:
- <<: *eva_template
- <<: *eva_domains
- only:
- refs:
- - schedules
-
-eva-domains-release:
- <<: *eva_template
- <<: *eva_domains
- only:
- variables:
- - $RELEASE == "yes"
kernel-tests:
stage: tests
script:
- ./nix/build-proxy.sh kernel-tests
+ <<: *coverage
plugins-tests:
stage: tests
script:
- ./nix/build-proxy.sh plugins-tests
+ <<: *coverage
wp-tests:
stage: tests
script:
- ./nix/build-proxy.sh wp-tests
+ <<: *coverage
external-plugins:
stage: tests
@@ -259,6 +261,22 @@ build-distrib-tarball:
- ./*.tar.gz
expire_in: 1 week
+# Coverage
+
+coverage:
+ stage: distrib
+ variables:
+ BISECT_DIR: "_bisect"
+ script:
+ - ./nix/shell-checkers.sh "./nix/coverage.sh"
+ coverage: '/Coverage: \d+\.\d+\%/'
+ artifacts:
+ reports:
+ coverage_report:
+ coverage_format: cobertura
+ path: report.xml
+ expire_in: 1 week
+
# Check files header
header-check:
diff --git a/bin/test.sh b/bin/test.sh
index ed3665e5275a347b93866410afd5b65b2d988038..5b2da558ae516c3a0aa2f0b98fa967eb0dd75e9e 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -32,6 +32,7 @@ LOGS=
COMMIT=
TESTS=
SAVE=
+COVER=
DUNE_ALIAS=
DUNE_OPT=
@@ -74,7 +75,8 @@ function Usage
echo " -u|--update run tests and update oracles (and WP-cache)"
echo " -s|--save save dune logs into $DUNE_LOG"
echo " -v|--verbose print executed commands"
- echo " -j|--jobs <jobs> Run no more than <jobs> commands simultaneously."
+ echo " -j|--jobs <jobs> run no more than <jobs> commands simultaneously."
+ echo " --coverage compute test coverage"
echo " -h|--help print this help"
echo ""
echo "VARIABLES"
@@ -188,6 +190,11 @@ do
CONFIG=$2
shift
;;
+ "--coverage")
+ COVER=yes
+ DUNE_OPT+="--workspace dev/dune-workspace.cover "
+ shift
+ ;;
"-n"|"--name")
ALIAS_NAME=$2
shift
@@ -265,6 +272,30 @@ function PullCache
fi
}
+# --------------------------------------------------------------------------
+# --- Coverage
+# --------------------------------------------------------------------------
+
+function PrepareCoverage
+{
+ export BISECT_FILE="$(pwd -P)/_bisect/bisect-"
+ if [ "$COVER" = "yes" ] ;
+ then
+ Cmd rm -rf _coverage
+ Cmd rm -rf _bisect
+ Cmd mkdir _bisect
+ fi
+}
+
+function GenerateCoverage
+{
+ if [ "$COVER" = "yes" ] ;
+ then
+ Head "Generating coverage in _coverage ..."
+ Cmd bisect-ppx-report html --coverage-path=_bisect
+ fi
+}
+
# --------------------------------------------------------------------------
# --- Test Suite Preparation
# --------------------------------------------------------------------------
@@ -446,10 +477,12 @@ function Status
SetEnv
PullCache
+PrepareCoverage
PrepareTests
Register $TESTS
RunAlias ${DUNE_ALIAS}
Commits ${COMMITS}
Status $DUNE_LOG
+GenerateCoverage
# --------------------------------------------------------------------------
diff --git a/dev/dune-workspace.cover b/dev/dune-workspace.cover
new file mode 100644
index 0000000000000000000000000000000000000000..86349742cd4e9d71bf7ee44ed42b70934fd3cf91
--- /dev/null
+++ b/dev/dune-workspace.cover
@@ -0,0 +1,26 @@
+(lang dune 3.2)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2023 ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(context
+ (default
+ (instrument_with bisect_ppx)))
diff --git a/nix/combinetura.nix b/nix/combinetura.nix
new file mode 100644
index 0000000000000000000000000000000000000000..723530d3a767b3d6cc482bd82ab3b2089f1c7610
--- /dev/null
+++ b/nix/combinetura.nix
@@ -0,0 +1,31 @@
+{ stdenv
+, bisect_ppx
+, dune_3
+, findlib
+, ocaml
+, ppxlib
+, xml-light
+} :
+
+stdenv.mkDerivation rec {
+ pname = "combinetura";
+ version = src.version;
+
+ src = (import ./sources.nix {}).combinetura;
+
+ buildInputs = [
+ bisect_ppx
+ dune_3
+ findlib
+ ocaml
+ xml-light
+ ];
+
+ buildPhase = ''
+ dune build @install
+ '' ;
+
+ installPhase = ''
+ dune install --prefix $out --libdir $OCAMLFIND_DESTDIR $pname --docdir $out/share/doc --mandir $out/share/man
+ '' ;
+}
diff --git a/nix/coverage.sh b/nix/coverage.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f1d8a3ea400516ee284b211301544814cc141ee7
--- /dev/null
+++ b/nix/coverage.sh
@@ -0,0 +1,44 @@
+#!/usr/bin/env sh
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2023 #
+# 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). #
+# #
+##########################################################################
+
+if [ -z ${BISECT_DIR+x} ]; then
+ echo "BISECT_DIR variable must indicate the reports directory"
+ exit 2
+fi
+
+for i in _bisect/*.tar.xz ; do
+ tar xfJ "$i" ;
+done
+
+combinetura ./*.xml -o report.xml
+
+LINE=$(sed -n '2p' report.xml)
+RATE=$(echo "$LINE" | sed -e 's/.*line-rate=\"\(.*\)\".*/\1/')
+
+PERCENT="0.0"
+if [ "$RATE" != "-nan" ]; then
+ # Keep the "/1", bc DOES NOT use scale for anything else than division ...
+ PERCENT=$(echo "scale=2; (100 * $RATE)/1" | bc -l)
+fi
+
+echo "Coverage: $PERCENT%"
diff --git a/nix/default-config-tests.nix b/nix/default-config-tests.nix
index 04f0b1bdb3dd8fc6492d23338b6dc90b1d706ba3..a3517e057a72520c946bf507c3612a1244cec3b6 100644
--- a/nix/default-config-tests.nix
+++ b/nix/default-config-tests.nix
@@ -1,9 +1,13 @@
-{ mk_tests } :
+{ mk_tests, frama-c-nocover } :
-mk_tests {
- tests-name = "default-config-tests";
+let mk_tests_distrib = mk_tests.override {
+ frama-c = frama-c-nocover ;
+}; in
+mk_tests_distrib {
+ cover = false ;
+ tests-name = "src-distrib-tests" ;
tests-command = ''
dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short @ptests_config
- '';
+ '' ;
}
diff --git a/nix/external-plugin-ci.sh b/nix/external-plugin-ci.sh
index e63d692dd76cb206d1174379c38c2645e7927815..fc1bc18392745742b4e9b3ff94e8955d9de7aa75 100755
--- a/nix/external-plugin-ci.sh
+++ b/nix/external-plugin-ci.sh
@@ -45,6 +45,11 @@ fi
# Normalize version for Nix
OCAML=${OCAML/./_}
+OUTOPT="--no-out-link"
+if [ ! -z ${OUT+x} ]; then
+ OUTOPT="-o $(pwd)/$OUT"
+fi
+
DEFAULT=${DEFAULT:-master}
# prints
@@ -118,7 +123,7 @@ if [[ -f "./nix/dependencies" ]]; then
fi
# run the build
-nix-build --no-out-link "./nix/pkgs.nix" $OPTS -A ocaml-ng.ocamlPackages_$OCAML."$plugin"
+nix-build $OUTOPT "./nix/pkgs.nix" $OPTS -A ocaml-ng.ocamlPackages_$OCAML."$plugin"
cd "$fc_dir"
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
index 6bd68e73379d6ec70d3e84673e61e84574d16a86..1456c7a6e92c47759ec74d112db5ef7ec9bee7aa 100644
--- a/nix/frama-c-checkers-shell.nix
+++ b/nix/frama-c-checkers-shell.nix
@@ -2,6 +2,7 @@
, stdenv
, black
, clang_10
+, combinetura
, frama-c-hdrck
, frama-c-lint
, git
@@ -16,6 +17,7 @@ stdenv.mkDerivation rec {
buildInputs = [
black
clang_10
+ combinetura
frama-c-hdrck
frama-c-lint
git
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 4be82fb950a17b6a28b4a09c0c8834462f96c25d..2aab3256ac2305aff99c5083713502e2d50bd60b 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -11,6 +11,7 @@
, findlib
# Frama-C build
, apron
+, bisect_ppx
, camlzip
, camomile
, dune_3
@@ -45,7 +46,7 @@
, doxygen
, python3
, python3Packages
-, yq
+, cover ? true
, release_mode ? false
}:
@@ -71,6 +72,7 @@ stdenvNoCC.mkDerivation rec {
buildInputs = [
apron
+ bisect_ppx
camlzip
camomile
dune_3
@@ -105,8 +107,6 @@ stdenvNoCC.mkDerivation rec {
dos2unix
doxygen
python3
- python3Packages.pyaml
- yq
];
outputs = [ "out" "build_dir" ];
@@ -121,11 +121,15 @@ stdenvNoCC.mkDerivation rec {
enableParallelBuilding = false;
dune_opt = if release_mode then "--release" else "" ;
- buildPhase = ''
- dune build -j2 --display short --error-reporting=twice $release_mode @install
- make tools/ptests/ptests.exe
- make tools/ptests/wtests.exe
- '';
+ buildPhase = (if cover then ''
+ export DUNE_WORKSPACE="dev/dune-workspace.cover"
+ '' else "") +
+ ''
+ dune build -j2 --display short --error-reporting=twice $dune_opt @install
+
+ make tools/ptests/ptests.exe
+ make tools/ptests/wtests.exe
+ '';
installFlags = [
"PREFIX=$(out)"
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index d56dc7155dc3a698acb0d594c8197a887c152761..1754f291e51b51d27fbae62bca47c0477643e129 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -26,6 +26,7 @@
, stdenvNoCC
, time
, unixtools
+, yq
, which
, wp-cache
} :
@@ -33,6 +34,7 @@
{ tests-name
, tests-command
, has-wp-proofs ? false
+, cover ? true
} :
stdenvNoCC.mkDerivation {
@@ -49,6 +51,7 @@ stdenvNoCC.mkDerivation {
perl
time
unixtools.getopt
+ yq
which
] ++
(if has-wp-proofs then [ alt-ergo ] else []);
@@ -68,14 +71,29 @@ stdenvNoCC.mkDerivation {
else "" ;
preBuild =
- if has-wp-proofs
+ (if has-wp-proofs
+ then ''
+ mkdir home
+ HOME=$(pwd)/home
+ why3 config detect
+ export FRAMAC_WP_CACHE=offline
+ export FRAMAC_WP_CACHEDIR=$wp_cache
+ ''
+ else "") +
+ (if cover
+ then ''
+ mkdir -p _bisect
+ export DUNE_WORKSPACE="dev/dune-workspace.cover"
+ export BISECT_FILE="$(pwd)/_bisect/bisect-"
+ ''
+ else "");
+
+ postBuild =
+ if cover
then ''
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- export FRAMAC_WP_CACHE=offline
- export FRAMAC_WP_CACHEDIR=$wp_cache
- ''
+ bisect-ppx-report cobertura --coverage-path=_bisect coverage-$pname.xml
+ tar cfJ coverage.tar.xz coverage-$pname.xml
+ ''
else "" ;
buildPhase = ''
@@ -86,7 +104,13 @@ stdenvNoCC.mkDerivation {
'';
# No installation required
- installPhase = ''
- touch $out
- '';
+ installPhase =
+ if cover
+ then ''
+ mkdir -p $out
+ cp -r coverage.tar.xz $out/$pname.tar.xz
+ ''
+ else ''
+ touch $out
+ '';
}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 8f08f15e2ed2c3ad9c9f176c69dd830e48dae2a3..69ec600c6a00dace82ffa98d0b4dbd1a110a69ed 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -4,6 +4,7 @@ let
# External Packages
alt-ergo = oself.callPackage ./alt-ergo.nix {};
camlp5 = oself.callPackage ./camlp5.nix {};
+ combinetura = oself.callPackage ./combinetura.nix {};
headache = oself.callPackage ./headache.nix {};
mlmpfr = oself.callPackage ./mlmpfr.nix {};
why3 = oself.callPackage ./why3.nix {};
@@ -23,11 +24,16 @@ let
# Builds
frama-c = oself.callPackage ./frama-c.nix {};
+ frama-c-no-cover = oself.callPackage ./frama-c.nix { cover = false ; };
frama-c-hdrck = oself.callPackage ./frama-c-hdrck.nix {};
frama-c-lint = oself.callPackage ./frama-c-lint.nix {};
# Tests
- default-config-tests = oself.callPackage ./default-config-tests.nix {};
+ default-config-tests = oself.callPackage ./default-config-tests.nix {
+ frama-c-nocover = oself.frama-c.override {
+ cover = false ;
+ } ;
+ };
e-acsl-tests = oself.callPackage ./e-acsl-tests.nix { config = ""; };
e-acsl-dev-tests = oself.callPackage ./e-acsl-tests.nix { config = "dev"; };
eva-default-tests = oself.callPackage ./eva-tests.nix { config = ""; };
@@ -52,7 +58,10 @@ let
api-doc = oself.callPackage ./api-doc.nix {};
manuals = oself.callPackage ./manuals.nix {};
src-distrib-tests = oself.callPackage ./src-distrib-tests.nix {
- frama-c-release = oself.frama-c.override { release_mode = true ; } ;
+ frama-c-release = oself.frama-c.override {
+ release_mode = true ;
+ cover = false ;
+ } ;
};
};
overlay = self: super: {
diff --git a/nix/sources.json b/nix/sources.json
index f3366def7224ddf86cc72dba0203100ae2053299..085757d6bd1478f3e88eefa4b4365d295a2e8018 100644
--- a/nix/sources.json
+++ b/nix/sources.json
@@ -41,5 +41,12 @@
"rev": "49c0c5193ef945f1a3dca30b59fa093a7b43437d",
"type": "git",
"version": "1.6.0"
+ },
+ "combinetura": {
+ "branch": "master",
+ "repo": "git@git.frama-c.com:dev/combinetura.git",
+ "rev": "7e44888e80c34d560da20a220c0ac1ab2126ff0f",
+ "type": "git",
+ "version": "0.0"
}
}
diff --git a/nix/src-distrib-tests.nix b/nix/src-distrib-tests.nix
index 6655a194c4c6f36aad1c92c81b8da5b2791ca13d..dba013d7aef295da3685b67372136d8dc9d1643d 100644
--- a/nix/src-distrib-tests.nix
+++ b/nix/src-distrib-tests.nix
@@ -4,9 +4,10 @@ let mk_tests_distrib = mk_tests.override {
frama-c = frama-c-release ;
}; in
mk_tests_distrib {
- tests-name = "src-distrib-tests";
+ cover = false ;
+ tests-name = "src-distrib-tests" ;
tests-command = ''
dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
dune build -j1 --display short @ptests_config
- '';
+ '' ;
}
diff --git a/nix/ts-api.nix b/nix/ts-api.nix
index cda9f980c8d6ef7811f8976bf361654e0af80dc8..5d181a1a77828c79abb308442b8edd916786354d 100644
--- a/nix/ts-api.nix
+++ b/nix/ts-api.nix
@@ -28,11 +28,16 @@ stdenv.mkDerivation rec {
'';
buildPhase = ''
+ mkdir coverage
+ export BISECT_FILE="$(pwd)/coverage/bisect-"
make -C ivette check-api
+ bisect-ppx-report cobertura --coverage-path=coverage coverage-$pname.xml
+ tar cfJ coverage.tar.xz coverage-$pname.xml
'';
# No installation required
installPhase = ''
- touch $out
+ mkdir -p $out
+ cp -r coverage.tar.xz $out/$pname.tar.xz
'';
}
diff --git a/src/dune b/src/dune
index 7cd55aa0b825af3628b942e63f2e0b5503c955a6..1df313dfe3b14cf5b89e8942fcd3e73b1a2e9e23 100644
--- a/src/dune
+++ b/src/dune
@@ -52,6 +52,7 @@
(flags :standard -w -9)
(libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
(preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
)
diff --git a/src/init/boot/dune b/src/init/boot/dune
index 99571de6546a5b56beee1f7079c5265df19a5a5c..ad7b0ab70d1895b2764e5ff15d5cb53d75b5908d 100644
--- a/src/init/boot/dune
+++ b/src/init/boot/dune
@@ -27,6 +27,7 @@
(flags :standard -open Frama_c_kernel)
(libraries frama_c_kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
diff --git a/src/init/dune b/src/init/dune
index 9187a431dcf969479cd4d5566c7051c1c3160604..a10c21f55224ee9e780edbeabc855b0485c31c70 100644
--- a/src/init/dune
+++ b/src/init/dune
@@ -27,6 +27,7 @@
(virtual_modules gui_init)
(libraries threads)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(include_subdirs no)
diff --git a/src/init/impl_cmdline/dune b/src/init/impl_cmdline/dune
index 7e8d680abd9dec1ca815acce0930ae1238b48d3b..8467d8184fb4ea1c1b03335fa14fdc66d408cfd4 100644
--- a/src/init/impl_cmdline/dune
+++ b/src/init/impl_cmdline/dune
@@ -25,4 +25,5 @@
(public_name frama-c.init.cmdline)
(implements frama-c.init)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index 1e48cad2696860e219610e9ed5df536a8fdd9c78..583d47d1811e751e5e3a1aa9069b11edd55144e8 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -77,8 +77,8 @@ struct
let is_included is_included x y =
match x, y with
- | `Bottom, _ | _, `Top -> true
- | _, `Bottom | `Top, _ -> false
+ | `Bottom, #or_top_bottom | #or_top_bottom, `Top -> true
+ | #or_top_bottom, `Bottom | `Top, #or_top_bottom -> false
| `Value vx, `Value vy -> is_included vx vy
(* Iterator *)
@@ -142,7 +142,7 @@ module Bottom = struct
let zip x y =
match x, y with
- | `Bottom, _ | _, `Bottom -> `Bottom
+ | `Bottom, #t | #t, `Bottom -> `Bottom
| `Value x, `Value y -> `Value (x,y)
(** Conversion *)
@@ -265,7 +265,7 @@ struct
let zip x y =
match x, y with
- | `Top, _ | _, `Top -> `Top
+ | `Top, #t | #t, `Top -> `Top
| `Value x, `Value y -> `Value (x,y)
(** Conversion. *)
@@ -327,8 +327,8 @@ struct
let zip x y =
match x, y with
- | `Bottom, _ | _, `Bottom -> `Bottom
- | `Top, _ | _, `Top -> `Top
+ | `Bottom, #t | #t, `Bottom -> `Bottom
+ | `Top, #t | #t, `Top -> `Top
| `Value x, `Value y -> `Value (x,y)
(** Operators *)
diff --git a/src/plugins/alias/dune b/src/plugins/alias/dune
index 63d49ab5cc95c628ad7d0cf25789504a89d9b823..480ffb1277133e4926f5ed26129715b08d444246 100644
--- a/src/plugins/alias/dune
+++ b/src/plugins/alias/dune
@@ -36,6 +36,7 @@
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel ocamlgraph unionFind)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
( plugin
diff --git a/src/plugins/aorai/dune b/src/plugins/aorai/dune
index 8c8a1eba3314648a79347cf1b4bab0fa271673dc..23a75aa916fa376e4efa41337af9660a2f21ed6c 100644
--- a/src/plugins/aorai/dune
+++ b/src/plugins/aorai/dune
@@ -45,6 +45,7 @@
)
)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(ocamllex yalexer)
diff --git a/src/plugins/api-generator/dune b/src/plugins/api-generator/dune
index 3d7931417a1a98e8aef73b922cac820a6b0a1e51..204f73e2bd785ba731bef1db9669eb1cd52f34a6 100644
--- a/src/plugins/api-generator/dune
+++ b/src/plugins/api-generator/dune
@@ -26,6 +26,7 @@
(public_name frama-c-api-generator.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-server.core)
-)
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx)))
(plugin (optional) (name api_generator) (libraries frama-c-api-generator.core) (site (frama-c plugins)))
diff --git a/src/plugins/callgraph/dune b/src/plugins/callgraph/dune
index b1ad818441d91a05e9a224d85cdaf1c7a1eafc3d..64ffc157d4cd564cc6a03a431dc2bb2bebec8694 100644
--- a/src/plugins/callgraph/dune
+++ b/src/plugins/callgraph/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins)))
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index 048101730ad1607edc551bee7a59fefadc666fdb..408db9a7f9c8ab6a5cb2a4ed63f7de52661cc153 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name constant_propagation) (libraries frama-c-constant_propagation.core) (site (frama-c plugins)))
diff --git a/src/plugins/dive/dune b/src/plugins/dive/dune
index 85e0415bdd0ea3cd1484f0b6c5c04e6743c857a4..a2c5d6b6e7e3fbb850f98f329704608a7b5db953 100644
--- a/src/plugins/dive/dune
+++ b/src/plugins/dive/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-studia.core frama-c-server.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name dive) (libraries frama-c-dive.core) (site (frama-c plugins)))
diff --git a/src/plugins/e-acsl/src/dune b/src/plugins/e-acsl/src/dune
index ee4a92ec6045a32ec7cc70b1b63644a466c93e38..a46349bec0d4c72f5625e42bd2361fc015b8edb7 100644
--- a/src/plugins/e-acsl/src/dune
+++ b/src/plugins/e-acsl/src/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-rtegen.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins)))
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index a5aae82cd3584e41c471019a26e2bfd4477b48c1..589387e2eda9f3eec9800160bc5a89a1b7dd86fd 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -40,7 +40,8 @@
(public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
(libraries frama-c.kernel frama-c-server.core)
- (instrumentation (backend landmarks)))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx)))
(plugin
(name eva)
@@ -74,7 +75,8 @@
(public_name frama-c-eva.numerors.core)
(flags -open Frama_c_kernel -open Eva__Private :standard)
(libraries frama-c.kernel frama-c-eva.core mlmpfr)
- (instrumentation (backend landmarks))))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))))
(plugin
(name eva.numerors)
@@ -92,7 +94,8 @@
(libraries
frama-c.kernel frama-c-eva.core
apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)
- (instrumentation (backend landmarks))))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))))
(plugin
(name eva.apron)
diff --git a/src/plugins/from/dune b/src/plugins/from/dune
index 649a080ec4f499857fd6e2178031d85c6b19da56..1f4eab52cb87d4906ba5ec6760a46e7ab3416fc9 100644
--- a/src/plugins/from/dune
+++ b/src/plugins/from/dune
@@ -39,6 +39,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name from) (libraries frama-c-from.core) (site (frama-c plugins)))
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 8bd94fb058126db9ae356f0ef7b36b74197afc9a..418b94fb5eb56c55e22551ccddcb85f2a336d41b 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -41,6 +41,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.core frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
diff --git a/src/plugins/inout/dune b/src/plugins/inout/dune
index 1029fd27994ec0c1a67c497a521b3bac50572b90..9ed847d58dca23a18a7d18af687751c14a0516aa 100644
--- a/src/plugins/inout/dune
+++ b/src/plugins/inout/dune
@@ -39,6 +39,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-from.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name inout) (libraries frama-c-inout.core) (site (frama-c plugins)))
diff --git a/src/plugins/instantiate/dune b/src/plugins/instantiate/dune
index 61f0edbbea34f20a3a0fb38815f5510506feae54..d98fd93169c94947cde040c491a98b5bbf077b8f 100644
--- a/src/plugins/instantiate/dune
+++ b/src/plugins/instantiate/dune
@@ -36,6 +36,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name instantiate) (libraries frama-c-instantiate.core) (site (frama-c plugins)))
diff --git a/src/plugins/loop_analysis/dune b/src/plugins/loop_analysis/dune
index 178b00973e557e2fa7c0a05be661e70f77132072..266477032f1b50f9c79653a9cdc2fb5f62b56285 100644
--- a/src/plugins/loop_analysis/dune
+++ b/src/plugins/loop_analysis/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name loop-analysis) (libraries frama-c-loop-analysis.core) (site (frama-c plugins)))
diff --git a/src/plugins/markdown-report/dune b/src/plugins/markdown-report/dune
index d09f77429709bca371b79c73a81d15cf917eefce..58cf7b1d43bef21c0612178cb7d08fa0c0976c03 100644
--- a/src/plugins/markdown-report/dune
+++ b/src/plugins/markdown-report/dune
@@ -38,6 +38,7 @@
(libraries frama-c.kernel)
(preprocess (pps ppx_deriving_yojson))
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name markdown-report) (libraries frama-c-markdown-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/markdown-report/eva-info/dune b/src/plugins/markdown-report/eva-info/dune
index 9d6d8395828a835e90f551da4f67067e54d5a970..6ea5596e04945496f2818323c29efe9eccbc50d5 100644
--- a/src/plugins/markdown-report/eva-info/dune
+++ b/src/plugins/markdown-report/eva-info/dune
@@ -39,6 +39,7 @@
(libraries frama-c.kernel frama-c-eva.core frama-c-markdown-report.core)
(preprocess (pps ppx_deriving_yojson))
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name markdown-report.eva-info) (libraries frama-c-markdown-report.eva-info.core) (site (frama-c plugins)))
diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune
index 04d94b067045dc9f4ce57d07191df87c7e464fea..4dc059de651db28f1581bd40ae537a6cf138426e 100644
--- a/src/plugins/metrics/dune
+++ b/src/plugins/metrics/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-server.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name metrics) (libraries frama-c-metrics.core) (site (frama-c plugins)))
diff --git a/src/plugins/nonterm/dune b/src/plugins/nonterm/dune
index b2273574bbbeb269cdc2ede7e4322982695fc689..7e65237e8986219f0a311538851bdc3a4384a11e 100644
--- a/src/plugins/nonterm/dune
+++ b/src/plugins/nonterm/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name nonterm) (libraries frama-c-nonterm.core) (site (frama-c plugins)))
diff --git a/src/plugins/obfuscator/dune b/src/plugins/obfuscator/dune
index 94ea79b5e98427298d0f43ab58249671f0c8d229..af464f3364cc4bac758598800e7131ac1bc3dd4f 100644
--- a/src/plugins/obfuscator/dune
+++ b/src/plugins/obfuscator/dune
@@ -36,6 +36,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name obfuscator) (libraries frama-c-obfuscator.core) (site (frama-c plugins)))
diff --git a/src/plugins/occurrence/dune b/src/plugins/occurrence/dune
index e7364f769a2319955e666378d4c9c6917417c6e8..7afdbd4ac8aa78b9fcbd3644fc93d5d1eae028f4 100644
--- a/src/plugins/occurrence/dune
+++ b/src/plugins/occurrence/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 863c56b6e2de6a019d56b95e83fc21c8796e79c7..ef59c0a573c37994967fd9f8d327eab5ed11d0a3 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -40,6 +40,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.types.core frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index 78bb8e11e3ebf71e1b64a21afdb6fbb040d8e047..6bcbe0cb1c77ffa55fccff8c6b57d6008edd4550 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/qed/dune b/src/plugins/qed/dune
index 2bac3d85858e21bf3acda8ff8f9d9449f11c00b0..7ab708cff07c260474742704375c3c6a9b320795 100644
--- a/src/plugins/qed/dune
+++ b/src/plugins/qed/dune
@@ -33,4 +33,5 @@
(public_name qed)
(flags (-open Frama_c_kernel :standard -w -9))
(libraries frama-c.kernel zarith)
- (instrumentation (backend landmarks)))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx)))
diff --git a/src/plugins/reduc/dune b/src/plugins/reduc/dune
index d95065487687c848e13aa3654a64d4a1ece01952..5e988de32a89f062c6fde4eb0285e4f700f18bfa 100644
--- a/src/plugins/reduc/dune
+++ b/src/plugins/reduc/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-inout.core frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name reduc) (libraries frama-c-reduc.core) (site (frama-c plugins)))
diff --git a/src/plugins/report/dune b/src/plugins/report/dune
index e0d6da734381d40aff29038564b6118251c0357c..d13c79cc7ed3e19086fcaa781a50577073f8b505 100644
--- a/src/plugins/report/dune
+++ b/src/plugins/report/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name report) (libraries frama-c-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune
index d2ef8a04f8c50435c80e13ae42a28a7b1fea6d8a..d6212e907f0118c6f328dab14883bc8d3a2ef3cd 100644
--- a/src/plugins/rte/dune
+++ b/src/plugins/rte/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name rtegen) (libraries frama-c-rtegen.core) (site (frama-c plugins)))
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 874c095e96cdafb17a43b2adba8a5ae42d075bd2..8bcbfda8750ecf4a2e6731d2634c909d1b208aa0 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -39,6 +39,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-inout.core frama-c-pdg.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index e214e44e80cd92c233b339643d2cc1090a39b286..c54b7cb8820d41975d354c8e2fac3c62038ebaca 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-pdg.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/server/dune b/src/plugins/server/dune
index 685cbacd1796d8ab5da67e7edaa70d1382c9ae8b..ff5efd4e2cad124c23a78a44bee412679689cf7e 100644
--- a/src/plugins/server/dune
+++ b/src/plugins/server/dune
@@ -41,6 +41,7 @@
( -> server_zmq.ko.ml)
))
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name server) (libraries frama-c-server.core) (site (frama-c plugins)))
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index a8c8753b1072312a5a538df7da1ac428dc8c9f1f..23df7d7c78f22a6323af17e578fa353b4e35501a 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name slicing) (libraries frama-c-slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/sparecode/dune b/src/plugins/sparecode/dune
index 5764630f5cf926628b7514a8030da150a8751252..24bba5862e67904a689a51d4e4a8c46a50102954 100644
--- a/src/plugins/sparecode/dune
+++ b/src/plugins/sparecode/dune
@@ -41,6 +41,7 @@
(flags :standard -open Frama_c_kernel)
(libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core frama-c-inout.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins)))
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index 841fcb9550f3922a0d4536be9475fbce65455deb..cb4cc468ce98a2b7a1559a7a72c75b9eebbaa98d 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-eva.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name studia) (libraries frama-c-studia.core) (site (frama-c plugins)))
diff --git a/src/plugins/users/dune b/src/plugins/users/dune
index 0f48402bedaf7da2495be36d1369f37df0ef1cd9..3bdf049483ba12ae10818bb061766d9c25538f91 100644
--- a/src/plugins/users/dune
+++ b/src/plugins/users/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-callgraph.core)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name users) (libraries frama-c-users.core) (site (frama-c plugins)))
diff --git a/src/plugins/variadic/dune b/src/plugins/variadic/dune
index fbd5f8dbde83ed0c866fb59ce32044f914f58926..573b69bdd08ee569948ed1bca825c221d5fd749a 100644
--- a/src/plugins/variadic/dune
+++ b/src/plugins/variadic/dune
@@ -36,6 +36,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))
)
(plugin (optional) (name variadic) (libraries frama-c-variadic.core) (site (frama-c plugins)))
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index e136f5b7960e00efa2cff1568f989eeca8077b4b..898e9209ba48c126c8e7cb0b384abc7066a3a183 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -908,7 +908,7 @@ open F
module N = struct
let ( + ) = e_add
- let ( ~- ) x = e_sub e_zero x
+ let ( ~-: ) x = e_sub e_zero x
let ( - ) = e_sub
let ( * ) = e_mul
let ( / ) = e_div
@@ -922,8 +922,8 @@ module N = struct
let ( <> ) = p_neq
let ( ==> ) = p_imply
- let ( && ) = p_and
- let ( || ) = p_or
+ let ( &&: ) = p_and
+ let ( ||: ) = p_or
let not = p_not
let ( $ ) = e_fun
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index bdb9af7a61b4e6c6f276457c569557b77e7f8a46..273b3dd5fde4e2060c0740435bc10874ffc4bff8 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -575,8 +575,11 @@ module N: sig
val ( - ): F.binop
(** {! F.p_sub } *)
- val ( ~- ): F.unop
- (** [fun x -> p_sub 0 x] *)
+ val ( ~-: ): F.unop
+ (** [fun x -> p_sub 0 x]
+ Beware that the operator does not have the same precedence as [~-] in
+ standard OCaml.
+ *)
val ( * ): F.binop
(** {! F.p_mul} *)
@@ -610,11 +613,17 @@ module N: sig
val ( ==> ): F.operator
(** {! F.p_imply } *)
- val ( && ): F.operator
- (** {! F.p_and } *)
-
- val ( || ): F.operator
- (** {! F.p_or } *)
+ val ( &&: ): F.operator
+ (** {! F.p_and }
+ Beware that the operator does not have the same precedence as [&&]
+ in standard OCaml.
+ *)
+
+ val ( ||: ): F.operator
+ (** {! F.p_or }
+ Beware that the operator does not have the same precedence as [||]
+ in standard OCaml.
+ *)
val not: F.pred -> F.pred
(** {! F.p_not } *)
diff --git a/src/plugins/wp/TacModMask.ml b/src/plugins/wp/TacModMask.ml
index 2eb2b7d7a790ca8d28cf3581f6f4ab5e1121acb9..c2e7cd09ba2e358847157112f9845f147ca124c0 100644
--- a/src/plugins/wp/TacModMask.ml
+++ b/src/plugins/wp/TacModMask.ml
@@ -78,9 +78,9 @@ class modmask =
let power_of_2 =
let v = Lang.freshvar ~basename:"n" Lang.t_int in
let tv = e_var v in
- p_exists [v] (e_zero <= tv && m = Cint.l_lsl e_one tv)
+ p_exists [v] ((e_zero <= tv) &&: (m = Cint.l_lsl e_one tv))
in
- let cond = (a >= e_zero && e_zero < m && power_of_2) in
+ let cond = ((a >= e_zero) &&: (e_zero < m) &&: power_of_2) in
let n = Cint.l_and a (m - e_one) in
update_display ~hard:true ~active_field:false ;
@@ -106,9 +106,10 @@ class modmask =
let plus_1_power_of_2 =
let v = Lang.freshvar ~basename:"n" Lang.t_int in
let tv = e_var v in
- p_exists [v] (e_zero <= tv && m + e_one = Cint.l_lsl e_one tv)
+ p_exists [v] (e_zero <= tv &&: (m + e_one = Cint.l_lsl e_one tv))
in
- let cond = (a >= e_zero && e_zero <= m && plus_1_power_of_2) in
+ let cond =
+ ((a >= e_zero) &&: (e_zero <= m) &&: (plus_1_power_of_2)) in
let n = a mod (m + e_one) in
update_display ~hard:true ~active_field:true ;
diff --git a/src/plugins/wp/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index ec5701d77360ed98b54cb68bbe4b2feb4155e1e5..c28c055e8728f1793bed1d114fd0d559d22429c7 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -42,7 +42,7 @@ class overflow =
let min, max = e_zint min, e_zint max in
let lower = v < min and upper = max < v in
- let in_range = not (lower || upper) in
+ let in_range = not (lower ||: upper) in
let length = (max - min) + e_one in
let overflow = min + ((v - min) mod length) in
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 286e356130a20349b6cc7a1a80c1bf77f6b760ef..b72a5d06e70472b3b918bb63ef6dd8b10de5dcce 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -44,7 +44,8 @@
(select wp_eva.ml from
(frama-c-eva.core -> wp_eva.enabled.ml)
( -> wp_eva.disabled.ml)))
- (instrumentation (backend landmarks)))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx)))
(plugin (optional) (name wp) (libraries frama-c-wp.core) (site (frama-c plugins)))