From 995e6b5a67bfb01bb7d8750b40951b0c6c38278c Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Fri, 14 Sep 2018 17:11:31 +0200
Subject: [PATCH] No coercion in mmodel_call_with_ranges
---
src/plugins/e-acsl/translate.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index e2f349e6ecf..ad972d9e986 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -762,7 +762,8 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
in
let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
let p_quantified =
- let loc = Some (loc :> Cil_types.location) in
+ (* [loc] prevents a type error with eta-expansion and label *)
+ let loc = Some loc in
let call f = f ?loc (Logic_const.here_label, t') in
match name with
| "valid" -> call Logic_const.pvalid
--
GitLab