From 5193f45424e4d4e298741950828f6e7dd222c848 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 16 Mar 2016 18:54:02 +0100
Subject: [PATCH] [RTL] Removed runction __init_argv from the API. Instead it
is called internally via __e_acsl_memory_init
---
.../e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h | 4 +++-
src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 5 -----
.../e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c | 1 -
src/plugins/e-acsl/visit.ml | 6 ------
4 files changed, 3 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
index 6e6816ad1d4..f95d39c1fa1 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+++ b/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);
}
/**********************/
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index caf3d55ee51..8fec227fc0b 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 7a93e7c7397..60e2c7f959d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/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;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 6b22631ba93..08d57de4d82 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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;
--
GitLab