diff --git a/Makefile b/Makefile index 50d209e216a4a18d429306bd3e86f2a42d38e01b..27461c0c1863e3a292ec9e703da7cd371726728f 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 0000000000000000000000000000000000000000..8431bf7e3175c9dd5ef2f93254077320db65c189 --- /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 0000000000000000000000000000000000000000..53a22a8a35725604a2cb712a6de7af9c672078df --- /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 5c01025c3d8f4772df6b90084451bb5efa0c2feb..275b6cef1b2cd3953a1e448bc1b7465426143302 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 2ba4de799b6923e7aa8c019804e4488eb81426fb..38364d3fc5b1fb1bbfc52647df1963840922a6fb 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