From c767103a766b57cfd6df93b493c23cce8ce1dddb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 29 Jun 2021 14:56:27 +0200
Subject: [PATCH] [Eva] Taint domain: fixes "taints" extension for behaviors.
Parses the extension terms in the post-state.
---
src/plugins/value/domains/taint_domain.ml | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 05a914e0b1a..b1406f526ec 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -367,13 +367,18 @@ let () =
(* Registers ACSL extension "taint" (statement annotation)
and "taints" (behavior extension). *)
let () =
- let typer context _loc args =
+ let typer kind context _loc args =
let open Logic_typing in
- let parse context = context.type_term context context.pre_state in
+ let get_state context =
+ match kind with
+ | `Pre -> context.pre_state
+ | `Post -> context.post_state [Normal]
+ in
+ let parse context = context.type_term context (get_state context) in
Ext_terms (List.map (parse context) args)
in
- Acsl_extension.register_behavior "taints" typer false;
- Acsl_extension.register_code_annot_next_stmt "taint" typer false
+ Acsl_extension.register_behavior "taints" (typer `Post) false;
+ Acsl_extension.register_code_annot_next_stmt "taint" (typer `Pre) false
(* Interpretation of logic by the taint domain, using the cvalue domain. *)
module TaintLogic = struct
--
GitLab