diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index e7cd2d6a7fea29e37d29d29638e5b22d3e3fefaa..912d6e60d5491652ccb349e5136c59d2f1819dbf 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -25,6 +25,8 @@ Plugin E-ACSL <next-release> ############################################################################### +-* 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/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index 90694e9169659e528d2d06079e9e6110ae420215..4d660be4b00bc720ce11e1207c50203195dca545 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -653,8 +653,10 @@ let rec type_term Error.not_yet "logic functions or predicates with no definition \ nor reads clause") | LBreads _ -> + type_args type_arg; Error.not_yet "logic functions or predicates performing read accesses" | LBinductive _ -> + type_args type_arg; Error.not_yet "inductive logic functions" end diff --git a/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle index ebbe084569ccc9a1ce67c2624868252d0dae5c32..780f50d206f595799a9c8274c18fd2161361dbfe 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle +++ b/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle @@ -1,9 +1,7 @@ -[kernel:CERT:MSC:37] axiomatic.c:29: Warning: - Body of function h falls-through. Adding a return statement -[kernel:CERT:MSC:37] axiomatic.c:33: Warning: +[kernel:CERT:MSC:37] axiomatic.c:36: Warning: Body of function i falls-through. Adding a return statement [e-acsl] beginning translation. -[e-acsl] axiomatic.c:28: Warning: +[e-acsl] axiomatic.c:29: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c index c43f0f870083ffa54f24598ca6d1d791d3be94fc..526a195441b51795c1e4c4a6b9e92af0a8a42079 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c +++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c @@ -33,38 +33,26 @@ int main(void) } /*@ axiomatic g { - logic integer g(char c) + logic integer g(int c) reads c; } */ -/*@ ensures g(\old(s)) == 0; */ -char __gen_e_acsl_h(char const s); +/*@ ensures g(\old(t)) == 0; */ +int __gen_e_acsl_h(int const t); -char h(char const s) +int h(int const t) { - char __retres; - { - __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0}; - __gen_e_acsl_assert_data.blocking = 1; - __gen_e_acsl_assert_data.kind = "Assertion"; - __gen_e_acsl_assert_data.pred_txt = "\\false"; - __gen_e_acsl_assert_data.file = "axiomatic.c"; - __gen_e_acsl_assert_data.fct = "h"; - __gen_e_acsl_assert_data.line = 29; - __gen_e_acsl_assert_data.name = "missing_return"; - __e_acsl_assert(0,& __gen_e_acsl_assert_data); - } - /*@ assert missing_return: \false; */ ; - __retres = (char)0; + int __retres; + __retres = 0; return __retres; } int i(void) { int __retres; - __gen_e_acsl_h((char)'c'); + __gen_e_acsl_h(1); { __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0}; __gen_e_acsl_assert_data.blocking = 1; @@ -72,7 +60,7 @@ int i(void) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "axiomatic.c"; __gen_e_acsl_assert_data.fct = "i"; - __gen_e_acsl_assert_data.line = 33; + __gen_e_acsl_assert_data.line = 36; __gen_e_acsl_assert_data.name = "missing_return"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); } @@ -81,13 +69,13 @@ int i(void) return __retres; } -/*@ ensures g(\old(s)) == 0; */ -char __gen_e_acsl_h(char const s) +/*@ ensures g(\old(t)) == 0; */ +int __gen_e_acsl_h(int const t) { - char __gen_e_acsl_at; - char __retres; - __gen_e_acsl_at = s; - __retres = h(s); + int __gen_e_acsl_at; + int __retres; + __gen_e_acsl_at = t; + __retres = h(t); return __retres; }