From 2c13b06589604911a451979dd61fec684c7f65ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jan 2024 19:02:20 +0100
Subject: [PATCH] [wp] last comment
---
src/plugins/wp/Probe.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Probe.ml b/src/plugins/wp/Probe.ml
index fb0b079a581..9c5aa89d7e3 100644
--- a/src/plugins/wp/Probe.ml
+++ b/src/plugins/wp/Probe.ml
@@ -64,7 +64,7 @@ include Datatype.Make_with_collections(S)
let rec name_of_host = function
| TVar { lv_name = x } -> x
- | TResult _ -> "result"
+ | TResult _ -> "result" (* currently not used, but could be one day *)
| TMem t -> name_of_term t
and name_of_term (t : term) =
@@ -90,6 +90,7 @@ let annotations stmt =
let parse_probe : Acsl_extension.extension_typer =
fun context _loc terms ->
+ (* use default context of the code-annotation (like an assert clause) *)
let parse_term = context.type_term context context.pre_state in
Ext_terms (List.map parse_term terms)
--
GitLab