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/kernel_services/abstract_interp/value_types.mli b/src/kernel_services/abstract_interp/value_types.mli
deleted file mode 100644
index 811e97b24fd8645dacd03b2224d5186e007f8c6a..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/value_types.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Declarations that are useful for plugins written on top of the results
- of Value. *)
-
-type 'a callback_result =
- | Normal of 'a
- | NormalStore of 'a * int
- | Reuse of int
-
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
-(** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
-
-(** Dependencies for the evaluation of a term or a predicate: for each
- program point involved, sets of zones that must be read *)
-type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 2cbd4c86ed67b863730b680daac78bcc60029fc0..1da9ccf2e15d1e4cc7265d5ca0a464811ce1d474 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -319,20 +319,6 @@ module Value = struct
((i land mask_then) <> 0, (i land mask_else) <> 0)
with Not_found -> false, false
- module RecursiveCallsFound =
- State_builder.Set_ref
- (Kernel_function.Set)
- (struct
- let name = "Db.Value.RecursiveCallsFound"
- let dependencies = only_self
- end)
-
- let ignored_recursive_call kf =
- RecursiveCallsFound.mem kf
-
- let recursive_call_occurred kf =
- RecursiveCallsFound.add kf
-
module Called_Functions_By_Callstack =
State_builder.Hashtbl(Kernel_function.Hashtbl)
(States_by_callstack)
@@ -369,54 +355,6 @@ module Value = struct
Cvalue.Model.pretty v)
*)
- module Record_Value_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Record_Value_Callbacks_New =
- Hook.Build
- (struct
- type t =
- callstack *
- ((state Stmt.Hashtbl.t) Lazy.t * (state Stmt.Hashtbl.t) Lazy.t)
- Value_types.callback_result
- end)
-
- module Record_Value_After_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Record_Value_Superposition_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state list Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Call_Value_Callbacks =
- Hook.Build
- (struct type t = state * callstack end)
-
- module Call_Type_Value_Callbacks =
- Hook.Build(struct
- type t = [`Builtin | `Spec
- | `Body | `Reuse]
- * state * callstack end)
- ;;
-
-
- module Compute_Statement_Callbacks =
- Hook.Build
- (struct type t = stmt * callstack * state list end)
-
- (* -remove-redundant-alarms feature, applied at the end of an Eva analysis,
- fulfilled by the Scope plugin that also depends on Eva. We thus use a
- reference here to avoid a cyclic dependency. *)
- let rm_asserts = mk_fun "Value.rm_asserts"
-
let no_results = mk_fun "Value.no_results"
let update_callstack_table ~after stmt callstack v =
@@ -476,10 +414,6 @@ module Value = struct
try Some (Called_Functions_By_Callstack.find kf)
with Not_found -> None
- let valid_behaviors = mk_fun "Value.get_valid_behaviors"
-
- let add_formals_to_state = mk_fun "add_formals_to_state"
-
let get_fundec_from_stmt stmt =
let kf =
try
@@ -536,18 +470,6 @@ module Value = struct
Table_By_Callstack.find stmt)
with Not_found -> None
- let fold_stmt_state_callstack f acc ~after stmt =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match get_stmt_state_callstack ~after stmt with
- | None -> acc
- | Some h -> Eva_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
-
- let fold_state_callstack f acc ~after ki =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- match ki with
- | Kglobal -> f (globals_state ()) acc
- | Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
-
let is_reachable = Cvalue.Model.is_reachable
exception Is_reachable
@@ -572,116 +494,8 @@ module Value = struct
| Kglobal -> Cvalue.Model.is_reachable (globals_state ())
| Kstmt stmt -> is_reachable_stmt stmt
- let is_called = mk_fun "Value.is_called"
- let callers = mk_fun "Value.callers"
-
- let access_location = mk_fun "Value.access_location"
-
- let find state loc = Cvalue.Model.find state loc
-
- let access = mk_fun "Value.access"
- let access_expr = mk_fun "Value.access_expr"
-
- let use_spec_instead_of_definition =
- mk_fun "Value.use_spec_instead_of_definition"
-
- let eval_lval =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_lval")
- let eval_expr =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_expr")
-
- let eval_expr_with_state =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_expr_with_state")
-
- let reduce_by_cond = mk_fun "Value.reduce_by_cond"
-
- let find_lv_plus = mk_fun "Value.find_lv_plus"
-
- let pretty_state = Cvalue.Model.pretty
-
- let pretty = Cvalue.V.pretty
-
let compute = mk_fun "Value.compute"
- let memoize = mk_fun "Value.memoize"
- let expr_to_kernel_function = mk_fun "Value.expr_to_kernel_function"
- let expr_to_kernel_function_state =
- mk_fun "Value.expr_to_kernel_function_state"
-
- exception Not_a_call
-
- let call_to_kernel_function call_stmt = match call_stmt.skind with
- | Instr (Call (_, fexp, _, _)) ->
- let _, called_functions =
- !expr_to_kernel_function ?with_alarms:None ~deps:None
- (Kstmt call_stmt) fexp
- in called_functions
- | Instr(Local_init(_, ConsInit(f,_,_),_)) ->
- Kernel_function.Hptset.singleton (Globals.Functions.get f)
- | _ -> raise Not_a_call
-
-
- let lval_to_loc_with_deps = mk_fun "Value.lval_to_loc_with_deps"
- let lval_to_loc_with_deps_state = mk_fun "Value.lval_to_loc_with_deps_state"
- let lval_to_loc = mk_fun "Value.lval_to_loc"
- let lval_to_offsetmap = mk_fun "Value.lval_to_offsetmap"
- let lval_to_offsetmap_state = mk_fun "Value.lval_to_offsetmap_state"
- let lval_to_loc_state = mk_fun "Value.lval_to_loc_state"
- let lval_to_zone = mk_fun "Value.lval_to_zone"
- let lval_to_zone_state = mk_fun "Value.lval_to_zone_state"
- let lval_to_zone_with_deps_state = mk_fun "Value.lval_to_zone_with_deps_state"
- let lval_to_precise_loc_state =
- ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.lval_to_precise_loc")
- let lval_to_precise_loc_with_deps_state =
- mk_fun "Value.lval_to_precise_loc_with_deps_state"
- let assigns_inputs_to_zone = mk_fun "Value.assigns_inputs_to_zone"
- let assigns_outputs_to_zone = mk_fun "Value.assigns_outputs_to_zone"
- let assigns_outputs_to_locations = mk_fun "Value.assigns_outputs_to_locations"
- let verify_assigns_froms = mk_fun "Value.verify_assigns_froms"
-
- module Logic = struct
- let eval_predicate =
- ref (fun ~pre:_ ~here:_ _ ->
- raise
- (Extlib.Unregistered_function
- "Function 'Value.Logic.eval_predicate' not registered yet"))
-
- end
-
- exception Void_Function
-
- let find_return_loc kf =
- try
- let ki = Kernel_function.find_return kf in
- let lval = match ki with
- | { skind = Return (Some ({enode = Lval ((_ , offset) as lval)}), _) }
- ->
- assert (offset = NoOffset) ;
- lval
- | { skind = Return (None, _) } -> raise Void_Function
- | _ -> assert false
- in
- !lval_to_loc (Kstmt ki) ?with_alarms:None lval
- with Kernel_function.No_Statement ->
- (* [JS 2011/05/17] should be better to have another name for this
- exception or another one since it is possible to have no return without
- returning void (the case when the kf corresponds to a declaration *)
- raise Void_Function
-
- let display = mk_fun "Value.display"
-
- let emitter = ref Emitter.dummy
-
-end
-
-module From = struct
- exception Not_lval
-
- let find_deps_no_transitivity = mk_fun "From.find_deps_no_transitivity"
- let find_deps_no_transitivity_state =
- mk_fun "From.find_deps_no_transitivity_state"
- let find_deps_term_no_transitivity_state =
- mk_fun "From.find_deps_term_no_transitivity_state"
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 4a82d0b724c34198a6b7dcb7821732989a710ebd..3e820ffff2a188f6965eade123baf0f20a01d628 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -109,9 +109,6 @@ module Value : sig
type t = Cvalue.V.t
(** Internal representation of a value. *)
- val emitter: Emitter.t ref
- (** Emitter used by Value to emit statuses *)
-
val proxy: State_builder.Proxy.t
val self : State.t
@@ -151,23 +148,11 @@ module Value : sig
of each reachable and evaluable statement. Filled only if
[Value_parameters.ResultsAfter] is set. *)
- val ignored_recursive_call: kernel_function -> bool
- (** This functions returns true if the value analysis found and ignored
- a recursive call to this function during the analysis. *)
-
val condition_truth_value: stmt -> bool * bool
(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
(resp. snd) is true if and only if the condition of the 'if' has been
evaluated to true (resp. false) at least once during the analysis. *)
- (** {3 Parameterization} *)
-
- val use_spec_instead_of_definition: (kernel_function -> bool) ref
- (** To be called by derived analyses to determine if they must use
- the body of the function (if available), or only its spec. Used for
- value builtins, and option -val-use-spec. *)
-
-
(** {4 Arguments of the main function} *)
(** The functions below are related to the arguments that are passed to the
@@ -231,65 +216,6 @@ module Value : sig
(** [after] is false by default.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val fold_stmt_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> stmt -> 'a
-
- val fold_state_callstack :
- (state -> 'a -> 'a) -> 'a -> after:bool -> kinstr -> 'a
-
- val find : state -> Locations.location -> t
-
- (** {3 Evaluations} *)
-
- val eval_lval :
- (?with_alarms:CilE.warn_mode ->
- Locations.Zone.t option ->
- state ->
- lval ->
- Locations.Zone.t option * t) ref
-
- val eval_expr :
- (?with_alarms:CilE.warn_mode -> state -> exp -> t) ref
-
- val eval_expr_with_state :
- (?with_alarms:CilE.warn_mode -> state -> exp -> state * t) ref
-
- val reduce_by_cond:
- (state -> exp -> bool -> state) ref
-
- val find_lv_plus :
- (Cvalue.Model.t -> Cil_types.exp ->
- (Cil_types.lval * Ival.t) list) ref
- (** returns the list of all decompositions of [expr] into the sum an lvalue
- and an interval. *)
-
- (** {3 Values and kernel functions} *)
-
- val expr_to_kernel_function :
- (kinstr
- -> ?with_alarms:CilE.warn_mode
- -> deps:Locations.Zone.t option
- -> exp
- -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
- val expr_to_kernel_function_state :
- (state
- -> deps:Locations.Zone.t option
- -> exp
- -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
- exception Not_a_call
- val call_to_kernel_function : stmt -> Kernel_function.Hptset.t
- (** Return the functions that can be called from this call.
- @raise Not_a_call if the statement is not a call. *)
-
- val valid_behaviors: (kernel_function -> state -> funbehavior list) ref
-
- val add_formals_to_state: (state -> kernel_function -> exp list -> state) ref
- (** [add_formals_to_state state kf exps] evaluates [exps] in [state]
- and binds them to the formal arguments of [kf] in the resulting
- state *)
-
(** {3 Reachability} *)
val is_accessible : kinstr -> bool
@@ -298,142 +224,6 @@ module Value : sig
val is_reachable_stmt : stmt -> bool
- (** {3 About kernel functions} *)
-
- exception Void_Function
- val find_return_loc : kernel_function -> Locations.location
- (** Return the location of the returned lvalue of the given function.
- @raise Void_Function if the function does not return any value. *)
-
- val is_called: (kernel_function -> bool) ref
-
- val callers: (kernel_function -> (kernel_function*stmt list) list) ref
- (** @return the list of callers with their call sites. Each function is
- present only once in the list. *)
-
- (** {3 State before a kinstr} *)
-
- val access : (kinstr -> lval -> t) ref
- val access_expr : (kinstr -> exp -> t) ref
- val access_location : (kinstr -> Locations.location -> t) ref
-
-
- (** {3 Locations of left values} *)
-
- val lval_to_loc :
- (kinstr -> ?with_alarms:CilE.warn_mode -> lval -> Locations.location) ref
-
- val lval_to_loc_with_deps :
- (kinstr
- -> ?with_alarms:CilE.warn_mode
- -> deps:Locations.Zone.t
- -> lval
- -> Locations.Zone.t * Locations.location) ref
-
- val lval_to_loc_with_deps_state :
- (state
- -> deps:Locations.Zone.t
- -> lval
- -> Locations.Zone.t * Locations.location) ref
-
- val lval_to_loc_state :
- (state -> lval -> Locations.location) ref
-
- val lval_to_offsetmap :
- ( kinstr -> ?with_alarms:CilE.warn_mode -> lval ->
- Cvalue.V_Offsetmap.t option) ref
-
- val lval_to_offsetmap_state :
- (state -> lval -> Cvalue.V_Offsetmap.t option) ref
- (** @since Carbon-20110201 *)
-
- val lval_to_zone :
- (kinstr -> ?with_alarms:CilE.warn_mode -> lval -> Locations.Zone.t) ref
-
- val lval_to_zone_state :
- (state -> lval -> Locations.Zone.t) ref
- (** Does not emit alarms. *)
-
- val lval_to_zone_with_deps_state:
- (state -> for_writing:bool -> deps:Locations.Zone.t option -> lval ->
- Locations.Zone.t * Locations.Zone.t * bool) ref
- (** [lval_to_zone_with_deps_state state ~for_writing ~deps lv] computes
- [res_deps, zone_lv, exact], where [res_deps] are the memory zones needed
- to evaluate [lv] in [state] joined with [deps]. [zone_lv] contains the
- valid memory zones that correspond to the location that [lv] evaluates
- to in [state]. If [for_writing] is true, [zone_lv] is restricted to
- memory zones that are writable. [exact] indicates that [lv] evaluates
- to a valid location of cardinal at most one. *)
-
- val lval_to_precise_loc_state:
- (?with_alarms:CilE.warn_mode -> state -> lval ->
- state * Precise_locs.precise_location * typ) ref
-
- val lval_to_precise_loc_with_deps_state:
- (state -> deps:Locations.Zone.t option -> lval ->
- Locations.Zone.t * Precise_locs.precise_location) ref
-
-
- (** Evaluation of the [\from] clause of an [assigns] clause.*)
- val assigns_inputs_to_zone :
- (state -> assigns -> Locations.Zone.t) ref
-
- (** Evaluation of the left part of [assigns] clause (without [\from]).*)
- val assigns_outputs_to_zone :
- (state -> result:varinfo option -> assigns -> Locations.Zone.t) ref
-
- (** Evaluation of the left part of [assigns] clause (without [\from]). Each
- assigns term results in one location. *)
- val assigns_outputs_to_locations :
- (state -> result:varinfo option -> assigns -> Locations.location list) ref
-
- (** For internal use only. Evaluate the [assigns] clause of the
- given function in the given prestate, compare it with the
- computed froms, return warning and set statuses. *)
- val verify_assigns_froms :
- (Kernel_function.t -> pre:state -> Function_Froms.t -> unit) ref
-
-
- (** {3 Evaluation of logic terms and predicates} *)
- module Logic : sig
- (** The APIs of this module are not stabilized yet, and are subject
- to change between Frama-C versions. *)
-
- val eval_predicate:
- (pre:state -> here:state -> predicate ->
- Property_status.emitted_status) ref
- (** Evaluate the given predicate in the given states for the Pre
- and Here ACSL labels.
- @since Neon-20140301 *)
- end
-
-
- (** {3 Callbacks} *)
-
- (** Actions to perform at end of each function analysis. Not compatible with
- option [-memexec-all] *)
-
- module Record_Value_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
-
- module Record_Value_Superposition_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state list Stmt.Hashtbl.t) Lazy.t
-
- module Record_Value_After_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
-
- (**/**)
- (* Temporary API, do not use *)
- module Record_Value_Callbacks_New: Hook.Iter_hook
- with type param =
- callstack *
- ((state Stmt.Hashtbl.t) Lazy.t (* before states *) *
- (state Stmt.Hashtbl.t) Lazy.t) (* after states *)
- Value_types.callback_result
- (**/**)
val no_results: (fundec -> bool) ref
(** Returns [true] if the user has requested that no results should
@@ -441,38 +231,6 @@ module Value : sig
on [Record_Value_Callbacks] and [Record_Value_Callbacks_New]
should not force their lazy argument *)
- (** Actions to perform at each treatment of a "call"
- statement. [state] is the state before the call.
- @deprecated Use Call_Type_Value_Callbacks instead. *)
- module Call_Value_Callbacks:
- Hook.Iter_hook with type param = state * callstack
-
- (** Actions to perform at each treatment of a "call"
- statement. [state] is the state before the call.
- @since Aluminium-20160501 *)
- module Call_Type_Value_Callbacks:
- Hook.Iter_hook with type param =
- [`Builtin | `Spec | `Body | `Reuse]
- * state * callstack
-
-
- (** Actions to perform whenever a statement is handled. *)
- module Compute_Statement_Callbacks:
- Hook.Iter_hook with type param = stmt * callstack * state list
-
- (* -remove-redundant-alarms feature, applied at the end of an Eva analysis,
- fulfilled by the Scope plugin that also depends on Eva. We thus use a
- reference here to avoid a cyclic dependency. *)
- val rm_asserts: (unit -> unit) ref
-
-
- (** {3 Pretty printing} *)
-
- val pretty : Format.formatter -> t -> unit
- val pretty_state : Format.formatter -> state -> unit
-
-
- val display : (Format.formatter -> kernel_function -> unit) ref
(**/**)
(** {3 Internal use only} *)
@@ -481,8 +239,6 @@ module Value : sig
(** To be used during the value analysis itself (instead of
{!get_state}). [after] is false by default. *)
- val recursive_call_occurred: kernel_function -> unit
-
val merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
val mask_then: int
val mask_else: int
@@ -492,12 +248,6 @@ module Value : sig
val update_callstack_table: after:bool -> stmt -> callstack -> state -> unit
(* Merge a new state in the table indexed by callstacks. *)
-
- val memoize : (kernel_function -> unit) ref
- (* val compute_call :
- (kernel_function -> call_kinstr:kinstr -> state -> (exp*t) list
- -> Cvalue.V_Offsetmap.t option (** returned value of [kernel_function] *) * state) ref
- *)
val merge_initial_state : callstack -> kernel_function -> state -> unit
(** Store an additional possible initial state for the given callstack as
well as its values for actuals. *)
@@ -508,30 +258,6 @@ end
"Db.Value is deprecated and will be removed in a future version \
of Frama-C. Please use the Eva.mli public API instead."]
-(** Functional dependencies between function inputs and function outputs.
- @see <../from/index.html> internal documentation. *)
-module From : sig
-
- (** exception raised by [find_deps_no_transitivity_*] if the given expression
- is not an lvalue.
- @since Aluminium-20160501
- *)
- exception Not_lval
-
- val find_deps_no_transitivity : (stmt -> exp -> Locations.Zone.t) ref
-
- val find_deps_no_transitivity_state :
- (Cvalue.Model.t -> exp -> Locations.Zone.t) ref
-
- (** @raise Not_lval if the given expression is not a C lvalue. *)
- val find_deps_term_no_transitivity_state :
- (Cvalue.Model.t -> term -> Value_types.logic_dependencies) ref
-
-end
-[@@alert db_deprecated
- "Db.From is deprecated and will be removed in a future version \
- of Frama-C. Please use the From module or the Eva API instead."]
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
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/Eva.mli b/src/plugins/eva/Eva.mli
index 3357d50d8349a3d3e2e90fe704eb5394b2b9109d..9d6baa29c8440b1deaab66ab6fdfbdbc366c91cb 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -685,6 +685,11 @@ module Cvalue_callbacks: sig
type state = Cvalue.Model.t
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result, and the dependencies
+ of each zone written to. *)
+ type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
| `Spec (** The specification is used to interpret the function. *)
@@ -708,7 +713,7 @@ module Cvalue_callbacks: sig
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 93fbcf970dc1d94407aa23aed067188751b4f5b3..47d8da9c980db7c8e0dad4beb6625dd7aef98d90 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_misc.ml
@@ -22,6 +22,7 @@
open Eva_utils
+open Lattice_bounds.Bottom.Operators
let frama_C_assert state actuals =
let do_bottom () =
@@ -35,10 +36,14 @@ let frama_C_assert state actuals =
then do_bottom ()
else if Cvalue.V.contains_zero arg
then begin
- let state = !Db.Value.reduce_by_cond state arg_exp true in
- if Cvalue.Model.is_reachable state
- then (warning_once_current "Frama_C_assert: unknown"; state)
- else do_bottom ()
+ let state =
+ let* valuation = fst (Cvalue_queries.reduce state arg_exp true) in
+ let valuation = Cvalue_queries.to_domain_valuation valuation in
+ Cvalue_transfer.update valuation state
+ in
+ match state with
+ | `Value state -> warning_once_current "Frama_C_assert: unknown"; state
+ | `Bottom -> do_bottom ()
end
else begin
warning_once_current "Frama_C_assert: true";
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index 5d6721b188a2ca2c2efc6d93ea2834e83db29bb5..a6a2cf2812a911993cd1ed76bfefdec413ca2933 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -74,7 +74,7 @@ let warning warn s =
[max_card] elements. *)
let split_v ~warn lv state max_card =
if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
- let loc = !Db.Value.lval_to_loc_state state lv in
+ let loc = Cvalue_queries.lval_to_loc state lv in
if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
let v_indet = Cvalue.Model.find_indeterminate state loc in
let v = Cvalue.V_Or_Uninitialized.get_v v_indet in
diff --git a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
index 39c576d07b60206c8b24bbb7bc700503bc983aa2..695278f28d6f4ae42c1d87c4c3887acdce294c40 100644
--- a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
@@ -96,7 +96,7 @@ let () =
Builtins.register_builtin "Frama_C_watch_cardinal" Cacheable
(add_watch make_watch_cardinal)
-let watch_hook (stmt, _callstack, states) =
+let watch_hook _callstack stmt states =
let treat ({name_lv = name; loc=loc; v=wa; remaining_count=current; stmts=set} as w) =
List.iter
(fun state ->
@@ -132,7 +132,7 @@ let watch_hook (stmt, _callstack, states) =
in
List.iter treat !watch_table
-let () = Db.Value.Compute_Statement_Callbacks.extend_once watch_hook
+let () = Cvalue_callbacks.register_statement_hook watch_hook
(*
Local Variables:
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 7822ad59369304d3781cdaa189f1c2abfb0fac4a..c6f8db8b6f69c634ccfd265263e9bd025c290884 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -24,142 +24,14 @@ open Eval
let dkey_card = Self.register_category "cardinal"
-module Model = struct
+module State = struct
- include Cvalue.Model
+ type state = Cvalue.Model.t * Locals_scoping.clobbered_set
type value = Main_values.CVal.t
type location = Main_locations.PLoc.location
- (* The origin is the value stored in the state for a lvalue, when this value
- has a type incompatible with the type of the lvalue. This may happen on
- union with fields of different types, or on code pattern such as
- int x = v; float f = *(float* )&x
- In this case, the value stored in the state and the value computed for the
- lvalue can be incomparable. The origin is then used to store the value from
- the state, to later choose which value to keep. This is done by the update
- function in cvalue_transfer. *)
- type origin = value
-
- let extract_expr _state _expr = `Value (Cvalue.V.top, None), Alarmset.all
-
- let indeterminate_alarms lval v =
- let open Cvalue.V_Or_Uninitialized in
- let status =
- if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
- in
- match v with
- | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
- | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
- | C_uninit_esc _ ->
- (* Unknown alarms: [v] can be either dangling or uninit *)
- Alarmset.(set (Alarms.Dangling lval) Unknown
- (set (Alarms.Uninitialized lval) Unknown none))
- | C_init_noesc _ -> Alarmset.none
-
-
- let eval_one_loc state lval typ =
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find_indeterminate state single_loc in
- Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
- in
- (* We have no good neutral element for "no alarm emitted yet", so we use
- [None] instead. *)
- let join_alarms acc alarms =
- match acc with
- | None -> Some alarms
- | Some acc -> Some (Alarmset.union alarms acc)
- in
- fun loc (acc_result, acc_alarms) ->
- let result, alarms = eval_one_loc loc in
- let result = Cvalue_forward.make_volatile ~typ:typ result in
- Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
-
- (* The zero singleton is shared between float and integer representations in
- ival, and is thus untyped. *)
- let is_float v =
- Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
-
- let extract_scalar_lval state lval typ loc =
- let process_one_loc = eval_one_loc state lval typ in
- let acc = Cvalue.V.bottom, None in
- let value, alarms = Precise_locs.fold process_one_loc loc acc in
- let alarms = match alarms with None -> Alarmset.none | Some a -> a in
- (* The origin is set to false when the value stored in the memory has not
- the same type as the read lvalue. In this case, we don't update the state
- with the new value stemming from the evaluation, even if it has been
- reduced, in order to not propagate incompatible type. *)
- let incompatible_type = is_float value <> Cil.isFloatingType typ in
- let origin = if incompatible_type then Some value else None in
- let value = Cvalue_forward.reinterpret typ value in
- if Cvalue.V.is_bottom value
- then `Bottom, alarms
- else `Value (value, origin), alarms
-
- (* Imprecise version for aggregate types that cvalues are unable to precisely
- represent. The initialization alarms must remain sound, though. *)
- let extract_aggregate_lval state lval _typ ploc =
- let loc = Precise_locs.imprecise_location ploc in
- match loc.Locations.size with
- | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
- | Int_Base.Value size ->
- let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
- match offsm with
- | `Bottom -> `Bottom, Alarmset.none
- | `Value offsm ->
- let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
- let alarms = indeterminate_alarms lval value in
- let v = Cvalue.V_Or_Uninitialized.get_v value in
- let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
- v, alarms
-
- let extract_lval state lval typ loc =
- if Cil.isArithmeticOrPointerType typ
- then extract_scalar_lval state lval typ loc
- else extract_aggregate_lval state lval typ loc
-
- let backward_location state _lval typ precise_loc value =
- let size = Precise_locs.loc_size precise_loc in
- let upto = succ (Int_set.get_small_cardinal()) in
- let loc = Precise_locs.imprecise_location precise_loc in
- let eval_one_loc single_loc =
- let v = Cvalue.Model.find state single_loc in
- let v = Cvalue_forward.make_volatile ~typ v in
- Cvalue_forward.reinterpret typ v
- in
- let process_ival base ival (acc_loc, acc_val as acc) =
- let loc_bits = Locations.Location_Bits.inject base ival in
- let single_loc = Locations.make_loc loc_bits size in
- let v = eval_one_loc single_loc in
- if Cvalue.V.intersects v value
- then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
- else acc
- in
- let fold_ival base ival acc =
- if Ival.cardinal_is_less_than ival upto
- then Ival.fold_enum (process_ival base) ival acc
- else process_ival base ival acc
- in
- let fold_location loc acc =
- try
- let loc = loc.Locations.loc in
- Locations.Location_Bits.fold_i fold_ival loc acc
- with
- Abstract_interp.Error_Top -> loc.Locations.loc, value
- in
- let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
- let loc_bits, value = fold_location loc acc in
- if Locations.Location_Bits.is_bottom loc_bits
- then `Bottom
- else
- let loc = Precise_locs.inject_location_bits loc_bits in
- `Value (Precise_locs.make_precise_loc loc ~size, value)
-
-end
-
-
-module State = struct
-
- type state = Model.t * Locals_scoping.clobbered_set
+ let value_dependencies = Main_values.cval
+ let location_dependencies = Main_locations.ploc
let log_category = Self.dkey_cvalue_domain
@@ -167,15 +39,16 @@ module State = struct
struct
include Datatype.Serializable_undefined
type t = state
- let name = Model.name ^ "+clobbered_set"
- let reprs = List.map (fun s -> s, Locals_scoping.bottom ()) Model.reprs
+ let name = Cvalue.Model.name ^ "+clobbered_set"
+ let reprs =
+ List.map (fun s -> s, Locals_scoping.bottom ()) Cvalue.Model.reprs
let structural_descr =
- Structural_descr.(
- t_tuple [| Model.packed_descr; pack Locals_scoping.structural_descr |])
- let pretty fmt (s, _) = Model.pretty fmt s
- let equal (a, _) (b, _) = Model.equal a b
- let compare (a, _) (b, _) = Model.compare a b
- let hash (s, _) = Model.hash s
+ Structural_descr.t_tuple
+ [| Cvalue.Model.packed_descr; Locals_scoping.packed_descr |]
+ let pretty fmt (s, _) = Cvalue.Model.pretty fmt s
+ let equal (a, _) (b, _) = Cvalue.Model.equal a b
+ let compare (a, _) (b, _) = Cvalue.Model.compare a b
+ let hash (s, _) = Cvalue.Model.hash s
let rehash = Datatype.identity
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -184,33 +57,31 @@ module State = struct
let name = "cvalue"
let key = Structure.Key_Domain.create_key name
- type value = Model.value
- type location = Model.location
-
- let value_dependencies = Main_values.cval
- let location_dependencies = Main_locations.ploc
-
- let top = Model.top, Locals_scoping.bottom ()
- let is_included (a, _) (b, _) = Model.is_included a b
- let join (a, clob) (b, _) = Model.join a b, clob
+ let top = Cvalue.Model.top, Locals_scoping.bottom ()
+ let is_included (a, _) (b, _) = Cvalue.Model.is_included a b
+ let join (a, clob) (b, _) = Cvalue.Model.join a b, clob
let widen kf stmt (a, clob) (b, _) =
let hint = Widen.getWidenHints kf stmt in
- Model.widen hint a b, clob
+ Cvalue.Model.widen hint a b, clob
let narrow (a, clob) (b, _) =
- let s = Model.narrow a b in
- if Model.(equal bottom s) then `Bottom else `Value (s, clob)
+ let s = Cvalue.Model.narrow a b in
+ if Cvalue.Model.(equal bottom s) then `Bottom else `Value (s, clob)
+
+ type origin = Cvalue_queries.origin
- type origin = Model.origin
+ let extract_expr ~oracle context (state, _) expr =
+ Cvalue_queries.extract_expr ~oracle context state expr
+
+ let extract_lval ~oracle context (state, _) lval typ loc =
+ Cvalue_queries.extract_lval ~oracle context state lval typ loc
- let extract_expr ~oracle:_ _context (s, _) expr =
- Model.extract_expr s expr
- let extract_lval ~oracle:_ _context (s, _) lval typ loc =
- Model.extract_lval s lval typ loc
let backward_location (state, _) lval typ precise_loc value =
- Model.backward_location state lval typ precise_loc value
- let reduce_further _ _ _ = []
+ Cvalue_queries.backward_location state lval typ precise_loc value
+
+ let reduce_further (state, _) expr value =
+ Cvalue_queries.reduce_further state expr value
(* ------------------------------------------------------------------------ *)
(* Transfer Functions *)
@@ -241,11 +112,11 @@ module State = struct
let start_recursive_call stmt call recursion (state, clob) =
let direct = is_direct_recursion stmt call in
- let state = Model.remove_variables recursion.withdrawal state in
+ let state = Cvalue.Model.remove_variables recursion.withdrawal state in
let substitution = recursion.base_substitution in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
- Model.replace_base substitution state
+ Cvalue.Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
(* Uses the [valuation] to update the [state] before the substitution
@@ -263,7 +134,7 @@ module State = struct
let direct = is_direct_recursion stmt call in
let pre, clob = pre in
let substitution = recursion.base_substitution in
- let state = Model.replace_base substitution state in
+ let state = Cvalue.Model.replace_base substitution state in
let clob = if direct then clob else Locals_scoping.top () in
let state = Locals_scoping.substitute substitution clob state in
let inter = Cvalue.Model.filter_by_shape recursion.base_withdrawal pre in
@@ -365,7 +236,7 @@ module State = struct
else Cvalue.V_Or_Uninitialized.C_uninit_noesc value
in
let loc = Precise_locs.imprecise_location loc in
- Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc cvalue, clob
let empty () =
let open Cvalue in
@@ -399,7 +270,7 @@ module State = struct
| Abstract_domain.Result kf ->
let value = Library_functions.returned_value kf in
let loc = Locations.loc_of_varinfo varinfo in
- Model.add_binding ~exact:true state loc value, clob
+ Cvalue.Model.add_binding ~exact:true state loc value, clob
(* ------------------------------------------------------------------------ *)
(* Misc *)
@@ -416,13 +287,13 @@ module State = struct
else
Bottom.non_bottom (Cvalue.Default_offsetmap.default_offsetmap b)
in
- Model.add_base b offsm state
+ Cvalue.Model.add_base b offsm state
let bind_global state varinfo =
let base = Base.of_varinfo varinfo in
let loc = Locations.loc_of_base base in
let value = Cvalue.V_Or_Uninitialized.uninitialized in
- Model.add_indeterminate_binding ~exact:true state loc value
+ Cvalue.Model.add_indeterminate_binding ~exact:true state loc value
let enter_scope kind vars (state, clob) =
let bind =
@@ -433,7 +304,7 @@ module State = struct
List.fold_left bind state vars, clob
let leave_scope kf vars (state, clob) =
- let state = Model.remove_variables vars state in
+ let state = Cvalue.Model.remove_variables vars state in
try
let fdec = Kernel_function.get_definition kf in
Locals_scoping.make_escaping_fundec fdec clob vars state, clob
@@ -584,8 +455,6 @@ module State = struct
then Parameters.ForceValues.output display_results
end
-let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
-
let registered =
let name = "cvalue"
@@ -597,16 +466,16 @@ let registered =
type prefix = Hptmap.prefix
module Subpart = struct
- type t = Model.subtree
- let hash = Model.hash_subtree
- let equal = Model.equal_subtree
+ type t = Cvalue.Model.subtree
+ let hash = Cvalue.Model.hash_subtree
+ let equal = Cvalue.Model.equal_subtree
end
let distinct_subpart (a, _) (b, _) =
- if Model.equal a b then None
+ if Cvalue.Model.equal a b then None
else
- try Model.comp_prefixes a b; None
- with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
-let find_subpart (s, _) prefix = Model.find_prefix s prefix
+ try Cvalue.Model.comp_prefixes a b; None
+ with Cvalue.Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
+let find_subpart (s, _) prefix = Cvalue.Model.find_prefix s prefix
module Getters (Dom : Abstract.Domain.External) = struct
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ae31230b0e8ede332ce8a485e99431acb7c51d83
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -0,0 +1,184 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Queries = struct
+
+ type state = Cvalue.Model.t
+ type value = Main_values.CVal.t
+ type location = Main_locations.PLoc.location
+
+ (* The origin is the value stored in the state for a lvalue, when this value
+ has a type incompatible with the type of the lvalue. This may happen on
+ union with fields of different types, or on code pattern such as
+ int x = v; float f = *(float* )&x
+ In this case, the value stored in the state and the value computed for the
+ lvalue can be incomparable. The origin is then used to store the value from
+ the state, to later choose which value to keep. This is done by the update
+ function in cvalue_transfer. *)
+ type origin = value
+
+ let extract_expr ~oracle:_ _context _state _expr =
+ `Value (Cvalue.V.top, None), Alarmset.all
+
+ let indeterminate_alarms lval v =
+ let open Cvalue.V_Or_Uninitialized in
+ let status =
+ if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
+ in
+ match v with
+ | C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
+ | C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
+ | C_uninit_esc _ ->
+ (* Unknown alarms: [v] can be either dangling or uninit *)
+ Alarmset.(set (Alarms.Dangling lval) Unknown
+ (set (Alarms.Uninitialized lval) Unknown none))
+ | C_init_noesc _ -> Alarmset.none
+
+
+ let eval_one_loc state lval typ =
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find_indeterminate state single_loc in
+ Cvalue.V_Or_Uninitialized.get_v v, indeterminate_alarms lval v
+ in
+ (* We have no good neutral element for "no alarm emitted yet", so we use
+ [None] instead. *)
+ let join_alarms acc alarms =
+ match acc with
+ | None -> Some alarms
+ | Some acc -> Some (Alarmset.union alarms acc)
+ in
+ fun loc (acc_result, acc_alarms) ->
+ let result, alarms = eval_one_loc loc in
+ let result = Cvalue_forward.make_volatile ~typ:typ result in
+ Cvalue.V.join result acc_result, join_alarms acc_alarms alarms
+
+ (* The zero singleton is shared between float and integer representations in
+ ival, and is thus untyped. *)
+ let is_float v =
+ Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
+
+ let extract_scalar_lval state lval typ loc =
+ let process_one_loc = eval_one_loc state lval typ in
+ let acc = Cvalue.V.bottom, None in
+ let value, alarms = Precise_locs.fold process_one_loc loc acc in
+ let alarms = match alarms with None -> Alarmset.none | Some a -> a in
+ (* The origin is set to false when the value stored in the memory has not
+ the same type as the read lvalue. In this case, we don't update the state
+ with the new value stemming from the evaluation, even if it has been
+ reduced, in order to not propagate incompatible type. *)
+ let incompatible_type = is_float value <> Cil.isFloatingType typ in
+ let origin = if incompatible_type then Some value else None in
+ let value = Cvalue_forward.reinterpret typ value in
+ if Cvalue.V.is_bottom value
+ then `Bottom, alarms
+ else `Value (value, origin), alarms
+
+ (* Imprecise version for aggregate types that cvalues are unable to precisely
+ represent. The initialization alarms must remain sound, though. *)
+ let extract_aggregate_lval state lval _typ ploc =
+ let loc = Precise_locs.imprecise_location ploc in
+ match loc.Locations.size with
+ | Int_Base.Top -> `Value (Cvalue.V.top, None), Alarmset.all
+ | Int_Base.Value size ->
+ let offsm = Cvalue.Model.copy_offsetmap loc.Locations.loc size state in
+ match offsm with
+ | `Bottom -> `Bottom, Alarmset.none
+ | `Value offsm ->
+ let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
+ let alarms = indeterminate_alarms lval value in
+ let v = Cvalue.V_Or_Uninitialized.get_v value in
+ let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
+ v, alarms
+
+ let extract_lval ~oracle:_ _context state lval typ loc =
+ if Cil.isArithmeticOrPointerType typ
+ then extract_scalar_lval state lval typ loc
+ else extract_aggregate_lval state lval typ loc
+
+ let backward_location state _lval typ precise_loc value =
+ let size = Precise_locs.loc_size precise_loc in
+ let upto = succ (Int_set.get_small_cardinal()) in
+ let loc = Precise_locs.imprecise_location precise_loc in
+ let eval_one_loc single_loc =
+ let v = Cvalue.Model.find state single_loc in
+ let v = Cvalue_forward.make_volatile ~typ v in
+ Cvalue_forward.reinterpret typ v
+ in
+ let process_ival base ival (acc_loc, acc_val as acc) =
+ let loc_bits = Locations.Location_Bits.inject base ival in
+ let single_loc = Locations.make_loc loc_bits size in
+ let v = eval_one_loc single_loc in
+ if Cvalue.V.intersects v value
+ then Locations.Location_Bits.join loc_bits acc_loc, Cvalue.V.join v acc_val
+ else acc
+ in
+ let fold_ival base ival acc =
+ if Ival.cardinal_is_less_than ival upto
+ then Ival.fold_enum (process_ival base) ival acc
+ else process_ival base ival acc
+ in
+ let fold_location loc acc =
+ try
+ let loc = loc.Locations.loc in
+ Locations.Location_Bits.fold_i fold_ival loc acc
+ with
+ Abstract_interp.Error_Top -> loc.Locations.loc, value
+ in
+ let acc = Locations.Location_Bits.bottom, Cvalue.V.bottom in
+ let loc_bits, value = fold_location loc acc in
+ if Locations.Location_Bits.is_bottom loc_bits
+ then `Bottom
+ else
+ let loc = Precise_locs.inject_location_bits loc_bits in
+ `Value (Precise_locs.make_precise_loc loc ~size, value)
+
+ let reduce_further _state _expr _value = []
+end
+
+include Queries
+
+(* -------------------------------------------------------------------------- *)
+(* Evaluation engine for the cvalue domain *)
+(* -------------------------------------------------------------------------- *)
+
+module Value = struct
+ module Internal = struct
+ include Main_values.CVal
+ let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
+ end
+ include Internal
+ include Structure.Open (Abstract.Value) (Internal)
+ let reduce t = t
+end
+
+module Domain = struct
+ include Cvalue.Model
+ include Queries
+end
+
+include Evaluation.Make (Value) (Main_locations.PLoc) (Domain)
+
+let lval_to_loc state lval =
+ let eval, _alarms = lvaluate ~for_writing:false state lval in
+ match eval with
+ | `Bottom -> Locations.loc_bottom
+ | `Value (_valuation, ploc, _typ) -> Precise_locs.imprecise_location ploc
diff --git a/src/kernel_services/abstract_interp/value_types.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
similarity index 71%
rename from src/kernel_services/abstract_interp/value_types.ml
rename to src/plugins/eva/domains/cvalue/cvalue_queries.mli
index d7d070d20e3053df8e3337c8921a6b9bd037c536..e6f423f25439ab77a9e34a23988997122a5e948e 100644
--- a/src/kernel_services/abstract_interp/value_types.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -20,17 +20,18 @@
(* *)
(**************************************************************************)
-type 'a callback_result =
- | Normal of 'a
- | NormalStore of 'a * int
- | Reuse of int
+(** Implementation of domain queries for the cvalue domain. *)
+include Abstract_domain.Queries
+ with type state = Cvalue.Model.t
+ and type value = Main_values.CVal.t
+ and type location = Main_locations.PLoc.location
+ and type origin = Main_values.CVal.t
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+(** Evaluation engine specific to the cvalue domain. *)
+include Evaluation_sig.S with type state := state
+ and type value := value
+ and type loc := location
+ and type origin := origin
-type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+(** Evaluates the location of a lvalue in a given cvalue state. *)
+val lval_to_loc: state -> Cil_types.lval -> Locations.location
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 222f8bbe68349524dabe96f1d9b91d1ed3e1e438..007674371f657ba8bdca117a649689e86287b3be 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -204,10 +204,7 @@ let actualize_formals state arguments =
List.fold_left treat_one_formal state arguments
let start_call _stmt call _recursion _valuation state =
- let with_formals = actualize_formals state call.arguments in
- let stack_with_call = Eva_utils.current_call_stack () in
- Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
- `Value with_formals
+ `Value (actualize_formals state call.arguments)
let finalize_call stmt call _recursion ~pre:_ ~post:state =
(* Deallocate memory allocated via alloca().
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.ml b/src/plugins/eva/domains/cvalue/locals_scoping.ml
index ce41844e798d31a73797da73a637810395c92398..2e263ae8d1f369514c6351153e9628b3e8b0bc62 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.ml
@@ -27,9 +27,9 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-let structural_descr =
+let packed_descr =
let open Structural_descr in
- t_record [| Base.SetLattice.packed_descr |]
+ pack (t_record [| Base.SetLattice.packed_descr |])
let bottom () = { clob = Base.SetLattice.bottom }
let top () = { clob = Base.SetLattice.top }
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.mli b/src/plugins/eva/domains/cvalue/locals_scoping.mli
index 274e3ea64d0991b14b936e847a82cbeaec21750f..abaf168a64d782eb7106b29bde409b2099d48271 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.mli
@@ -30,7 +30,7 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-val structural_descr: Structural_descr.t
+val packed_descr: Structural_descr.pack
val bottom: unit -> clobbered_set
val top: unit -> clobbered_set
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/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index a93c6903e27d182ab6bc564fa6a3b82ae951c8ad..6bbfef27ba4dc1a948398cb182431dd2c0fda689 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -187,6 +187,8 @@ let cvalue_initial_state () =
let _, lib_entry = Globals.entry_point () in
G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
+let () = Db.Value.initial_state_only_globals := cvalue_initial_state
+
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
@@ -207,6 +209,12 @@ let reset_analyzer () =
if not (Abstractions.Config.equal config (fst !ref_analyzer))
then make_analyzer config
+(* Resets the Analyzer when the current project is changed. *)
+let () =
+ Project.register_after_set_current_hook
+ ~user_only:true (fun _ -> reset_analyzer ());
+ Project.register_after_global_load_hook reset_analyzer
+
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
Ast.compute ();
@@ -230,8 +238,12 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
-(* Resets the Analyzer when the current project is changed. *)
-let () =
- Project.register_after_set_current_hook
- ~user_only:true (fun _ -> reset_analyzer ());
- Project.register_after_global_load_hook reset_analyzer
+let () = Db.Value.compute := compute
+let () = Parameters.ForceValues.set_output_dependencies [Self.state]
+
+let main () =
+ (* Value computations *)
+ if Parameters.ForceValues.get () then compute ();
+ if is_computed () then Red_statuses.report ()
+
+let () = Db.Main.extend main
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 8dd74f365d0902882070a351b18b404853d35eef..fe482f514af1c500e3757d6505f5dc40adc3c5f7 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -154,6 +154,3 @@ val use_spec_instead_of_definition: Cil_types.kernel_function -> bool
to known whether results are available for a given function. *)
val save_results: Cil_types.kernel_function -> bool
[@@@ api_end]
-
-val cvalue_initial_state: unit -> Cvalue.Model.t
-(** Return the initial state of the cvalue domain only. *)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 9fda306efa9a0cafb74be4405962cf7d244a63ce..03dc9b5a62980335cac260fe0a35c8d5e8c0c418 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -353,16 +353,11 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* ----- Main call -------------------------------------------------------- *)
- let store_initial_state callstack kf init_state =
- Abstract.Dom.Store.register_initial_state callstack kf init_state;
- let cvalue_state = get_cvalue_or_top init_state in
- Db.Value.Call_Value_Callbacks.apply (cvalue_state, callstack)
-
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
let callstack = Eva_utils.init_call_stack kf in
- store_initial_state callstack kf init_state;
+ Abstract.Dom.Store.register_initial_state callstack kf init_state;
let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index e97c859d276e889eadf25f1374727816f36479fa..28a09aefb91ba4effb0aa2d49f0ee2a97f5c8e6f 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -35,7 +35,6 @@ let check_signals, signal_abort =
(fun () -> signal_emitted := true)
let dkey = Self.dkey_iterator
-let dkey_callbacks = Self.dkey_callbacks
let stat_iterations = Statistics.register_statement_stat "iterations"
let blocks_share_locals b1 b2 =
@@ -686,13 +685,6 @@ module Make_Dataflow
let merged_post_states = lazy
(states_after_stmt merged_pre_states merged_post_states)
in
- let unmerged_pre_cvalues = lazy
- (StmtTable.map (fun _stmt (v,_) ->
- let store = get_vertex_store v in
- let states = Partitioning.expanded store in
- List.map (fun (_k,x) -> get_cvalue_or_top x) states)
- automaton.stmt_table)
- in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
let callstack = Eva_utils.current_call_stack () in
@@ -703,22 +695,6 @@ module Make_Dataflow
StmtTable.iter register_post (Lazy.force merged_post_states);
merge_conditions ();
end;
- if not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value_Superposition callbacks";
- Db.Value.Record_Value_Superposition_Callbacks.apply
- (callstack, unmerged_pre_cvalues);
- end;
- if not (Db.Value.Record_Value_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value callbacks";
- Db.Value.Record_Value_Callbacks.apply
- (callstack, merged_pre_cvalues)
- end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
after_stmts = merged_post_cvalues }
@@ -726,14 +702,6 @@ module Make_Dataflow
let cvalue_init = get_cvalue_or_top initial_state in
let results = `Body (states, Mem_exec.new_counter ()) in
Cvalue_callbacks.apply_call_results_hooks callstack kf cvalue_init results;
- if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_After_Value callbacks";
- Db.Value.Record_Value_After_Callbacks.apply
- (callstack, merged_post_cvalues);
- end;
end
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 75e3571534fd65d3b671950aa9250ccfcb87ed59..78ab84bc9725887ee9d3ce1810e128248af25ce5 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -733,7 +733,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let call_stack = Eva_utils.current_call_stack () in
let stack_with_call = Callstack.push kf stmt call_stack in
let cvalue_state = get_cvalue_or_top state in
- Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Cvalue_callbacks.apply_call_hooks stack_with_call kf cvalue_state `Builtin;
Cvalue_callbacks.apply_call_results_hooks stack_with_call kf cvalue_state
(`Builtin ([cvalue_state], None))
diff --git a/src/plugins/eva/legacy/function_args.ml b/src/plugins/eva/legacy/function_args.ml
deleted file mode 100644
index b1f4dd23053f3a49a56eccdd76ff835d4b8376e6..0000000000000000000000000000000000000000
--- a/src/plugins/eva/legacy/function_args.ml
+++ /dev/null
@@ -1,83 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Lattice_bounds
-
-exception Actual_is_bottom
-exception WrongFunctionType (* at a call through a pointer *)
-
-let rec fold_left2_best_effort f acc l1 l2 =
- match l1,l2 with
- | _,[] -> acc
- | [],_ -> raise WrongFunctionType (* Too few arguments *)
- | (x1::r1),(x2::r2) -> fold_left2_best_effort f (f acc x1 x2) r1 r2
-
-let actualize_formals kf state actuals =
- let formals = Kernel_function.get_formals kf in
- let treat_one_formal acc actual_o formal =
- Cvalue.Model.add_base (Base.of_varinfo formal) actual_o acc
- in
- fold_left2_best_effort treat_one_formal state actuals formals
-
-let offsetmap_of_lv state lv =
- let open Locations in
- let state, loc_to_read, _typ = !Db.Value.lval_to_precise_loc_state state lv in
- let aux loc offsm_res =
- let size = Int_Base.project loc.size in
- let copy = Cvalue.Model.copy_offsetmap loc.loc size state in
- Bottom.join Cvalue.V_Offsetmap.join copy offsm_res
- in
- Precise_locs.fold aux loc_to_read `Bottom
-
-let compute_actual state e =
- match e with
- | { enode = Lval lv } when not (Eval_typ.is_bitfield (Cil.typeOfLval lv)) ->
- let o =
- try offsetmap_of_lv state lv
- with Abstract_interp.Error_Top ->
- Self.abort ~current:true
- "Function argument %a has unknown size. Aborting" Printer.pp_exp e;
- in begin
- match o with
- | `Value o -> o
- | `Bottom -> raise Actual_is_bottom
- end
- | _ ->
- let interpreted_expr = !Db.Value.eval_expr state e in
- if Cvalue.V.is_bottom interpreted_expr then raise Actual_is_bottom;
- let typ = Cil.typeOf e in
- Eval_op.offsetmap_of_v ~typ interpreted_expr
-
-let () =
- Db.Value.add_formals_to_state :=
- (fun state kf exps ->
- try
- let actuals = List.map (fun e -> compute_actual state e) exps in
- actualize_formals kf state actuals
- with Actual_is_bottom | WrongFunctionType -> Cvalue.Model.bottom)
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/eva/legacy/function_args.mli b/src/plugins/eva/legacy/function_args.mli
deleted file mode 100644
index c2690f3b81659bccfa182f636ed5b8851db004ca..0000000000000000000000000000000000000000
--- a/src/plugins/eva/legacy/function_args.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Nothing is exported; the function [compute_atual] is registered
- in {!Db.Value}. *)
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
deleted file mode 100644
index 0994d6ee1ec9087820633e00d0d76eb0352e4ea2..0000000000000000000000000000000000000000
--- a/src/plugins/eva/register.ml
+++ /dev/null
@@ -1,447 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Locations
-
-let () = Db.Value.compute := Analysis.compute
-let () = Parameters.ForceValues.set_output_dependencies [Self.state]
-
-let main () =
- (* Value computations *)
- if Parameters.ForceValues.get () then Analysis.compute ();
- if Analysis.is_computed () then Red_statuses.report ()
-
-let () = Db.Main.extend main
-
-
-(* "access" functions before evaluation, registered in Db.Value *)
-let access_value_of_lval kinstr lv =
- let state = Db.Value.get_state kinstr in
- snd (!Db.Value.eval_lval None state lv)
-
-let access_value_of_expr kinstr e =
- let state = Db.Value.get_state kinstr in
- !Db.Value.eval_expr state e
-
-let access_value_of_location kinstr loc =
- let state = Db.Value.get_state kinstr in
- Db.Value.find state loc
-
-let find_deps_term_no_transitivity_state state t =
- try
- let env = Eval_terms.env_only_here state in
- let r = Eval_terms.eval_term ~alarm_mode:Eval_terms.Ignore env t in
- r.Eval_terms.ldeps
- with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval
-
-let find_deps_no_transitivity stmt expr =
- Results.(before stmt |> expr_deps expr)
-
-let find_deps_no_transitivity_state state expr =
- Results.(in_cvalue_state state |> expr_deps expr)
-
-let eval_predicate ~pre ~here p =
- let open Eval_terms in
- let env = env_annot ~pre ~here () in
- match eval_predicate env p with
- | True -> Property_status.True
- | False -> Property_status.False_if_reachable
- | Unknown -> Property_status.Dont_know
-
-let () =
- Db.Value.is_called := Function_calls.is_called;
- Db.Value.callers := Function_calls.callsites;
- Db.Value.use_spec_instead_of_definition :=
- Function_calls.use_spec_instead_of_definition;
- Db.Value.assigns_outputs_to_zone :=
- (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
- Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
- Db.Value.access := access_value_of_lval;
- Db.Value.access_location := access_value_of_location;
- Db.Value.access_expr := access_value_of_expr;
- Db.Value.Logic.eval_predicate := eval_predicate;
- Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
- Db.From.find_deps_term_no_transitivity_state :=
- find_deps_term_no_transitivity_state;
- Db.From.find_deps_no_transitivity := find_deps_no_transitivity;
- Db.From.find_deps_no_transitivity_state := find_deps_no_transitivity_state;
-
-
- (* -------------------------------------------------------------------------- *)
- (* Register Evaluation Functions *)
- (* -------------------------------------------------------------------------- *)
-
-open Eval
-
-module CVal = struct
- include Main_values.CVal
- let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
-end
-
-module Val = struct
- include CVal
- include Structure.Open (Abstract.Value) (CVal)
- let reduce t = t
-end
-
-module Eva =
- Evaluation.Make
- (Val)
- (Main_locations.PLoc)
- (Cvalue_domain.State)
-
-let inject_cvalue state = state, Locals_scoping.bottom ()
-
-let bot_value = function
- | `Bottom -> Cvalue.V.bottom
- | `Value v -> v
-
-let bot_state = function
- | `Bottom -> Cvalue.Model.bottom
- | `Value s -> s
-
-let update valuation state =
- let domain_valuation = Eva.to_domain_valuation valuation in
- bot_state (Cvalue_domain.State.update domain_valuation state >>-: fst)
-
-let rec eval_deps state e =
- match e.enode with
- | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | Const _ ->
- Locations.Zone.bottom
- | Lval lv -> eval_deps_lval state lv
- | BinOp (_,e1,e2,_) ->
- Locations.Zone.join (eval_deps state e1) (eval_deps state e2)
- | CastE (_,e) | UnOp (_,e,_) ->
- eval_deps state e
- | AddrOf lv | StartOf lv -> eval_deps_addr state lv
-and eval_deps_lval state lv =
- let for_writing = false in
- let deps = eval_deps_addr state lv in
- let loc =
- fst (Eva.lvaluate ~for_writing state lv)
- >>-: fun (_valuation, loc, _typ) -> loc
- in
- match loc with
- | `Bottom -> deps
- | `Value loc ->
- let deps_lv = Precise_locs.enumerate_valid_bits Read loc in
- Locations.Zone.join deps deps_lv
-and eval_deps_addr state (h, o:lval) =
- Locations.Zone.join (eval_deps_host state h) (eval_deps_offset state o)
-and eval_deps_host state h = match h with
- | Var _ -> Locations.Zone.bottom
- | Mem e -> eval_deps state e
-and eval_deps_offset state o = match o with
- | NoOffset -> Locations.Zone.bottom
- | Field (_, o) -> eval_deps_offset state o
- | Index (i, o) ->
- Locations.Zone.join (eval_deps state i) (eval_deps_offset state o)
-
-let notify_opt with_alarms alarms =
- Option.iter (fun mode -> Alarmset.notify mode alarms) with_alarms
-
-let eval_expr_with_valuation ?with_alarms deps state expr=
- let state = inject_cvalue state in
- let deps = match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps state expr in
- Some (Locations.Zone.join deps' deps)
- in
- let eval, alarms = Eva.evaluate state expr in
- notify_opt with_alarms alarms;
- match eval with
- | `Bottom -> (Cvalue.Model.bottom, deps, Cvalue.V.bottom), None
- | `Value (valuation, result) ->
- let state = update valuation state in
- (state, deps, result), Some valuation
-
-(* Compatibility layer between the old API of eval_exprs and the new evaluation
- scheme. *)
-module Eval = struct
-
- let eval_expr ?with_alarms state expr =
- let state = inject_cvalue state in
- let eval, alarms = Eva.evaluate ~reduction:false state expr in
- notify_opt with_alarms alarms;
- bot_value (eval >>-: snd)
-
- let eval_lval ?with_alarms deps state lval =
- let expr = Eva_utils.lval_to_exp lval in
- let res, valuation = eval_expr_with_valuation ?with_alarms deps state expr in
- let typ = match valuation with
- | None -> Cil.typeOfLval lval
- | Some valuation -> match Eva.Valuation.find_loc valuation lval with
- | `Value record -> record.typ
- | `Top -> Cil.typeOfLval lval
- in
- let state, deps, v = res in
- state, deps, v, typ
-
- let eval_expr_with_deps_state ?with_alarms deps state expr =
- fst (eval_expr_with_valuation ?with_alarms deps state expr)
-
-
- let reduce_by_cond state expr positive =
- let state = inject_cvalue state in
- let eval, _alarms =
- Eva.reduce state expr positive
- in
- bot_state (eval >>-: fun valuation -> update valuation state)
-
-
- let lval_to_precise_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index:(_:bool) lval =
- if not (Cvalue.Model.is_reachable state)
- then state, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- else
- let state = inject_cvalue state in
- let deps = match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps_addr state lval in
- Some (Locations.Zone.join deps' deps)
- in
- let eval, alarms =
- Eva.lvaluate ~for_writing:false state lval
- in
- notify_opt with_alarms alarms;
- match eval with
- | `Bottom -> Cvalue.Model.bottom, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- | `Value (valuation, loc, typ) -> update valuation state, deps, loc, typ
-
- let lval_to_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index lv =
- let state, deps, pl, typ =
- lval_to_precise_loc_deps_state
- ?with_alarms ~deps state ~reduce_valid_index lv
- in
- state, deps, Precise_locs.imprecise_location pl, typ
-
- let lval_to_precise_loc_state ?with_alarms state lv =
- let state, _, r, typ =
- lval_to_precise_loc_deps_state
- ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state lv
- in
- state, r, typ
-
- and lval_to_loc_state ?with_alarms state lv =
- let state, _, r, typ =
- lval_to_loc_deps_state
- ?with_alarms ~deps:None ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state lv
- in
- state, r, typ
-
- let lval_to_precise_loc ?with_alarms state lv =
- let _, r, _typ = lval_to_precise_loc_state ?with_alarms state lv in
- r
-
- let lval_to_loc ?with_alarms state lv =
- let _, r, _typ = lval_to_loc_state ?with_alarms state lv in
- r
-
-
- let resolv_func_vinfo ?with_alarms deps state funcexp =
- let open Cil_types in
- let state = inject_cvalue state in
- let deps = match funcexp.enode with
- | Lval (Var _, NoOffset) -> deps
- | Lval (Mem v, _) ->
- begin match deps with
- | None -> None
- | Some deps ->
- let deps' = eval_deps state v in
- Some (Locations.Zone.join deps' deps)
- end
- | _ -> assert false
- in
- let kfs, alarms = Eva.eval_function_exp funcexp state in
- notify_opt with_alarms alarms;
- let kfs = match kfs with
- | `Bottom -> Kernel_function.Hptset.empty
- | `Value kfs ->
- List.fold_left
- (fun acc (kf, _) -> Kernel_function.Hptset.add kf acc)
- Kernel_function.Hptset.empty kfs
- in
- kfs, deps
-
-end
-
-module type Eval = module type of Eval
-
-(* Functions to register in Db.Value that depend on evaluation functions. *)
-module Export (Eval : Eval) = struct
-
- open Eval
-
- let lval_to_loc_with_deps_state ?with_alarms state ~deps lv =
- let _state, deps, r, _ =
- lval_to_loc_deps_state
- ?with_alarms
- ~deps:(Some deps)
- ~reduce_valid_index:(Kernel.SafeArrays.get ())
- state
- lv
- in
- Option.value ~default:Locations.Zone.bottom deps, r
-
- let lval_to_loc_with_deps kinstr ?with_alarms ~deps lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_loc_with_deps_state ?with_alarms state ~deps lv
-
- let lval_to_loc_kinstr kinstr ?with_alarms lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_loc ?with_alarms state lv
-
- let lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps lv =
- let _state, deps, ploc, _ =
- lval_to_precise_loc_deps_state ?with_alarms
- ~deps ~reduce_valid_index:(Kernel.SafeArrays.get ()) state lv
- in
- let deps = Option.value ~default:Locations.Zone.bottom deps in
- deps, ploc
-
- let lval_to_precise_loc_with_deps_state =
- lval_to_precise_loc_with_deps_state_alarm ?with_alarms:None
-
- let lval_to_zone kinstr ?with_alarms lv =
- let state_to_joined_zone state acc =
- let _, r =
- lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps:None lv
- in
- let zone = Precise_locs.enumerate_valid_bits Read r in
- Locations.Zone.join acc zone
- in
- Db.Value.fold_state_callstack
- state_to_joined_zone Locations.Zone.bottom ~after:false kinstr
-
- let lval_to_zone_state state lv =
- let _, r = lval_to_precise_loc_with_deps_state state ~deps:None lv in
- Precise_locs.enumerate_valid_bits Read r
-
- let lval_to_zone_with_deps_state state ~for_writing ~deps lv =
- let deps, r = lval_to_precise_loc_with_deps_state state ~deps lv in
- let r = (* No write effect if [lv] is const *)
- if for_writing && (Eva_utils.is_const_write_invalid (Cil.typeOfLval lv))
- then Precise_locs.loc_bottom
- else r
- in
- let access = if for_writing then Write else Read in
- let zone = Precise_locs.enumerate_valid_bits access r in
- let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing r in
- deps, zone, exact
-
-
- let lval_to_offsetmap_aux ?with_alarms state lv =
- let loc =
- Locations.valid_part Read
- (lval_to_loc ?with_alarms state lv)
- in
- match loc.Locations.size with
- | Int_Base.Top -> None
- | Int_Base.Value size ->
- match Cvalue.Model.copy_offsetmap loc.Locations.loc size state with
- | `Bottom -> None
- | `Value m -> Some m
-
- let lval_to_offsetmap kinstr ?with_alarms lv =
- let state = Db.Value.noassert_get_state kinstr in
- lval_to_offsetmap_aux ?with_alarms state lv
-
- let lval_to_offsetmap_state state lv =
- lval_to_offsetmap_aux state lv
-
-
- let expr_to_kernel_function_state ?with_alarms state ~deps exp =
- let r, deps = resolv_func_vinfo ?with_alarms deps state exp in
- Option.value ~default:Locations.Zone.bottom deps, r
-
- let expr_to_kernel_function kinstr ?with_alarms ~deps exp =
- let state_to_joined_kernel_function state (z_acc, kf_acc) =
- let z, kf =
- expr_to_kernel_function_state ?with_alarms state ~deps exp
- in
- Locations.Zone.join z z_acc,
- Kernel_function.Hptset.union kf kf_acc
- in
- Db.Value.fold_state_callstack
- state_to_joined_kernel_function
- ((match deps with None -> Locations.Zone.bottom | Some z -> z),
- Kernel_function.Hptset.empty)
- ~after:false kinstr
-
- let expr_to_kernel_function_state =
- expr_to_kernel_function_state ?with_alarms:None
-end
-
-
-module type Export = module type of (Export (Eval))
-
-let register (module Eval: Eval) (module Export: Export) =
- let open Export in
- Db.Value.eval_expr := Eval.eval_expr;
- Db.Value.eval_expr_with_state :=
- (fun ?with_alarms state expr ->
- let (s, _, v) =
- Eval.eval_expr_with_deps_state ?with_alarms None state expr
- in
- s, v);
- Db.Value.reduce_by_cond := Eval.reduce_by_cond;
- Db.Value.eval_lval :=
- (fun ?with_alarms deps state lval ->
- let _, deps, r, _ = Eval.eval_lval ?with_alarms deps state lval in
- deps, r);
- Db.Value.lval_to_loc_with_deps := lval_to_loc_with_deps;
- Db.Value.lval_to_loc_with_deps_state :=
- lval_to_loc_with_deps_state ?with_alarms:None;
- Db.Value.lval_to_loc := lval_to_loc_kinstr;
- Db.Value.lval_to_loc_state := Eval.lval_to_loc ?with_alarms:None;
- Db.Value.lval_to_zone_state := lval_to_zone_state;
- Db.Value.lval_to_zone := lval_to_zone;
- Db.Value.lval_to_zone_with_deps_state := lval_to_zone_with_deps_state;
- Db.Value.lval_to_precise_loc_state := Eval.lval_to_precise_loc_state;
- Db.Value.lval_to_precise_loc_with_deps_state :=
- lval_to_precise_loc_with_deps_state;
- Db.Value.lval_to_offsetmap := lval_to_offsetmap;
- Db.Value.lval_to_offsetmap_state := lval_to_offsetmap_state;
- Db.Value.expr_to_kernel_function := expr_to_kernel_function;
- Db.Value.expr_to_kernel_function_state := expr_to_kernel_function_state;
- ()
-
-
-let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state
-
-let () = Db.Value.verify_assigns_froms := Logic_inout.verify_assigns
-
-let () =
- let eval = (module Eval : Eval) in
- let export = (module Export ((val eval : Eval)) : Export) in
- register eval export;;
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/register.mli b/src/plugins/eva/register.mli
deleted file mode 100644
index 3898a7c5ac07923fdae7ad7914c1dcbd1322a25b..0000000000000000000000000000000000000000
--- a/src/plugins/eva/register.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Functions of the Value plugin registered in {!Db}. Only three functions
- are exported. *)
-
-val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t
-val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
-val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index d5bf54e2f5b77bc048ad80777e94aa85cc0e2c81..d4101a12b9c2de6f3a289deef62458ba3a3ef6c6 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -39,15 +39,15 @@ let register_call_hook f =
Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
let apply_call_hooks callstack kf state kind =
- Call.apply (callstack, kf, state, kind);
- Db.Value.Call_Type_Value_Callbacks.apply (kind, state, callstack)
+ Call.apply (callstack, kf, state, kind)
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
| `Spec of state list
| `Body of results * int
| `Reuse of int
@@ -65,21 +65,9 @@ let register_call_results_hook f =
(fun (callstack, kf, state, results) -> f callstack kf state results)
let apply_call_results_hooks callstack kf state call_results =
- if Parameters.ValShowProgress.get ()
- && not (Call_Results.is_empty ()
- && Db.Value.Record_Value_Callbacks_New.is_empty ())
+ if Parameters.ValShowProgress.get () && not (Call_Results.is_empty ())
then Self.debug ~dkey "now calling Call_Results callbacks";
- Call_Results.apply (callstack, kf, state, call_results);
- let results =
- match call_results with
- | `Builtin _ | `Spec _ -> None
- | `Reuse i -> Some (Value_types.Reuse i)
- | `Body ({before_stmts; after_stmts}, i) ->
- Some (Value_types.NormalStore ((before_stmts, after_stmts), i))
- in
- Option.iter
- (fun r -> Db.Value.Record_Value_Callbacks_New.apply (callstack, r))
- results
+ Call_Results.apply (callstack, kf, state, call_results)
module Statement =
@@ -89,5 +77,4 @@ let register_statement_hook f =
Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
let apply_statement_hooks callstack stmt states =
- Statement.apply (callstack, stmt, states);
- Db.Value.Compute_Statement_Callbacks.apply (stmt, callstack, states)
+ Statement.apply (callstack, stmt, states)
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index 52d0d41330f31893650a9a232d2173376ea029bc..baa6dc0942ac19de3ec39a0ce11584b893626fe8 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -30,6 +30,11 @@
type state = Cvalue.Model.t
+(** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result, and the dependencies
+ of each zone written to. *)
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
| `Spec (** The specification is used to interpret the function. *)
@@ -53,7 +58,7 @@ type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/utils/eva_dynamic.ml b/src/plugins/eva/utils/eva_dynamic.ml
index ebfdc9384ad7969a7b94b12b290d03c92ccc47f0..c623675e2d22d95923eb4b3a9817f0c91cd2a8ec 100644
--- a/src/plugins/eva/utils/eva_dynamic.ml
+++ b/src/plugins/eva/utils/eva_dynamic.ml
@@ -62,5 +62,6 @@ module RteGen = struct
let mark_generated_rte () =
let list = all_statuses () in
let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in
- Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf)
+ Globals.Functions.iter
+ (fun kf -> if Function_calls.is_called kf then mark kf)
end
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 73dc03924ed0497f7e611994aeb9631803134333..1c3e435164f5ac9774c60b5390c7037c2061651d 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -79,8 +79,6 @@ let emitter =
~correctness:Parameters.parameters_correctness
~tuning:Parameters.parameters_tuning
-let () = Db.Value.emitter := emitter
-
let get_slevel kf =
try Parameters.SlevelFunction.find kf
with Not_found -> Parameters.SemanticUnrollingLevel.get ()
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 00f6e6a4283eb02d0687521a5b4f732f7c8fcb52..b26bb71371f86aef95114f2fda4217a5348188b6 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -499,7 +499,7 @@ module Parsed_Dynamic_Hints =
let dynamic_bases_of_lval states e offset =
let lv = (Mem e, offset) in
List.fold_left (fun acc' state ->
- let location = !Db.Value.lval_to_loc_state state lv in
+ let location = Cvalue_queries.lval_to_loc state lv in
Locations.Location_Bits.fold_bases
(fun base acc'' -> Base.Hptset.add base acc'')
location.Locations.loc acc'
@@ -561,7 +561,7 @@ let extract_per_function_hints fdec =
let per_function_hints = Per_Function_Hints.memo extract_per_function_hints
-let dynamic_widen_hints_hook (stmt, _callstack, states) =
+let dynamic_widen_hints_hook _callstack stmt states =
if Annotations.has_code_annot stmt then
let hs = parsed_dynamic_hints stmt in
if hs <> [] then
@@ -602,8 +602,7 @@ let dynamic_widen_hints_hook (stmt, _callstack, states) =
Dynamic_Hints.set hints;
end
-let () =
- Db.Value.Compute_Statement_Callbacks.extend_once dynamic_widen_hints_hook
+let () = Cvalue_callbacks.register_statement_hook dynamic_widen_hints_hook
let getWidenHints (kf:kernel_function) (stmt:stmt) =
let hints =
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/datascope.ml b/src/plugins/scope/datascope.ml
index 513145d4b9f96e3016858c565b2c4176e932d7b0..f992fda8da2b72a2dc2d59a582b7fa832b201391 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -637,9 +637,6 @@ let rm_asserts () =
CA_Map.iter aux to_be_removed
end
-
-let () = Db.register Db.Value.rm_asserts rm_asserts [@alert "-db_deprecated"]
-
let rm_asserts =
Dynamic.register
~comment:"Remove redundant alarms. Used by the Eva plugin."
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)))