From d594f758cdbe217359a421167e4e22ab2bb829de Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 3 Sep 2024 11:27:44 +0200
Subject: [PATCH] [e-acsl] correctly handle negative integers in rational
context
This fixes the pathological example from the previous commit by
adding missing code to Gmp.Q.normalize_str that handles signs.
---
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/src/code_generator/gmp.ml | 3 +
.../tests/arith/oracle/gen_neg_rte_int.c | 80 +++++++++++++++++++
.../tests/arith/oracle/neg_rte_int.res.oracle | 9 +++
4 files changed, 93 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/gen_neg_rte_int.c
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/neg_rte_int.res.oracle
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 912d6e60d54..8a8cf08be9b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
###############################################################################
+-* E-ACSL [2024-09-03] handle negative integers generated by RTE
-* E-ACSL [2024-08-30] fix typing exception occurring for applications
of axiomatically defined premises and logic functions
-* E-ACSL [2024-06-20] fix typing of logic functions over rationals
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 51d50aaa518..1ac1f29301a 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -290,6 +290,9 @@ module Q = struct
str
else
match String.unsafe_get str i with
+ | '-' when i = 0 ->
+ Bytes.unsafe_set buf i '-';
+ pre str len buf (i + 1)
| '.' ->
mid buf len;
post str len buf (len + 1) (i + 1)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_neg_rte_int.c b/src/plugins/e-acsl/tests/arith/oracle/gen_neg_rte_int.c
new file mode 100644
index 00000000000..f44035f04d8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_neg_rte_int.c
@@ -0,0 +1,80 @@
+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+char c;
+float f;
+void main(void)
+{
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ {
+ __e_acsl_mpq_t __gen_e_acsl_;
+ __e_acsl_mpq_t __gen_e_acsl__2;
+ __e_acsl_mpq_t __gen_e_acsl__3;
+ __e_acsl_mpq_t __gen_e_acsl_add;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpq_t __gen_e_acsl__4;
+ int __gen_e_acsl_lt_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_str(__gen_e_acsl_,"-129",10);
+ __gmpq_init(__gen_e_acsl__2);
+ __gmpq_set_d(__gen_e_acsl__2,(double)f);
+ __gmpq_init(__gen_e_acsl__3);
+ __gmpq_set_d(__gen_e_acsl__3,0.5);
+ __gmpq_init(__gen_e_acsl_add);
+ __gmpq_add(__gen_e_acsl_add,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
+ __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
+ __e_acsl_assert_register_float(& __gen_e_acsl_assert_data,"f",f);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "-129 < (double)f + 0.5";
+ __gen_e_acsl_assert_data.file = "neg_rte_int.c";
+ __gen_e_acsl_assert_data.fct = "main";
+ __gen_e_acsl_assert_data.line = 10;
+ __gen_e_acsl_assert_data.name = "rte/float_to_int";
+ __e_acsl_assert(__gen_e_acsl_lt < 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_str(__gen_e_acsl__4,"128",10);
+ __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert_register_float(& __gen_e_acsl_assert_data_2,"f",f);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Assertion";
+ __gen_e_acsl_assert_data_2.pred_txt = "(double)f + 0.5 < 128";
+ __gen_e_acsl_assert_data_2.file = "neg_rte_int.c";
+ __gen_e_acsl_assert_data_2.fct = "main";
+ __gen_e_acsl_assert_data_2.line = 10;
+ __gen_e_acsl_assert_data_2.name = "rte/float_to_int";
+ __e_acsl_assert(__gen_e_acsl_lt_2 < 0,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl__2);
+ __gmpq_clear(__gen_e_acsl__3);
+ __gmpq_clear(__gen_e_acsl_add);
+ __gmpq_clear(__gen_e_acsl__4);
+ }
+ /*@ assert
+ rte: is_nan_or_infinite:
+ \is_finite(\add_double((double)f, (double)0.5));
+ */
+ /*@ assert rte: float_to_int: (double)f + 0.5 < 128; */
+ /*@ assert rte: float_to_int: -129 < (double)f + 0.5; */
+ c = (char)((double)f + 0.5);
+ __e_acsl_memory_clean();
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle/neg_rte_int.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/neg_rte_int.res.oracle
new file mode 100644
index 00000000000..59dd7cf1d5e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/neg_rte_int.res.oracle
@@ -0,0 +1,9 @@
+[e-acsl] beginning translation.
+[e-acsl] neg_rte_int.c:10: Warning:
+ E-ACSL construct
+ `logic functions or predicates with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] neg_rte_int.c:10: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
--
GitLab