From d5ad375d562588a484a83a15d5ce32135fedb33a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 13 Jul 2023 15:44:34 +0200
Subject: [PATCH] [dune] add coverage build
---
.gitignore | 2 ++
dev/dune-workspace.cover | 26 +++++++++++++++++++
src/dune | 1 +
src/init/boot/dune | 1 +
src/init/dune | 1 +
src/init/impl_cmdline/dune | 1 +
.../abstract_interp/lattice_bounds.ml | 12 ++++-----
src/plugins/alias/dune | 1 +
src/plugins/aorai/dune | 1 +
src/plugins/callgraph/dune | 1 +
src/plugins/constant_propagation/dune | 1 +
src/plugins/dive/dune | 1 +
src/plugins/e-acsl/src/dune | 1 +
src/plugins/eva/dune | 12 ++++++---
src/plugins/from/dune | 1 +
src/plugins/impact/dune | 1 +
src/plugins/inout/dune | 1 +
src/plugins/instantiate/dune | 1 +
src/plugins/loop_analysis/dune | 1 +
src/plugins/markdown-report/dune | 1 +
src/plugins/markdown-report/eva-info/dune | 1 +
src/plugins/metrics/dune | 1 +
src/plugins/nonterm/dune | 1 +
src/plugins/obfuscator/dune | 1 +
src/plugins/occurrence/dune | 1 +
src/plugins/pdg/dune | 1 +
src/plugins/postdominators/dune | 1 +
src/plugins/qed/dune | 3 ++-
src/plugins/reduc/dune | 1 +
src/plugins/report/dune | 1 +
src/plugins/rte/dune | 1 +
src/plugins/scope/dune | 1 +
src/plugins/security_slicing/dune | 1 +
src/plugins/server/dune | 1 +
src/plugins/slicing/dune | 1 +
src/plugins/sparecode/dune | 1 +
src/plugins/studia/dune | 1 +
src/plugins/users/dune | 1 +
src/plugins/variadic/dune | 1 +
src/plugins/wp/TacOverflow.ml | 15 +++++------
src/plugins/wp/dune | 3 ++-
41 files changed, 87 insertions(+), 20 deletions(-)
create mode 100644 dev/dune-workspace.cover
diff --git a/.gitignore b/.gitignore
index 0d9cfe2b2ec..427a0ac8f32 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 00000000000..86349742cd4
--- /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 7cd55aa0b82..1df313dfe3b 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 99571de6546..ad7b0ab70d1 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 9187a431dcf..a10c21f5522 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 7e8d680abd9..8467d8184fb 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 1e48cad2696..583d47d1811 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 63d49ab5cc9..480ffb12771 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 8c8a1eba331..23a75aa916f 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 b1ad818441d..64ffc157d4c 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 048101730ad..408db9a7f9c 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 85e0415bdd0..a2c5d6b6e7e 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 ee4a92ec604..a46349bec0d 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 a5aae82cd35..e2c9a5d3e0a 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 649a080ec4f..1f4eab52cb8 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 8bd94fb0581..418b94fb5eb 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 1029fd27994..9ed847d58dc 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 61f0edbbea3..d98fd93169c 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 178b00973e5..266477032f1 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 d09f7742970..58cf7b1d43b 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 9d6d8395828..6ea5596e049 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 04d94b06704..4dc059de651 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 b2273574bbb..7e65237e898 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 94ea79b5e98..af464f3364c 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 e7364f769a2..7afdbd4ac8a 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 863c56b6e2d..ef59c0a573c 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 78bb8e11e3e..6bcbe0cb1c7 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 2bac3d85858..7ab708cff07 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 d9506548768..5e988de32a8 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 e0d6da73438..d13c79cc7ed 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 d2ef8a04f8c..d6212e907f0 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 874c095e96c..8bcbfda8750 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 e214e44e80c..c54b7cb8820 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 685cbacd179..ff5efd4e2ca 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 a8c8753b107..23df7d7c78f 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 5764630f5cf..24bba5862e6 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 841fcb9550f..cb4cc468ce9 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 0f48402beda..3bdf049483b 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 fbd5f8dbde8..573b69bdd08 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 ec5701d7736..c077192b105 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 286e356130a..b72a5d06e70 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)))
--
GitLab