From ee58e76705fbb8d9fde4acd531f930fa3c3119c3 Mon Sep 17 00:00:00 2001
From: Arvid Jakobsson <arvid.jakobsson@gmail.com>
Date: Wed, 16 Jul 2014 14:20:15 +0200
Subject: [PATCH] fix bug #1381, adds argc and argv to memory model when
present
also change gcc_test.sh so that one can pass arguments to program
under test.
---
src/plugins/e-acsl/gcc_test.sh | 16 +-
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 14 +
.../share/e-acsl/memory_model/e_acsl_mmodel.h | 5 +
.../e-acsl/tests/e-acsl-runtime/mainargs.i | 24 ++
.../e-acsl-runtime/oracle/gen_mainargs.c | 248 +++++++++++
.../e-acsl-runtime/oracle/gen_mainargs2.c | 402 ++++++++++++++++++
.../oracle/mainargs.1.err.oracle | 0
.../oracle/mainargs.1.res.oracle | 74 ++++
.../e-acsl-runtime/oracle/mainargs.err.oracle | 0
.../e-acsl-runtime/oracle/mainargs.res.oracle | 49 +++
src/plugins/e-acsl/visit.ml | 42 +-
11 files changed, 860 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
diff --git a/src/plugins/e-acsl/gcc_test.sh b/src/plugins/e-acsl/gcc_test.sh
index c8cfdada045..20dc759894c 100755
--- a/src/plugins/e-acsl/gcc_test.sh
+++ b/src/plugins/e-acsl/gcc_test.sh
@@ -1,8 +1,16 @@
#!/bin/sh
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+IN=$1
+if [ $# -gt 1 ]; then
+ shift;
+ BUILTIN=$1
+ shift;
+ ARGS=$@
+fi
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
-gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
+
+gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 8db9c737e84..cb1d9e85836 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -77,6 +77,20 @@ size_t needed_bytes (size_t size) {
return (size % 8) == 0 ? (size/8) : (size/8 + 1);
}
+
+/* adds argc / argv to the memory model */
+void __init_args(int argc, char **argv) {
+ int i;
+
+ __store_block(argv, (argc+1)*sizeof(char*));
+ __full_init(argv);
+
+ for (i = 0; i < argc; i++) {
+ __store_block(argv[i], strlen(argv[i])+1);
+ __full_init(argv[i]);
+ }
+}
+
/* store the block of size bytes starting at ptr */
void* __store_block(void* ptr, size_t size) {
struct _block * tmp;
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 7454e06c2c1..2480dbc0ad5 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -53,6 +53,11 @@ void * __calloc(size_t nbr_elt, size_t size_elt)
/* From outside the library, the following functions have no side effect */
+/* put argc/argv in memory model */
+/*@ assigns \nothing; */
+void __init_args(int argc_ref, char **argv_ref)
+ __attribute__((FC_BUILTIN));
+
/* store the block of size bytes starting at ptr */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
void * __store_block(void * ptr, size_t size)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i
new file mode 100644
index 00000000000..a08234b3a93
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i
@@ -0,0 +1,24 @@
+/* run.config
+ COMMENT: the contents of argv should be valid
+ EXECNOW: LOG gen_mainargs.c BIN gen_mainargs.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs.c > /dev/null && ./gcc_test.sh mainargs "" bar baz
+ EXECNOW: LOG gen_mainargs2.c BIN gen_mainargs2.out @frama-c@ -machdep x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/mainargs.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_mainargs2.c > /dev/null && ./gcc_test.sh mainargs2 "" bar baz
+*/
+
+#include <string.h>
+
+int main(int argc, char **argv) {
+ int i;
+
+ /*@ assert \valid(&argc) ; */
+ /*@ assert \valid(&argv) ; */
+ /*@ assert \forall int k; 0 <= k && k < argc ==> \valid(argv + k) ; */
+ /*@ assert \block_length(argv) == (argc+1)*sizeof(char*) ; */
+
+ /*@ assert argv[argc] == \null ; */
+ /*@ assert ! \valid(argv[argc]) ; */
+ for (i = 0; i < argc; i++) {
+ int len = strlen(argv[i]);
+ /*@ assert \valid(argv[i]) ; */
+ /*@ assert \forall int k; 0 <= k && k <= len ==> \valid(&argv[i][k]) ; */
+ }
+}
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
new file mode 100644
index 00000000000..8e31ea4ce12
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -0,0 +1,248 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __init_args(int argc_ref,
+ char **argv_ref);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+
+/*@ ensures \result ≡ \block_length(\old(ptr));
+ assigns \result;
+ assigns \result \from ptr;
+ */
+extern __attribute__((__FC_BUILTIN__)) size_t __block_length(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+/*@ ghost extern size_t __memory_size; */
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+/*@ assigns \result, *(x_0+(0 ..));
+ assigns \result \from *(x_0+(0 ..));
+ assigns *(x_0+(0 ..)) \from *(x_0+(0 ..));
+ */
+extern int ( /* missing proto */ strlen)(char *x_0);
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ int i;
+ __init_args(argc,argv);
+ /*@ assert \valid(&argc); */
+ {
+ int __e_acsl_valid;
+ __store_block((void *)(& argc),4U);
+ __store_block((void *)(& argv),8U);
+ __e_acsl_valid = __valid((void *)(& argc),(size_t)sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&argc)",12);
+ }
+ /*@ assert \valid(&argv); */
+ {
+ int __e_acsl_valid_2;
+ __e_acsl_valid_2 = __valid((void *)(& argv),(size_t)sizeof(char **));
+ e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&argv)",13);
+ }
+ /*@ assert ∀ int k; 0 ≤ k ∧ k < argc ⇒ \valid(argv+k); */
+ {
+ int __e_acsl_forall;
+ int __e_acsl_k;
+ __e_acsl_forall = 1;
+ __e_acsl_k = 0;
+ while (1) {
+ if (__e_acsl_k < argc) ; else break;
+ {
+ int __e_acsl_valid_3;
+ __e_acsl_valid_3 = __valid((void *)(argv + __e_acsl_k),
+ (size_t)sizeof(char *));
+ if (__e_acsl_valid_3) ;
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+ __e_acsl_k ++;
+ }
+ e_acsl_end_loop1: ;
+ e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall int k; 0 <= k && k < argc ==> \\valid(argv+k)",
+ 14);
+ }
+ /*@ assert \block_length(argv) ≡ (argc+1)*sizeof(char *); */
+ {
+ unsigned long __e_acsl_block_length;
+ __e_acsl_block_length = (unsigned long)__block_length((void *)argv);
+ e_acsl_assert(__e_acsl_block_length == (unsigned long)(((long)argc + (long)1) * 8L),
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(argv) == (argc+1)*sizeof(char *)",
+ 15);
+ }
+ /*@ assert *(argv+argc) ≡ \null; */
+ {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)(argv + argc),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+argc)",17);
+ e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
+ (char *)"main",(char *)"*(argv+argc) == \\null",17);
+ }
+ /*@ assert ¬\valid(*(argv+argc)); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(argv + argc),
+ (size_t)sizeof(char *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_read_2;
+ int __e_acsl_valid_4;
+ __e_acsl_valid_read_2 = __valid_read((void *)(argv + argc),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+argc)",18);
+ __e_acsl_valid_4 = __valid((void *)*(argv + argc),(size_t)sizeof(char));
+ __e_acsl_and = __e_acsl_valid_4;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(*(argv+argc))",18);
+ }
+ i = 0;
+ while (i < argc) {
+ {
+ int len;
+ len = strlen(*(argv + i));
+ /*@ assert \valid(*(argv+i)); */
+ {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and_2;
+ __e_acsl_initialized_2 = __initialized((void *)(argv + i),
+ (size_t)sizeof(char *));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read_3;
+ int __e_acsl_valid_5;
+ __e_acsl_valid_read_3 = __valid_read((void *)(argv + i),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+i)",21);
+ __e_acsl_valid_5 = __valid((void *)*(argv + i),
+ (size_t)sizeof(char));
+ __e_acsl_and_2 = __e_acsl_valid_5;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*(argv+i))",21);
+ }
+ /*@ assert ∀ int k; 0 ≤ k ∧ k ≤ len ⇒ \valid(*(argv+i)+k); */
+ {
+ int __e_acsl_forall_2;
+ long __e_acsl_k_2;
+ __e_acsl_forall_2 = 1;
+ __e_acsl_k_2 = (long)0;
+ while (1) {
+ if (__e_acsl_k_2 <= (long)len) ; else break;
+ {
+ int __e_acsl_valid_read_4;
+ int __e_acsl_valid_6;
+ __e_acsl_valid_read_4 = __valid_read((void *)(argv + i),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+i)",22);
+ __e_acsl_valid_6 = __valid((void *)(*(argv + i) + __e_acsl_k_2),
+ (size_t)sizeof(char));
+ if (__e_acsl_valid_6) ;
+ else {
+ __e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ }
+ __e_acsl_k_2 ++;
+ }
+ e_acsl_end_loop2: ;
+ e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall int k; 0 <= k && k <= len ==> \\valid(*(argv+i)+k)",
+ 22);
+ }
+ }
+ i ++;
+ }
+ __retres = 0;
+ __delete_block((void *)(& argc));
+ __delete_block((void *)(& argv));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
new file mode 100644
index 00000000000..00f3f226a99
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
@@ -0,0 +1,402 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from __e_acsl_init;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
+ unsigned long n);
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(z_orig);
+ requires \valid(z);
+ assigns *z;
+ assigns *z \from *z_orig;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
+ __mpz_struct const * /*[1]*/ z_orig);
+
+/*@ requires \valid(x);
+ assigns *x;
+ assigns *x \from *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \result;
+ assigns \result \from *z1, *z2;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+ assigns *z1 \from *z2, *z3;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+ assigns *z1 \from *z2, *z3;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+
+/*@ requires \valid(z);
+ assigns \result;
+ assigns \result \from *z; */
+extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __init_args(int argc_ref,
+ char **argv_ref);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+
+/*@ ensures \result ≡ \block_length(\old(ptr));
+ assigns \result;
+ assigns \result \from ptr;
+ */
+extern __attribute__((__FC_BUILTIN__)) size_t __block_length(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+/*@ ghost extern size_t __memory_size; */
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+/*@ assigns \result, *(x_0+(0 ..));
+ assigns \result \from *(x_0+(0 ..));
+ assigns *(x_0+(0 ..)) \from *(x_0+(0 ..));
+ */
+extern int ( /* missing proto */ strlen)(char *x_0);
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ int i;
+ __init_args(argc,argv);
+ /*@ assert \valid(&argc); */
+ {
+ int __e_acsl_valid;
+ __store_block((void *)(& argc),4U);
+ __store_block((void *)(& argv),8U);
+ __e_acsl_valid = __valid((void *)(& argc),(size_t)sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&argc)",12);
+ }
+ /*@ assert \valid(&argv); */
+ {
+ int __e_acsl_valid_2;
+ __e_acsl_valid_2 = __valid((void *)(& argv),(size_t)sizeof(char **));
+ e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&argv)",13);
+ }
+ /*@ assert ∀ int k; 0 ≤ k ∧ k < argc ⇒ \valid(argv+k); */
+ {
+ int __e_acsl_forall;
+ mpz_t __e_acsl_k;
+ __e_acsl_forall = 1;
+ __gmpz_init(__e_acsl_k);
+ {
+ mpz_t __e_acsl;
+ __gmpz_init_set_si(__e_acsl,(long)0);
+ __gmpz_set(__e_acsl_k,(__mpz_struct const *)(__e_acsl));
+ __gmpz_clear(__e_acsl);
+ }
+ while (1) {
+ {
+ mpz_t __e_acsl_argc;
+ int __e_acsl_lt;
+ __gmpz_init_set_si(__e_acsl_argc,(long)argc);
+ __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_k),
+ (__mpz_struct const *)(__e_acsl_argc));
+ if (__e_acsl_lt < 0) ; else break;
+ __gmpz_clear(__e_acsl_argc);
+ }
+ {
+ unsigned long __e_acsl_k_2;
+ int __e_acsl_valid_3;
+ __e_acsl_k_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_k));
+ __e_acsl_valid_3 = __valid((void *)(argv + __e_acsl_k_2),
+ (size_t)sizeof(char *));
+ if (__e_acsl_valid_3) ;
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+ {
+ mpz_t __e_acsl_2;
+ mpz_t __e_acsl_add;
+ __gmpz_init_set_si(__e_acsl_2,1L);
+ __gmpz_init(__e_acsl_add);
+ __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_k),
+ (__mpz_struct const *)(__e_acsl_2));
+ __gmpz_set(__e_acsl_k,(__mpz_struct const *)(__e_acsl_add));
+ __gmpz_clear(__e_acsl_2);
+ __gmpz_clear(__e_acsl_add);
+ }
+ }
+ e_acsl_end_loop1: ;
+ e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall int k; 0 <= k && k < argc ==> \\valid(argv+k)",
+ 14);
+ __gmpz_clear(__e_acsl_k);
+ }
+ /*@ assert \block_length(argv) ≡ (argc+1)*sizeof(char *); */
+ {
+ unsigned long __e_acsl_block_length;
+ mpz_t __e_acsl_block_length_2;
+ mpz_t __e_acsl_argc_2;
+ mpz_t __e_acsl_3;
+ mpz_t __e_acsl_add_2;
+ mpz_t __e_acsl_sizeof;
+ mpz_t __e_acsl_mul;
+ int __e_acsl_eq;
+ __e_acsl_block_length = (unsigned long)__block_length((void *)argv);
+ __gmpz_init_set_ui(__e_acsl_block_length_2,__e_acsl_block_length);
+ __gmpz_init_set_si(__e_acsl_argc_2,(long)argc);
+ __gmpz_init_set_si(__e_acsl_3,(long)1);
+ __gmpz_init(__e_acsl_add_2);
+ __gmpz_add(__e_acsl_add_2,(__mpz_struct const *)(__e_acsl_argc_2),
+ (__mpz_struct const *)(__e_acsl_3));
+ __gmpz_init_set_si(__e_acsl_sizeof,8L);
+ __gmpz_init(__e_acsl_mul);
+ __gmpz_mul(__e_acsl_mul,(__mpz_struct const *)(__e_acsl_add_2),
+ (__mpz_struct const *)(__e_acsl_sizeof));
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_2),
+ (__mpz_struct const *)(__e_acsl_mul));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(argv) == (argc+1)*sizeof(char *)",
+ 15);
+ __gmpz_clear(__e_acsl_block_length_2);
+ __gmpz_clear(__e_acsl_argc_2);
+ __gmpz_clear(__e_acsl_3);
+ __gmpz_clear(__e_acsl_add_2);
+ __gmpz_clear(__e_acsl_sizeof);
+ __gmpz_clear(__e_acsl_mul);
+ }
+ /*@ assert *(argv+argc) ≡ \null; */
+ {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)(argv + (long)argc),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+(long)argc)",17);
+ e_acsl_assert(*(argv + (long)argc) == (void *)0,(char *)"Assertion",
+ (char *)"main",(char *)"*(argv+argc) == \\null",17);
+ }
+ /*@ assert ¬\valid(*(argv+argc)); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(argv + (long)argc),
+ (size_t)sizeof(char *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_read_2;
+ int __e_acsl_valid_4;
+ __e_acsl_valid_read_2 = __valid_read((void *)(argv + (long)argc),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+(long)argc)",18);
+ __e_acsl_valid_4 = __valid((void *)*(argv + (long)argc),
+ (size_t)sizeof(char));
+ __e_acsl_and = __e_acsl_valid_4;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(*(argv+argc))",18);
+ }
+ i = 0;
+ while (i < argc) {
+ {
+ int len;
+ len = strlen(*(argv + i));
+ /*@ assert \valid(*(argv+i)); */
+ {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and_2;
+ __e_acsl_initialized_2 = __initialized((void *)(argv + (long)i),
+ (size_t)sizeof(char *));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read_3;
+ int __e_acsl_valid_5;
+ __e_acsl_valid_read_3 = __valid_read((void *)(argv + (long)i),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+(long)i)",21);
+ __e_acsl_valid_5 = __valid((void *)*(argv + (long)i),
+ (size_t)sizeof(char));
+ __e_acsl_and_2 = __e_acsl_valid_5;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(*(argv+i))",21);
+ }
+ /*@ assert ∀ int k; 0 ≤ k ∧ k ≤ len ⇒ \valid(*(argv+i)+k); */
+ {
+ int __e_acsl_forall_2;
+ mpz_t __e_acsl_k_3;
+ __e_acsl_forall_2 = 1;
+ __gmpz_init(__e_acsl_k_3);
+ {
+ mpz_t __e_acsl_4;
+ __gmpz_init_set_si(__e_acsl_4,(long)0);
+ __gmpz_set(__e_acsl_k_3,(__mpz_struct const *)(__e_acsl_4));
+ __gmpz_clear(__e_acsl_4);
+ }
+ while (1) {
+ {
+ mpz_t __e_acsl_len;
+ int __e_acsl_le;
+ __gmpz_init_set_si(__e_acsl_len,(long)len);
+ __e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__e_acsl_k_3),
+ (__mpz_struct const *)(__e_acsl_len));
+ if (__e_acsl_le <= 0) ; else break;
+ __gmpz_clear(__e_acsl_len);
+ }
+ {
+ unsigned long __e_acsl_k_4;
+ int __e_acsl_valid_read_4;
+ int __e_acsl_valid_6;
+ __e_acsl_k_4 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_k_3));
+ __e_acsl_valid_read_4 = __valid_read((void *)(argv + (long)i),
+ (size_t)sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
+ (char *)"mem_access: \\valid_read(argv+(long)i)",
+ 22);
+ __e_acsl_valid_6 = __valid((void *)(*(argv + (long)i) + __e_acsl_k_4),
+ (size_t)sizeof(char));
+ if (__e_acsl_valid_6) ;
+ else {
+ __e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ }
+ {
+ mpz_t __e_acsl_5;
+ mpz_t __e_acsl_add_3;
+ __gmpz_init_set_si(__e_acsl_5,1L);
+ __gmpz_init(__e_acsl_add_3);
+ __gmpz_add(__e_acsl_add_3,(__mpz_struct const *)(__e_acsl_k_3),
+ (__mpz_struct const *)(__e_acsl_5));
+ __gmpz_set(__e_acsl_k_3,(__mpz_struct const *)(__e_acsl_add_3));
+ __gmpz_clear(__e_acsl_5);
+ __gmpz_clear(__e_acsl_add_3);
+ }
+ }
+ e_acsl_end_loop2: ;
+ e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall int k; 0 <= k && k <= len ==> \\valid(*(argv+i)+k)",
+ 22);
+ __gmpz_clear(__e_acsl_k_3);
+ }
+ }
+ i ++;
+ }
+ __retres = 0;
+ __delete_block((void *)(& argc));
+ __delete_block((void *)(& argv));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
new file mode 100644
index 00000000000..10628751ac5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -0,0 +1,74 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Calling undeclared function strlen. Old style K&R code?
+[e-acsl] beginning translation.
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specification for function strlen, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __init_args
+tests/e-acsl-runtime/mainargs.i:12:[value] Assertion got status valid.
+[value] using specification for function __store_block
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/mainargs.i:13:[value] Assertion got status valid.
+tests/e-acsl-runtime/mainargs.i:14:[value] Assertion got status unknown.
+[value] using specification for function __gmpz_init
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
+[value] using specification for function __gmpz_init_set_si
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
+[value] using specification for function __gmpz_set
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
+[value] using specification for function __gmpz_clear
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
+tests/e-acsl-runtime/mainargs.i:14:[value] entering loop for the first time
+[value] using specification for function __gmpz_cmp
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function __gmpz_get_ui
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
+[value] using specification for function __gmpz_add
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
+tests/e-acsl-runtime/mainargs.i:15:[value] Assertion got status unknown.
+[value] using specification for function __block_length
+[value] using specification for function __gmpz_init_set_ui
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
+[value] using specification for function __gmpz_mul
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
+tests/e-acsl-runtime/mainargs.i:17:[value] Assertion got status unknown.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/mainargs.i:17:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
+tests/e-acsl-runtime/mainargs.i:18:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+tests/e-acsl-runtime/mainargs.i:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
+tests/e-acsl-runtime/mainargs.i:19:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+[value] using specification for function strlen
+tests/e-acsl-runtime/mainargs.i:21:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.i:21:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
+tests/e-acsl-runtime/mainargs.i:22:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.i:22:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.i:22:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
+tests/e-acsl-runtime/mainargs.i:19:[kernel] warning: signed overflow. assert i+1 ≤ 2147483647;
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
new file mode 100644
index 00000000000..0919a446346
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -0,0 +1,49 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Calling undeclared function strlen. Old style K&R code?
+[e-acsl] beginning translation.
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specification for function strlen, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __init_args
+tests/e-acsl-runtime/mainargs.i:12:[value] Assertion got status valid.
+[value] using specification for function __store_block
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/mainargs.i:13:[value] Assertion got status valid.
+tests/e-acsl-runtime/mainargs.i:14:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.i:14:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.i:15:[value] Assertion got status unknown.
+[value] using specification for function __block_length
+tests/e-acsl-runtime/mainargs.i:17:[value] Assertion got status unknown.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/mainargs.i:17:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.i:18:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+tests/e-acsl-runtime/mainargs.i:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.i:19:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+[value] using specification for function strlen
+tests/e-acsl-runtime/mainargs.i:21:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.i:21:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+tests/e-acsl-runtime/mainargs.i:22:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.i:22:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.i:22:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 5af377d2bf8..850e9faf10f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -196,18 +196,40 @@ class e_acsl_visitor prj generate = object (self)
[ cil_fct; GFun(main, Location.unknown) ]
in
f.globals <- new_globals
- | None ->
+ | None ->
Kernel.warning "@[no entry point specified:@ \
you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
- fname;
- f.globals <- f.globals @ [ cil_fct ]
- in
- Project.on prj build_initializer ()
- end;
- (* reset copied states at the end to be observationally equivalent to a
- standard visitor. *)
- if generate then Project.clear ~selection ~project:prj ();
- f)
+ fname;
+ f.globals <- f.globals @ [ cil_fct ]
+ in
+ Project.on prj build_initializer ()
+ end;
+
+ (* init memory store, and then add program arguments if there
+ are any. must be called before global variables are
+ initialized. *)
+ if Pre_analysis.use_model () then begin
+ match main_fct with
+ | Some main ->
+ let charPtrPtrType = TPtr(Cil.charPtrType,[]) in
+ let loc = Location.unknown in
+ (* this might not be valid in an embedded environment,
+ where int/char** arguments is not necessarily valid *)
+ let stmts_pre = match main.sformals with
+ | { vtype = t1 }::{ vtype = t2 }::_ when
+ t1 = Cil.intType && t2 = charPtrPtrType ->
+ let args = (List.map Cil.evar main.sformals) in
+ [(Misc.mk_call loc "__init_args" args)]
+ | _ -> []
+ in
+ main.sbody.bstmts <- stmts_pre @ main.sbody.bstmts;
+ | None -> ()
+ end;
+
+ (* reset copied states at the end to be observationally equivalent to a
+ standard visitor. *)
+ if generate then Project.clear ~selection ~project:prj ();
+ f)
method !vglob_aux = function
| GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
--
GitLab