From f3f0502f988300b6dfd088ba35f39dc421f30263 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 14 Feb 2019 19:53:38 +0100
Subject: [PATCH] [ACSL] coerce comparisons from floats to real
---
src/kernel_services/ast_queries/logic_typing.ml | 5 +++--
tests/spec/float-acsl.i | 10 ++++++++++
tests/spec/oracle/float-acsl.res.oracle | 11 +++++++++++
3 files changed, 24 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 92b4d3ab5e7..520ec3756d9 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1710,10 +1710,10 @@ struct
in
let rec aux lty1 lty2 =
match (unroll_type lty1), (unroll_type lty2) with
- | t1, t2 when is_same_type t1 t2 -> t1
| Ctype ty1, Ctype ty2 ->
if isIntegralType ty1 && isIntegralType ty2 then
- if (isSignedInteger ty1) <> (isSignedInteger ty2) then
+ if is_same_type lty1 lty2 then lty1
+ else if (isSignedInteger ty1) <> (isSignedInteger ty2) then
(* in ACSL, the comparison between 0xFFFFFFFF seen as int and
unsigned int is not true: we really have to operate at
the integer level.
@@ -1760,6 +1760,7 @@ struct
(* implicit conversion to set *)
| Ltype ({lt_name = "set"} as lt,[t1]), t2
| t1, Ltype({lt_name="set"} as lt,[t2]) -> Ltype(lt,[aux t1 t2])
+ | t1, t2 when is_same_type t1 t2 -> t1
| _ ->
C.error loc "types %a and %a are not convertible"
Cil_printer.pp_logic_type lty1 Cil_printer.pp_logic_type lty2
diff --git a/tests/spec/float-acsl.i b/tests/spec/float-acsl.i
index 3e33afc86d0..571ae93e666 100644
--- a/tests/spec/float-acsl.i
+++ b/tests/spec/float-acsl.i
@@ -1,3 +1,7 @@
+/* run.config*
+STDOPT: +"-kernel-msg-key printer:logic-coercions"
+*/
+
/*@
assigns \result \from \nothing;
ensures \le_double(\result, (double)0.0);
@@ -21,6 +25,12 @@ double minus_one(void);
*/
float minus_onef(void);
+/*@ requires x <= y;
+ assigns \result \from x,y;
+ ensures x <= \result <= y;
+*/
+float test(float x, float y);
+
void main() {
double mone = minus_one();
float monef = minus_onef();
diff --git a/tests/spec/oracle/float-acsl.res.oracle b/tests/spec/oracle/float-acsl.res.oracle
index 5489ef5e784..3aa9fe9e8fb 100644
--- a/tests/spec/oracle/float-acsl.res.oracle
+++ b/tests/spec/oracle/float-acsl.res.oracle
@@ -22,6 +22,17 @@ double minus_one(void);
*/
float minus_onef(void);
+/*@ requires
+ /* (coercion to:℠*/x/* ) */ ≤ /* (coercion to:℠*/y/* ) */;
+ ensures
+ /* (coercion to:℠*/\old(x)/* ) */ ≤
+ /* (coercion to:℠*/\result/* ) */ ≤
+ /* (coercion to:â„ */\old(y)/* ) */;
+ assigns \result;
+ assigns \result \from x, y;
+ */
+float test(float x, float y);
+
void main(void)
{
double mone = minus_one();
--
GitLab