module Taint_domain:sig
..end
Domain for a taint analysis.
include Abstract_domain.Leaf
val flag : Abstractions.flag
type
taint_error =
| |
NotComputed |
(* | The Eva analysis has not been run, or the taint domain was not enabled. | *) |
| |
Irrelevant |
(* | Properties other than assertions, invariants and preconditions are irrelevant here. | *) |
| |
LogicError |
(* | The memory zone on which the property depends could not be computed. | *) |
type
taint_ok =
| |
Data |
(* | Data-taint: there is a data dependency from the values provided by the attacker to the given property, meaning that the attacker may alter the values on which the property depends. | *) |
| |
Control |
(* | Control-taint: there is a control-dependency from the values provided by the attacker to the given property. The attacker cannot directly alter the values on which the property depends, but he may be able to choose the path where these values are computed. | *) |
| |
None |
(* | No taint: the property cannot be altered by the attacker. | *) |
typetaint_result =
(taint_ok, taint_error) Stdlib.result
val is_tainted_property : Property.t -> taint_result