[Eva] Results: exports new function to evaluate the taint of a memory zone.
In the taint domain: - exports generic function [is_tainted] evaluating the taint of a memory zone in a given state. Removes function [is_tainted_property]. - returns Direct/Indirect/Untainted instead of Data/Control/None. Implements [is_tainted_property] in the general request, using [Results.is_tainted].
Showing
- ivette/src/frama-c/plugins/eva/api/general/index.ts 4 additions, 4 deletionsivette/src/frama-c/plugins/eva/api/general/index.ts
- src/plugins/eva/Eva.mli 16 additions, 0 deletionssrc/plugins/eva/Eva.mli
- src/plugins/eva/api/general_requests.ml 49 additions, 17 deletionssrc/plugins/eva/api/general_requests.ml
- src/plugins/eva/domains/taint_domain.ml 15 additions, 48 deletionssrc/plugins/eva/domains/taint_domain.ml
- src/plugins/eva/domains/taint_domain.mli 5 additions, 21 deletionssrc/plugins/eva/domains/taint_domain.mli
- src/plugins/eva/utils/results.ml 14 additions, 0 deletionssrc/plugins/eva/utils/results.ml
- src/plugins/eva/utils/results.mli 16 additions, 0 deletionssrc/plugins/eva/utils/results.mli
Loading
Please register or sign in to comment