From 62f4703064f6194cbe59bec13f620831771aeac0 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Fri, 30 Aug 2024 15:27:50 +0200
Subject: [PATCH] [e-acsl] type arguments of unsupported Tapp variants
The previous commit showcases a simple piece of code that causes an
exception. This commit fixes this exception.
---
src/plugins/e-acsl/doc/Changelog | 2 +
src/plugins/e-acsl/src/analyses/typing.ml | 2 +
.../constructs/oracle/axiomatic.res.oracle | 6 +--
.../tests/constructs/oracle/gen_axiomatic.c | 40 +++++++------------
4 files changed, 20 insertions(+), 30 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index e7cd2d6a7fe..912d6e60d54 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 90694e91696..4d660be4b00 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 ebbe084569c..780f50d206f 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 c43f0f87008..526a195441b 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;
}
--
GitLab