From 88668f6b39da08bc0abe41bff4ef8edb59080854 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 16 Mar 2020 15:37:36 +0100
Subject: [PATCH] [ACSL] fixes casts to unsigned short int (add test file)
---
tests/spec/cast_int.i | 6 ++++++
tests/spec/oracle/cast_int.res.oracle | 12 ++++++++++++
2 files changed, 18 insertions(+)
create mode 100644 tests/spec/cast_int.i
create mode 100644 tests/spec/oracle/cast_int.res.oracle
diff --git a/tests/spec/cast_int.i b/tests/spec/cast_int.i
new file mode 100644
index 00000000000..21505c3ff13
--- /dev/null
+++ b/tests/spec/cast_int.i
@@ -0,0 +1,6 @@
+unsigned short int toto;
+
+/*@ensures toto==(unsigned short int)param;*/
+int F(int param){
+return 0;
+}
diff --git a/tests/spec/oracle/cast_int.res.oracle b/tests/spec/oracle/cast_int.res.oracle
new file mode 100644
index 00000000000..23501c9b3c5
--- /dev/null
+++ b/tests/spec/oracle/cast_int.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/spec/cast_int.i (no preprocessing)
+/* Generated by Frama-C */
+unsigned short toto;
+/*@ ensures toto ≡ (unsigned short)\old(param); */
+int F(int param)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab