From 395302f8c8f1e481f01e63055c4a668988c2651b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 25 Mar 2014 11:06:56 +0100
Subject: [PATCH] code fix according to deletion of Cil.kinteger64_repr
---
src/plugins/e-acsl/translate.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 97c698e9669..a19406bf900 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -81,11 +81,13 @@ let name_of_mpz_arith_bop = function
| Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
let constant_to_exp ~loc = function
- | Integer(n, s) ->
+ | Integer(n, repr) ->
(try
- let k = Typing.typ_of_integer n (Integer.ge n Integer.zero) in
- if Typing.is_representable n k then Cil.kinteger64_repr ~loc k n s, false
- else raise Cil.Not_representable
+ let kind = Typing.typ_of_integer n (Integer.ge n Integer.zero) in
+ if Typing.is_representable n kind then
+ Cil.kinteger64 ~loc ~kind ?repr n, false
+ else
+ raise Cil.Not_representable
with Cil.Not_representable ->
Cil.mkString ~loc (Integer.to_string n), true)
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
--
GitLab