From 8d7b41fc76c07fd67991657a36be67f26b2995c5 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 28 Mar 2019 15:20:19 +0100
Subject: [PATCH] [ACSL] adds some tests about ACSL cast

---
 tests/spec/logic_type.c                 |  8 ++++++++
 tests/spec/oracle/logic_type.res.oracle | 11 +++++++++++
 2 files changed, 19 insertions(+)

diff --git a/tests/spec/logic_type.c b/tests/spec/logic_type.c
index 0b8380d9dc8..008bec88b3c 100644
--- a/tests/spec/logic_type.c
+++ b/tests/spec/logic_type.c
@@ -26,3 +26,11 @@ Point tab[3];
 void h(void) {
   f(tab) ;
 }
+
+//@ logic t t_from_t(t x) = (t) x;
+
+//@ logic _Bool _Bool_from_boolean(boolean b) = (_Bool) b;
+
+//@ logic boolean boolean_from_integer(integer b) = (boolean) b;
+//@ logic boolean boolean_from_int(int b) = (boolean) b;
+//@ logic boolean boolean_from_Bool(_Bool b) = (boolean) b;
diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index 4521f06fa5f..c9a81bc49b7 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -51,4 +51,15 @@ void h(void)
   return;
 }
 
+/*@ logic t t_from_t(t x) = x;
+ */
+/*@ logic _Bool _Bool_from_boolean(𝔹 b) = (_Bool)b;
+ */
+/*@ logic 𝔹 boolean_from_integer(ℤ b) = b;
+ */
+/*@ logic 𝔹 boolean_from_int(int b) = b;
+ */
+/*@ logic 𝔹 boolean_from_Bool(_Bool b) = b;
+
+*/
 
-- 
GitLab