From 7c296de953191948476dc091cb4fd7a6a3d4588a Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Thu, 28 Mar 2013 07:23:08 +0000
Subject: [PATCH] [e-acsl] resync for new definition of Cil_types.logic_real
---
src/plugins/e-acsl/translate.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 195ec761fbc..ebb85f3c6d5 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -84,7 +84,7 @@ let constant_to_exp ?(loc=Location.unknown) = function
| LStr s -> Cil.new_exp ?loc (Const (CStr s)), false
| LWStr s -> Cil.new_exp ?loc (Const (CWStr s)), false
| LChr c -> Cil.new_exp ?loc (Const (CChr c)), false
- | LReal((f, l, u), s) ->
+ | LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} ->
if l <> u then
Options.feedback ~current:true ~once:true
"approximating a real number by a float";
--
GitLab