diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index c1f6cc09d3e171e3d92c6bcbf84920061eace966..abd2c08e061c483ab77afb401484158e7d825f51 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-08-22] fix arity confusion of generated functions. diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml index 51d50aaa5186fb5403f70bc17617a4b971bf2bef..1ac1f29301a57ef19b56382cb8c56ea4df2d173a 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/neg_rte_int.c b/src/plugins/e-acsl/tests/arith/neg_rte_int.c new file mode 100644 index 0000000000000000000000000000000000000000..d31e60b261b9eb6a9e5923f5463578f6918f55af --- /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; +} 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 0000000000000000000000000000000000000000..f44035f04d84920ca58a5f8ad108ba8478d8004e --- /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 0000000000000000000000000000000000000000..59dd7cf1d5ea2b31e9cac614b591fc43533875dd --- /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.