From 6f28678e41bfc4f7a6e6caaa6d46436fa8cf2f48 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 13 Oct 2020 09:07:21 +0200
Subject: [PATCH] [Eva] Minor fix in recursion.ml.
---
src/plugins/value/engine/recursion.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 65d34306b0e..78f0d88d84a 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -54,7 +54,7 @@ let mark_unknown_requires kinstr kf funspec =
let status = Property_status.Dont_know in
let emit_behavior behavior =
let emit_predicate predicate =
- let ip = Property.ip_of_requires kf kinstr behavior predicate in
+ let ip = Property.ip_of_requires kf Kglobal behavior predicate in
Statuses_by_call.setup_precondition_proxy kf ip;
let property = Statuses_by_call.precondition_at_call kf ip stmt in
Property_status.emit ~distinct:true emitter ~hyps:[] property status
--
GitLab