[RTL] Removed runction __init_argv from the API. Instead it is called

internally via __e_acsl_memory_init

src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h

@@ -393,7 +393,7 @@ void __e_acsl_memory_clean() {
 }
 
 /* adds argc / argv to the memory model */
-void __init_argv(int argc, char **argv) {
+static void __init_argv(int argc, char **argv) {
   int i;
 
   __store_block(argv, (argc+1)*sizeof(char*));
@@ -411,6 +411,8 @@ void __init_argv(int argc, char **argv) {
  *  ptr_size the size of the pointer computed during instrumentation. */
 void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   arch_assert(ptr_size);
+  if (argc_ref)
+    __init_argv(*argc_ref, *argv_ref);
 }
 
 /**********************/

src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h

@@ -135,11 +135,6 @@ int __offset(void * ptr)
 int __initialized(void * ptr, size_t size)
   __attribute__((FC_BUILTIN));
 
-/* put argv in the memory model */
-/*@ assigns \nothing; */
-void __init_argv(int argc, char **argv)
-	__attribute__((FC_BUILTIN));
-
 /* print the content of the abstract structure */
 void __e_acsl_memory_debug(void)
   __attribute__((FC_BUILTIN));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c

@@ -4,7 +4,6 @@ int main(int argc, char **argv)
   int __retres;
   int i;
   __e_acsl_memory_init(& argc,& argv,8UL);
-  __init_argv(argc,argv);
   /*@ assert \valid(&argc); */
   {
     int __e_acsl_valid;

src/plugins/e-acsl/visit.ml

@@ -284,12 +284,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
           match main.sformals with
           | vi1 :: vi2 :: _
             when vi1.vtype = Cil.intType && vi2.vtype = charPtrPtrType ->
-              (* Add a call to __init_args if need argv for analysis *)
-              if Mmodel_analysis.must_model_vi vi2 then begin
-                let arg = [ Cil.evar vi1 ; Cil.evar vi2 ] in
-                let arginit = Misc.mk_call loc "__init_argv" arg in
-                main.sbody.bstmts <- arginit :: main.sbody.bstmts;
-              end;
               (* Grab addresses of arguments for a call to the main
               initialization function, i.e., [__e_acsl_memory_init] *)
               List.map Cil.mkAddrOfVi main.sformals;