[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

@@ -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
 
 ###############################################################################

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
 

src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle

-[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.

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;
 }