From 64a2dca5c8b0ccac3890e9f4e6eb91b5b6481d5e Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Wed, 10 Aug 2022 18:03:22 +0200
Subject: [PATCH] [e-acsl] test for function returning rationals
---
src/plugins/e-acsl/tests/arith/functions.c | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index f4b773c2774..9c327c0e1b9 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -43,6 +43,9 @@ int glob = 5;
// Test sums inside functions
/*@ logic integer f_sum (integer x) = \sum(1,x,\lambda integer y; 1); */
+// Test functions returning a rational
+/*@ logic real over(real a, real b) = a/b; */
+
int main(void) {
int x = 1, y = 2;
/*@ assert p1(x, y); */;
@@ -75,7 +78,9 @@ int main(void) {
double d = 2.0;
/*@ assert f2(d) > 0; */;
- /*@ assert f_sum (100) == 100; */
+ /*@ assert f_sum (100) == 100; */;
+
+ /*@ assert over(1., 2.) == 1./2.; */;
// not yet supported
/* /\*@ assert p_notyet(27); *\/ ; */
--
GitLab