From 21615c0fe23ee73ecb4fae34f17a2d41b14caf91 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 30 Mar 2021 17:44:12 +0200
Subject: [PATCH] [eacsl] Fix location on funspec unsupported clauses messages
---
src/plugins/e-acsl/src/code_generator/translate_annots.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index d337b04075c..27a8185b7ca 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -67,8 +67,9 @@ let pre_funspec kf kinstr env funspec =
funspec;
env
in
- let env = convert_unsupported_clauses env in
let loc = Kernel_function.get_location kf in
+ Cil.CurrentLoc.set loc;
+ let env = convert_unsupported_clauses env in
let contract = Contract.create ~loc funspec in
Env.with_rte env true
~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
--
GitLab