From 4e8ce94e8d5df885e6867eac60648ff58b40feb1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 9 Feb 2021 13:10:55 +0100
Subject: [PATCH] [Eva] Registers a new abstract domain in the engine.
---
Makefile | 2 +-
src/plugins/value/domains/taint_domain.ml | 23 ++++++++++++++++++
src/plugins/value/domains/taint_domain.mli | 27 ++++++++++++++++++++++
src/plugins/value/engine/abstractions.ml | 4 ++++
src/plugins/value/engine/abstractions.mli | 1 +
5 files changed, 56 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/value/domains/taint_domain.ml
create mode 100644 src/plugins/value/domains/taint_domain.mli
diff --git a/Makefile b/Makefile
index 50d209e216a..27461c0c186 100644
--- a/Makefile
+++ b/Makefile
@@ -881,7 +881,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/builtins_memory domains/cvalue/builtins_print_c \
domains/cvalue/builtins_watchpoint \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
- domains/inout_domain \
+ domains/inout_domain domains/taint_domain \
legacy/eval_terms legacy/eval_annots \
domains/powerset engine/transfer_logic \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
new file mode 100644
index 00000000000..8431bf7e317
--- /dev/null
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Inout_domain.D
diff --git a/src/plugins/value/domains/taint_domain.mli b/src/plugins/value/domains/taint_domain.mli
new file mode 100644
index 00000000000..53a22a8a357
--- /dev/null
+++ b/src/plugins/value/domains/taint_domain.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Domain for a taint analysis. *)
+
+include Abstract_domain.Leaf
+ with type value = Cvalue.V.t
+ and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5c01025c3d8..275b6cef1b2 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -162,6 +162,10 @@ module Config = struct
"Infers the inputs and outputs of each function."
(module Inout_domain.D)
+ let taint = make 5 "taint" ~experimental:true
+ "TODO"
+ (module Taint_domain)
+
let traces =
make 2 "traces" ~experimental:true
"Builds an over-approximation of all the traces that lead \
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 2ba4de799b6..38364d3fc5b 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -155,6 +155,7 @@ module Config : sig
val octagon: flag
val bitwise: flag
val inout: flag
+ val taint: flag
val sign: flag
val traces: flag
val printer: flag
--
GitLab