[e-acsl] improve support for functions returning structures

src/plugins/e-acsl/src/code_generator/assigns.ml

@@ -81,10 +81,15 @@ let rec get_assigns_from ~loc env lprofile lv =
 
 (* Special case when the function takes an extra argument as its result:
    For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
-   expression [( *__retres_arg )[0]] *)
-let get_gmp_integer ~loc vi =
-  Smart_exp.lval
-    ~loc
-    (Mem
-       (Smart_exp.lval  ~loc (Var vi, NoOffset)),
-     (Index (Cil.zero ~loc, NoOffset)))
+   expression [( *__retres_arg )[0]]. For a struct argument, this function just
+   generates the variable corresponding to the argument. *)
+let get_assigned_var ~loc vi ret_gmp =
+  let var =
+    if ret_gmp then
+      Smart_exp.lval
+        ~loc
+        (Mem
+           (Smart_exp.lval  ~loc (Var vi, NoOffset)),
+         (Index (Cil.zero ~loc, NoOffset)))
+    else Smart_exp.lval ~loc (Var vi, NoOffset)
+  in Logic_utils.expr_to_term var

src/plugins/e-acsl/src/code_generator/assigns.mli

@@ -31,7 +31,7 @@ val get_assigns_from :
 (* @returns the list of expressions that are allowed to be used to assign the
    the result of a logic function *)
 
-val get_gmp_integer :
-  loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
+val get_assigned_var :
+  loc:Cil_types.location -> Cil_types.varinfo -> bool -> Cil_types.term
 (* @returns the expression that gets assigned when the result of the function is
-   a pointer on a GMP type *)
+   passed as an additional argument *)

src/plugins/e-acsl/src/code_generator/logic_functions.ml

@@ -55,7 +55,14 @@ let term_to_exp_ref
 
 (* @return true iff the result of the function is provided by reference as the
    first extra argument at each call *)
-let result_as_extra_argument = Gmp_types.Z.is_t
+let result_as_extra_argument typ =
+  let is_composite = function
+    | TComp _ | TPtr _ | TArray _ -> true
+    | TInt _ | TVoid _  | TFloat _ | TFun _ | TNamed _ | TEnum _
+    | TBuiltin_va_list _ -> false
+  in
+  Gmp_types.Z.is_t typ ||
+  is_composite typ
 (* TODO: to be extended to any compound type? E.g. returning a struct is not
    good practice... *)
 
@@ -151,6 +158,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
   in
   (* build the varinfo storing the result *)
   let res_as_extra_arg = result_as_extra_argument ret_ty in
+  let ret_gmp = Gmp_types.Z.is_t ret_ty in
   let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
     let vname = "__retres" in
     if res_as_extra_arg then
@@ -209,7 +217,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
     let assigned_var =
       Logic_const.new_identified_term
         (if res_as_extra_arg then
-           Logic_utils.expr_to_term (Assigns.get_gmp_integer ~loc ret_vi)
+           Assigns.get_assigned_var ~loc ret_vi ret_gmp
          else
            Logic_const.tresult fundec.svar.vtype)
     in

src/plugins/e-acsl/tests/arith/functions.c

@@ -67,6 +67,7 @@ int main(void) {
   mystruct m;
   m.k = 8;
   m.l = 9;
+  /*@ assert \let r = t1(m); r.k == 8; */;
   /*@ assert t2(t1(m)) == 17; */;
 
   k(9);

src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle

 [e-acsl] beginning translation.
+[e-acsl] functions.c:70: Warning: 
+  E-ACSL construct `function application' is not yet supported.
+  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] functions.c:48: Warning: 
   function __e_acsl_assert_register_int: precondition data->values == \null ||
@@ -46,16 +49,23 @@
   function __e_acsl_assert_register_struct: precondition data->values == \null ||
                                                          \valid(data->values) got status unknown.
 [eva:alarm] functions.c:70: Warning: 
+  function __e_acsl_assert_register_struct: precondition data->values == \null ||
+                                                         \valid(data->values) got status unknown.
+[eva:alarm] functions.c:70: Warning: assertion got status unknown.
+[eva:alarm] functions.c:71: Warning: 
+  function __e_acsl_assert_register_struct: precondition data->values == \null ||
+                                                         \valid(data->values) got status unknown.
+[eva:alarm] functions.c:71: Warning: 
   function __e_acsl_assert_register_long: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
 [eva:alarm] functions.c:28: Warning: 
   function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                       \valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning: 
+[eva:alarm] functions.c:76: Warning: 
   non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] functions.c:75: Warning: 
+[eva:alarm] functions.c:76: Warning: 
   function __e_acsl_assert_register_double: precondition data->values == \null ||
                                                          \valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning: 
+[eva:alarm] functions.c:76: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:77: Warning: assertion got status unknown.
+[eva:alarm] functions.c:78: Warning: assertion got status unknown.

src/plugins/e-acsl/tests/arith/oracle/gen_functions.c

@@ -325,63 +325,84 @@ int main(void)
   m.k = 8;
   m.l = 9;
   {
+    mystruct __gen_e_acsl_r;
     mystruct __gen_e_acsl_t1_2;
-    long __gen_e_acsl_t2_2;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
       {.values = (void *)0};
     __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
-    __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_2);
+    __gen_e_acsl_r = __gen_e_acsl_t1_2;
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0,
+                                 __gen_e_acsl_r.k);
     __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"m");
     __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"t1(m)");
-    __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_11,"t2(t1(m))",
-                                  0,__gen_e_acsl_t2_2);
     __gen_e_acsl_assert_data_11.blocking = 1;
     __gen_e_acsl_assert_data_11.kind = "Assertion";
-    __gen_e_acsl_assert_data_11.pred_txt = "t2(t1(m)) == 17";
+    __gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8";
     __gen_e_acsl_assert_data_11.file = "functions.c";
     __gen_e_acsl_assert_data_11.fct = "main";
     __gen_e_acsl_assert_data_11.line = 70;
-    __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_11);
+    __e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
   }
-  /*@ assert t2(t1(m)) == 17; */ ;
-  __gen_e_acsl_k(9);
-  double d = 2.0;
+  /*@ assert \let r = t1(m); r.k == 8; */ ;
   {
-    double __gen_e_acsl_f2_2;
+    mystruct __gen_e_acsl_t1_4;
+    long __gen_e_acsl_t2_2;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
       {.values = (void *)0};
-    __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
-    __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"d",d);
-    __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"f2(d)",
-                                    __gen_e_acsl_f2_2);
+    __gen_e_acsl_t1_4 = __gen_e_acsl_t1(m);
+    __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4);
+    __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m");
+    __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)");
+    __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_12,"t2(t1(m))",
+                                  0,__gen_e_acsl_t2_2);
     __gen_e_acsl_assert_data_12.blocking = 1;
     __gen_e_acsl_assert_data_12.kind = "Assertion";
-    __gen_e_acsl_assert_data_12.pred_txt = "f2(d) > 0";
+    __gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17";
     __gen_e_acsl_assert_data_12.file = "functions.c";
     __gen_e_acsl_assert_data_12.fct = "main";
-    __gen_e_acsl_assert_data_12.line = 75;
-    __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_12);
+    __gen_e_acsl_assert_data_12.line = 71;
+    __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
   }
-  /*@ assert f2(d) > 0; */ ;
+  /*@ assert t2(t1(m)) == 17; */ ;
+  __gen_e_acsl_k(9);
+  double d = 2.0;
   {
-    int __gen_e_acsl_f_sum_2;
+    double __gen_e_acsl_f2_2;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_13 =
       {.values = (void *)0};
-    __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
-    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"f_sum(100)",
-                                 0,__gen_e_acsl_f_sum_2);
+    __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
+    __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"d",d);
+    __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"f2(d)",
+                                    __gen_e_acsl_f2_2);
     __gen_e_acsl_assert_data_13.blocking = 1;
     __gen_e_acsl_assert_data_13.kind = "Assertion";
-    __gen_e_acsl_assert_data_13.pred_txt = "f_sum(100) == 100";
+    __gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0";
     __gen_e_acsl_assert_data_13.file = "functions.c";
     __gen_e_acsl_assert_data_13.fct = "main";
-    __gen_e_acsl_assert_data_13.line = 77;
-    __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
-                    & __gen_e_acsl_assert_data_13);
+    __gen_e_acsl_assert_data_13.line = 76;
+    __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13);
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
   }
+  /*@ assert f2(d) > 0; */ ;
+  {
+    int __gen_e_acsl_f_sum_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
+      {.values = (void *)0};
+    __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,"f_sum(100)",
+                                 0,__gen_e_acsl_f_sum_2);
+    __gen_e_acsl_assert_data_14.blocking = 1;
+    __gen_e_acsl_assert_data_14.kind = "Assertion";
+    __gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100";
+    __gen_e_acsl_assert_data_14.file = "functions.c";
+    __gen_e_acsl_assert_data_14.fct = "main";
+    __gen_e_acsl_assert_data_14.line = 78;
+    __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
+                    & __gen_e_acsl_assert_data_14);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
+  }
   /*@ assert f_sum(100) == 100; */ ;
   __retres = 0;
   __e_acsl_memory_clean();