sync with frama-c/frama-c!1930

src/plugins/e-acsl/dup_functions.ml

@@ -134,7 +134,7 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
   let res =
     let ty = Kernel_function.get_return_type kf in
     if Cil.isVoidType ty then None
-    else Some (Cil.makeVarinfo false false "__retres" ty)
+    else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
   in
   let return =
     Cil.mkStmt ~valid_sid:true

src/plugins/e-acsl/env.ml

@@ -184,6 +184,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
       ~source:true
       false (* is a global? *)
       false (* is a formal? *)
+      ~referenced:true
       (Varname.get ~scope (Functions.RTL.mk_gen_name name))
       ty
   in

src/plugins/e-acsl/misc.ml

@@ -211,7 +211,7 @@ let term_addr_of ~loc tlv ty =
 let reorder_ast () =
   let ast = Ast.get() in
   let is_from_library = function
-    | GType(ti, _) when ti.tname = "size_t"
+    | GType(ti, _) when ti.tname = "size_t" || ti.tname = "FILE"
       || RTL.is_rtl_name ti.tname -> true
     | GCompTag (ci, _) when RTL.is_rtl_name ci.cname -> true
     | GFunDecl(_, _, loc) | GVarDecl(_, loc) when is_library_loc loc -> true

src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c

 /* Generated by Frama-C */
+#include "signal.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "sys/time.h"
@@ -212,6 +213,10 @@ void __e_acsl_globals_init(void)
     __e_acsl_full_init((void *)(& testno));
     __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
     __e_acsl_full_init((void *)(& __fc_time));
+    __e_acsl_store_block((void *)(& __fc_p_sigaction),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_sigaction));
+    __e_acsl_store_block((void *)(sigaction),(size_t)2080);
+    __e_acsl_full_init((void *)(& sigaction));
     __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
     __e_acsl_full_init((void *)(& __fc_p_fopen));
     __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
@@ -601,6 +606,8 @@ int main(int argc, char const **argv)
   __e_acsl_delete_block((void *)(& signal_eval));
   __e_acsl_delete_block((void *)(& testno));
   __e_acsl_delete_block((void *)(& __fc_time));
+  __e_acsl_delete_block((void *)(& __fc_p_sigaction));
+  __e_acsl_delete_block((void *)(sigaction));
   __e_acsl_delete_block((void *)(& __fc_p_fopen));
   __e_acsl_delete_block((void *)(__fc_fopen));
   __e_acsl_delete_block((void *)(& stdout));