From 3b19f39eb495ed1ba64920d454b5c0836afdc533 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 4 Aug 2020 11:12:33 +0200
Subject: [PATCH] [tests] use better C++ expression for testing, avoiding a
 Clang warning

---
 tests/specs/oracle/ternary_op_bts1532.res.oracle | 8 +++++---
 tests/specs/ternary_op_bts1532.cpp               | 4 ++--
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/tests/specs/oracle/ternary_op_bts1532.res.oracle b/tests/specs/oracle/ternary_op_bts1532.res.oracle
index 2421e2cd..b00b48dc 100644
--- a/tests/specs/oracle/ternary_op_bts1532.res.oracle
+++ b/tests/specs/oracle/ternary_op_bts1532.res.oracle
@@ -1,11 +1,13 @@
 [kernel] Parsing tests/specs/ternary_op_bts1532.cpp (external front-end)
 Now output intermediate result
 /* Generated by Frama-C */
-/*@ ensures \result ≡ (1 ≢ 0? 2: 3); */
-_Bool empty(void)
+/*@ ensures \result ≡ (\old(x) ≢ 0? 0: 1); */
+_Bool empty(int x)
 {
   _Bool __retres;
-  __retres = (_Bool)1;
+  int tmp;
+  if ((_Bool)(x != 0)) tmp = 0; else tmp = 1;
+  __retres = (_Bool)(tmp != 0);
   return __retres;
 }
 
diff --git a/tests/specs/ternary_op_bts1532.cpp b/tests/specs/ternary_op_bts1532.cpp
index 43454b19..3352d561 100644
--- a/tests/specs/ternary_op_bts1532.cpp
+++ b/tests/specs/ternary_op_bts1532.cpp
@@ -1,6 +1,6 @@
 
-//@ ensures \result == (1 ? 2 : 3);
-bool empty() { return (1 ? 2 : 3); }
+//@ ensures \result == (x ? 0 : 1);
+bool empty(int x) { return (x ? 0 : 1); }
 
 //@ logic integer min(integer x, integer y) = x < y ? x : y;
 
-- 
GitLab