From 31b33fa2e645749f91d98fc4e1fb90cb701c0ed1 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 3 Sep 2024 11:43:50 +0200
Subject: [PATCH] [e-acsl] add pathological case for negative integer handling
The -rte flag causes the generation of a negative integer in a rational
context. In that case Translate_terms.constant_to_exp converts the
integer to a real string representation by converting the integer to a
string and then normalising that string using Gmp.Q.normalize_str.
However Gmp.Q.normalize_str does not correctly handle negative integers.
Note that negative integers do not occur when writing for instance -1 in
the source file as it is parsed as TUnOp(Neg, _).
---
src/plugins/e-acsl/tests/arith/neg_rte_int.c | 11 +++++++++++
1 file changed, 11 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/arith/neg_rte_int.c
diff --git a/src/plugins/e-acsl/tests/arith/neg_rte_int.c b/src/plugins/e-acsl/tests/arith/neg_rte_int.c
new file mode 100644
index 00000000000..d31e60b261b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/neg_rte_int.c
@@ -0,0 +1,11 @@
+/* run.config
+ STDOPT: #"-rte"
+ COMMENT: Generates an RTE with a negative integer
+ COMMENT: (The negative integer being the lower bound of signed chars)
+ COMMENT: This regression test ensures that E-ACSL correctly handles negative integers.
+*/
+char c;
+float f;
+void main() {
+ c = f + 0.5;
+}
--
GitLab