diff --git a/.gitignore b/.gitignore
index 0d9cfe2b2ecfb4a609ee6d1c3a813c24a3756795..427a0ac8f322cd484471ce451c6c04fe80f07fcf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -30,6 +30,8 @@ frama_c_journal.ml
/distributed
_build
*.install
+*.coverage
+_coverage
# This file is generated (on need) during configure
/src/plugins/dune
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/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/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..e2c9a5d3e0a34e273c5cdc221405ebca15dcdfa4 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)
@@ -58,7 +59,8 @@
(public_name frama-c-eva.gui)
(flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9 -alert -db_deprecated)
(libraries eva frama-c.kernel frama-c.gui)
- (instrumentation (backend landmarks))))
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx))))
(plugin
(name eva-gui)
@@ -74,7 +76,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 +95,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/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index ec5701d77360ed98b54cb68bbe4b2feb4155e1e5..c077192b105b8950d252e73d590ae2d417070f36 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -37,25 +37,24 @@ class overflow =
match F.repr e with
| Fun(f,[v]) ->
let open Lang.F in
- let open Lang.N in
let min, max = Ctypes.bounds @@ Cint.to_cint f in
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 lower = p_lt v min and upper = p_lt max v in
+ let in_range = p_not (p_or lower upper) in
- let length = (max - min) + e_one in
- let overflow = min + ((v - min) mod length) in
+ let length = e_add (e_sub max min) e_one in
+ let overflow = e_add min (e_mod (e_sub v min) length) in
let replace_with v = fun u -> if u == e then v else raise Not_found in
Applicable(fun (hs,g) -> [
"In-Range",
- Conditions.subst (replace_with v) (hs , in_range ==> g) ;
+ Conditions.subst (replace_with v) (hs , p_imply in_range g) ;
"Lower",
- Conditions.subst (replace_with overflow) (hs , lower ==> g) ;
+ Conditions.subst (replace_with overflow) (hs , p_imply lower g) ;
"Upper",
- Conditions.subst (replace_with overflow) (hs , upper ==> g)
+ Conditions.subst (replace_with overflow) (hs , p_imply upper g)
])
| _ -> Not_applicable
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)))