Merge branch 'jan/eacsl-fix-typing' into 'master'

[e-acsl] type arguments of unsupported Papp/Tapp variants

See merge request frama-c/frama-c!4734

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
 
@@ -764,6 +766,7 @@ and type_bound_variables ~profile (t1, lv, t2) =
   ignore(type_term ~use_gmp_opt:false ~ctx ~profile t2)
 
 and type_predicate ~profile p =
+  Options.feedback ~dkey ~level:3 "typing predicate: %a" Printer.pp_predicate p;
   let
     do_both f g = (try f() with e -> try g(); raise e with | _ -> raise e); g()
   in
@@ -774,11 +777,11 @@ and type_predicate ~profile p =
   | Pfalse | Ptrue -> ()
   | Papp(li, _, args) ->
     begin
+      List.iter
+        (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
+        args;
       match li.l_body with
       | LBpred p ->
-        List.iter
-          (fun x -> ignore (type_term ~use_gmp_opt: true ~profile x))
-          args;
         let new_profile =
           Profile.make
             li.l_profile

src/plugins/e-acsl/tests/constructs/axiomatic.c

+/* run.config
+COMMENT: [e-acsl] Failure: typing was not performed on construct s in phase `analysis:typing'
+*/
+
+/*@
+  axiomatic p {
+    predicate p(ℤ s);
+  }
+*/
+
+/*@ ensures p(s); */
+void f(int s) {
+  return;
+}
+
+int main() {
+  f(2);
+}
+
+/*@
+
+axiomatic g {
+  logic ℤ g(int c)
+    reads c;
+}
+
+@*/
+
+/*@ ensures g(t) == 0; */
+int h(const int t) {
+  return 0;
+}
+
+int i() {
+  h(1);
+}

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

+[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:29: Warning: 
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] axiomatic.c:11: 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] axiomatic.c:11: Warning: 
+  function __gen_e_acsl_f: postcondition got status unknown.

src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c

+/* 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;
+
+/*@ axiomatic p {
+      predicate p(integer s) ;
+      
+      }
+
+*/
+/*@ ensures p(\old(s)); */
+void __gen_e_acsl_f(int s);
+
+void f(int s)
+{
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __gen_e_acsl_f(2);
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+/*@ axiomatic g {
+      logic integer g(int c) 
+        reads c;
+      
+      }
+
+*/
+/*@ ensures g(\old(t)) == 0; */
+int __gen_e_acsl_h(int const t);
+
+int h(int const t)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+int i(void)
+{
+  int __retres;
+  __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;
+    __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 = "i";
+    __gen_e_acsl_assert_data.line = 36;
+    __gen_e_acsl_assert_data.name = "missing_return";
+    __e_acsl_assert(0,& __gen_e_acsl_assert_data);
+  }
+  /*@ assert missing_return: \false; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ ensures g(\old(t)) == 0; */
+int __gen_e_acsl_h(int const t)
+{
+  int __gen_e_acsl_at;
+  int __retres;
+  __gen_e_acsl_at = t;
+  __retres = h(t);
+  return __retres;
+}
+
+/*@ ensures p(\old(s)); */
+void __gen_e_acsl_f(int s)
+{
+  int __gen_e_acsl_at;
+  __gen_e_acsl_at = s;
+  f(s);
+  return;
+}
+
+