diff --git a/src/plugins/e-acsl/gcc_test.sh b/src/plugins/e-acsl/gcc_test.sh
index c8cfdada04523213e1008b6ad7c94e3596019c58..20dc759894c03f5ae9b2434c016b07c9d6c09fc7 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 8db9c737e840388279e08131c6a3c854d8dc2ff9..cb1d9e85836e60ef9322c8fee3868475cc8b879d 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 1910afc7b8a96888d46a5e019e14f96d374dd0e2..d5f29902700bcba7d888c70d8a45b13aed5246d2 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.c b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
new file mode 100644
index 0000000000000000000000000000000000000000..3a4801a487cc7fba78f9fa718a888b79217f02d9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
@@ -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.c -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.c -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 0000000000000000000000000000000000000000..b741ebe03b2ecdfe3cfe29da6ccfca233aa931b5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -0,0 +1,594 @@
+/* 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;
+typedef int wchar_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;
+ */
+/*@
+axiomatic
+ MemCmp {
+ logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
+
+ reads *(s1+(0 .. n-1)), *(s2+(0 .. n-1));
+
+ axiom
+ memcmp_zero{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ⇔
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@
+axiomatic
+ MemChr {
+ logic 𔹠memchr{L}(char *s, ℤ c, ℤ n) ;
+
+ axiom
+ memchr_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ (∀ ℤ n;
+ memchr{L}(s, c, n) ≡ \true ⇔
+ (∃ int i; (0 ≤ i ∧ i < n) ∧ *(s+i) ≡ c)));
+
+ }
+ */
+/*@
+axiomatic
+ MemSet {
+ logic 𔹠memset{L}(char *s, ℤ c, ℤ n) ;
+
+ axiom
+ memset_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ (∀ ℤ n;
+ memset{L}(s, c, n) ≡ \true ⇔
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s+i) ≡ c)));
+
+ }
+ */
+/*@
+axiomatic
+ StrLen {
+ logic ℤ strlen{L}(char *s) ;
+
+ axiom
+ strlen_pos_or_null{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧
+ (∀ ℤ j;
+ 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ '\000'))
+ ∧ *(s+i) ≡ '\000' ⇒ strlen{L}(s) ≡ i);
+
+ axiom
+ strlen_neg{L}:
+ ∀ char *s;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ '\000') ⇒
+ strlen{L}(s) < 0;
+
+ axiom
+ strlen_before_null{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ i < strlen{L}(s) ⇒
+ *(s+i) ≢ '\000');
+
+ axiom
+ strlen_at_null{L}:
+ ∀ char *s;
+ 0 ≤ strlen{L}(s) ⇒ *(s+strlen{L}(s)) ≡ '\000';
+
+ axiom
+ strlen_not_zero{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧
+ *(s+i) ≢ '\000' ⇒ i < strlen{L}(s));
+
+ axiom
+ strlen_zero{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ '\000'
+ ⇒ i ≡ strlen{L}(s));
+
+ axiom
+ strlen_sup{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
+ 0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
+
+ axiom
+ strlen_shift{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ strlen{L}(s) ⇒
+ strlen{L}(s+i) ≡ strlen{L}(s)-i);
+
+ axiom
+ strlen_create{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
+ 0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
+
+ axiom
+ strlen_create_shift{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (∀ ℤ k;
+ (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ '\000'
+ ⇒
+ 0 ≤ strlen{L}(s+k) ∧
+ strlen{L}(s+k) ≤ i-k));
+
+ axiom
+ memcmp_strlen_left{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ∧ strlen{L}(s1) < n
+ ⇒ strlen{L}(s1) ≡ strlen{L}(s2));
+
+ axiom
+ memcmp_strlen_right{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ∧
+ strlen{L}(s2) < n ⇒
+ strlen{L}(s1) ≡ strlen{L}(s2));
+
+ axiom
+ memcmp_strlen_shift_left{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ k, ℤ n;
+ (memcmp{L}(s1, s2+k, n) ≡ 0 ∧ 0 ≤ k)
+ ∧ strlen{L}(s1) < n ⇒
+ 0 ≤ strlen{L}(s2) ∧
+ strlen{L}(s2) ≤ k+strlen{L}(s1));
+
+ axiom
+ memcmp_strlen_shift_right{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ k, ℤ n;
+ (memcmp{L}(s1+k, s2, n) ≡ 0 ∧ 0 ≤ k)
+ ∧ strlen{L}(s2) < n ⇒
+ 0 ≤ strlen{L}(s1) ∧
+ strlen{L}(s1) ≤ k+strlen{L}(s2));
+
+ }
+ */
+/*@
+axiomatic
+ StrCmp {
+ logic ℤ strcmp{L}(char *s1, char *s2) ;
+
+ axiom
+ strcmp_zero{L}:
+ ∀ char *s1, char *s2;
+ strcmp{L}(s1, s2) ≡ 0 ⇔
+ strlen{L}(s1) ≡ strlen{L}(s2) ∧
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ strlen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
+
+ }
+ */
+/*@
+axiomatic
+ StrNCmp {
+ logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) ;
+
+ axiom
+ strncmp_zero{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ strncmp{L}(s1, s2, n) ≡ 0 ⇔
+ (strlen{L}(s1) < n ∧ strcmp{L}(s1, s2) ≡ 0) ∨
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@
+axiomatic
+ StrChr {
+ logic 𔹠strchr{L}(char *s, ℤ c) ;
+
+ axiom
+ strchr_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ strchr{L}(s, c) ≡ \true ⇔
+ (∃ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ c));
+
+ }
+ */
+/*@
+axiomatic
+ WcsLen {
+ logic ℤ wcslen{L}(wchar_t *s) ;
+
+ axiom
+ wcslen_pos_or_null{L}:
+ ∀ wchar_t *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧
+ (∀ ℤ j; 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ 0))
+ ∧ *(s+i) ≡ 0 ⇒ wcslen{L}(s) ≡ i);
+
+ axiom
+ wcslen_neg{L}:
+ ∀ wchar_t *s;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ 0) ⇒ wcslen{L}(s) < 0;
+
+ axiom
+ wcslen_before_null{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ i < wcslen{L}(s) ⇒ *(s+i) ≢ 0);
+
+ axiom
+ wcslen_at_null{L}:
+ ∀ wchar_t *s;
+ 0 ≤ wcslen{L}(s) ⇒ *(s+wcslen{L}(s)) ≡ 0;
+
+ axiom
+ wcslen_not_zero{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≢ 0
+ ⇒ i < wcslen{L}(s));
+
+ axiom
+ wcslen_zero{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≡ 0 ⇒
+ i ≡ wcslen{L}(s));
+
+ axiom
+ wcslen_sup{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
+
+ axiom
+ wcslen_shift{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ i ≤ wcslen{L}(s) ⇒
+ wcslen{L}(s+i) ≡ wcslen{L}(s)-i);
+
+ axiom
+ wcslen_create{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
+
+ axiom
+ wcslen_create_shift{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (∀ int k;
+ (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s+k) ∧
+ wcslen{L}(s+k) ≤ i-k));
+
+ }
+ */
+/*@
+axiomatic
+ WcsCmp {
+ logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) ;
+
+ axiom
+ wcscmp_zero{L}:
+ ∀ wchar_t *s1, wchar_t *s2;
+ wcscmp{L}(s1, s2) ≡ 0 ⇔
+ wcslen{L}(s1) ≡ wcslen{L}(s2) ∧
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ wcslen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
+
+ }
+ */
+/*@
+axiomatic
+ WcsNCmp {
+ logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) ;
+
+ axiom
+ wcsncmp_zero{L}:
+ ∀ wchar_t *s1, wchar_t *s2;
+ (∀ ℤ n;
+ wcsncmp{L}(s1, s2, n) ≡ 0 ⇔
+ (wcslen{L}(s1) < n ∧ wcscmp{L}(s1, s2) ≡ 0) ∨
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@ logic ℤ minimum(ℤ i, ℤ j) = i<j? i: j;
+ */
+/*@ logic ℤ maximum(ℤ i, ℤ j) = i<j? j: i;
+ */
+/*@
+predicate valid_string{L}(char *s) =
+ 0 ≤ strlen{L}(s) ∧ \valid{L}(s+(0 .. strlen{L}(s)));
+ */
+/*@
+predicate valid_string_or_null{L}(char *s) =
+ s ≡ \null ∨ valid_string{L}(s);
+ */
+/*@
+predicate valid_wstring{L}(wchar_t *s) =
+ 0 ≤ wcslen{L}(s) ∧ \valid{L}(s+(0 .. wcslen{L}(s)));
+ */
+/*@
+predicate valid_wstring_or_null{L}(wchar_t *s) =
+ s ≡ \null ∨ valid_wstring{L}(s);
+ */
+/*@ requires valid_string_src: valid_string(s);
+ ensures \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s+(0 ..));
+ */
+extern size_t strlen(char const *s);
+
+/*@ requires valid_string_src: valid_string(s);
+ ensures \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s+(0 ..));
+ */
+size_t __e_acsl_strlen(char const *s)
+{
+ size_t __retres;
+ __store_block((void *)(& s),8U);
+ __retres = strlen(s);
+ __delete_block((void *)(& s));
+ return __retres;
+}
+
+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;
+ size_t tmp;
+ tmp = __e_acsl_strlen((char const *)*(argv + i));
+ len = (int)tmp;
+ /*@ 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 0000000000000000000000000000000000000000..cf644234f2a23491775ec663d077c6419fa887ec
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
@@ -0,0 +1,748 @@
+/* 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;
+typedef int wchar_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;
+ */
+/*@
+axiomatic
+ MemCmp {
+ logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
+
+ reads *(s1+(0 .. n-1)), *(s2+(0 .. n-1));
+
+ axiom
+ memcmp_zero{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ⇔
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@
+axiomatic
+ MemChr {
+ logic 𔹠memchr{L}(char *s, ℤ c, ℤ n) ;
+
+ axiom
+ memchr_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ (∀ ℤ n;
+ memchr{L}(s, c, n) ≡ \true ⇔
+ (∃ int i; (0 ≤ i ∧ i < n) ∧ *(s+i) ≡ c)));
+
+ }
+ */
+/*@
+axiomatic
+ MemSet {
+ logic 𔹠memset{L}(char *s, ℤ c, ℤ n) ;
+
+ axiom
+ memset_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ (∀ ℤ n;
+ memset{L}(s, c, n) ≡ \true ⇔
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s+i) ≡ c)));
+
+ }
+ */
+/*@
+axiomatic
+ StrLen {
+ logic ℤ strlen{L}(char *s) ;
+
+ axiom
+ strlen_pos_or_null{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧
+ (∀ ℤ j;
+ 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ '\000'))
+ ∧ *(s+i) ≡ '\000' ⇒ strlen{L}(s) ≡ i);
+
+ axiom
+ strlen_neg{L}:
+ ∀ char *s;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ '\000') ⇒
+ strlen{L}(s) < 0;
+
+ axiom
+ strlen_before_null{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ i < strlen{L}(s) ⇒
+ *(s+i) ≢ '\000');
+
+ axiom
+ strlen_at_null{L}:
+ ∀ char *s;
+ 0 ≤ strlen{L}(s) ⇒ *(s+strlen{L}(s)) ≡ '\000';
+
+ axiom
+ strlen_not_zero{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧
+ *(s+i) ≢ '\000' ⇒ i < strlen{L}(s));
+
+ axiom
+ strlen_zero{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ '\000'
+ ⇒ i ≡ strlen{L}(s));
+
+ axiom
+ strlen_sup{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
+ 0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
+
+ axiom
+ strlen_shift{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ strlen{L}(s) ⇒
+ strlen{L}(s+i) ≡ strlen{L}(s)-i);
+
+ axiom
+ strlen_create{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ 0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
+ 0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
+
+ axiom
+ strlen_create_shift{L}:
+ ∀ char *s;
+ (∀ ℤ i;
+ (∀ ℤ k;
+ (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ '\000'
+ ⇒
+ 0 ≤ strlen{L}(s+k) ∧
+ strlen{L}(s+k) ≤ i-k));
+
+ axiom
+ memcmp_strlen_left{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ∧ strlen{L}(s1) < n
+ ⇒ strlen{L}(s1) ≡ strlen{L}(s2));
+
+ axiom
+ memcmp_strlen_right{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ memcmp{L}(s1, s2, n) ≡ 0 ∧
+ strlen{L}(s2) < n ⇒
+ strlen{L}(s1) ≡ strlen{L}(s2));
+
+ axiom
+ memcmp_strlen_shift_left{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ k, ℤ n;
+ (memcmp{L}(s1, s2+k, n) ≡ 0 ∧ 0 ≤ k)
+ ∧ strlen{L}(s1) < n ⇒
+ 0 ≤ strlen{L}(s2) ∧
+ strlen{L}(s2) ≤ k+strlen{L}(s1));
+
+ axiom
+ memcmp_strlen_shift_right{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ k, ℤ n;
+ (memcmp{L}(s1+k, s2, n) ≡ 0 ∧ 0 ≤ k)
+ ∧ strlen{L}(s2) < n ⇒
+ 0 ≤ strlen{L}(s1) ∧
+ strlen{L}(s1) ≤ k+strlen{L}(s2));
+
+ }
+ */
+/*@
+axiomatic
+ StrCmp {
+ logic ℤ strcmp{L}(char *s1, char *s2) ;
+
+ axiom
+ strcmp_zero{L}:
+ ∀ char *s1, char *s2;
+ strcmp{L}(s1, s2) ≡ 0 ⇔
+ strlen{L}(s1) ≡ strlen{L}(s2) ∧
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ strlen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
+
+ }
+ */
+/*@
+axiomatic
+ StrNCmp {
+ logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) ;
+
+ axiom
+ strncmp_zero{L}:
+ ∀ char *s1, char *s2;
+ (∀ ℤ n;
+ strncmp{L}(s1, s2, n) ≡ 0 ⇔
+ (strlen{L}(s1) < n ∧ strcmp{L}(s1, s2) ≡ 0) ∨
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@
+axiomatic
+ StrChr {
+ logic 𔹠strchr{L}(char *s, ℤ c) ;
+
+ axiom
+ strchr_def{L}:
+ ∀ char *s;
+ (∀ ℤ c;
+ strchr{L}(s, c) ≡ \true ⇔
+ (∃ ℤ i;
+ (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ c));
+
+ }
+ */
+/*@
+axiomatic
+ WcsLen {
+ logic ℤ wcslen{L}(wchar_t *s) ;
+
+ axiom
+ wcslen_pos_or_null{L}:
+ ∀ wchar_t *s;
+ (∀ ℤ i;
+ (0 ≤ i ∧
+ (∀ ℤ j; 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ 0))
+ ∧ *(s+i) ≡ 0 ⇒ wcslen{L}(s) ≡ i);
+
+ axiom
+ wcslen_neg{L}:
+ ∀ wchar_t *s;
+ (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ 0) ⇒ wcslen{L}(s) < 0;
+
+ axiom
+ wcslen_before_null{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ i < wcslen{L}(s) ⇒ *(s+i) ≢ 0);
+
+ axiom
+ wcslen_at_null{L}:
+ ∀ wchar_t *s;
+ 0 ≤ wcslen{L}(s) ⇒ *(s+wcslen{L}(s)) ≡ 0;
+
+ axiom
+ wcslen_not_zero{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≢ 0
+ ⇒ i < wcslen{L}(s));
+
+ axiom
+ wcslen_zero{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≡ 0 ⇒
+ i ≡ wcslen{L}(s));
+
+ axiom
+ wcslen_sup{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
+
+ axiom
+ wcslen_shift{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ i ≤ wcslen{L}(s) ⇒
+ wcslen{L}(s+i) ≡ wcslen{L}(s)-i);
+
+ axiom
+ wcslen_create{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ 0 ≤ i ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
+
+ axiom
+ wcslen_create_shift{L}:
+ ∀ wchar_t *s;
+ (∀ int i;
+ (∀ int k;
+ (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ 0 ⇒
+ 0 ≤ wcslen{L}(s+k) ∧
+ wcslen{L}(s+k) ≤ i-k));
+
+ }
+ */
+/*@
+axiomatic
+ WcsCmp {
+ logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) ;
+
+ axiom
+ wcscmp_zero{L}:
+ ∀ wchar_t *s1, wchar_t *s2;
+ wcscmp{L}(s1, s2) ≡ 0 ⇔
+ wcslen{L}(s1) ≡ wcslen{L}(s2) ∧
+ (∀ ℤ i;
+ 0 ≤ i ∧ i ≤ wcslen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
+
+ }
+ */
+/*@
+axiomatic
+ WcsNCmp {
+ logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) ;
+
+ axiom
+ wcsncmp_zero{L}:
+ ∀ wchar_t *s1, wchar_t *s2;
+ (∀ ℤ n;
+ wcsncmp{L}(s1, s2, n) ≡ 0 ⇔
+ (wcslen{L}(s1) < n ∧ wcscmp{L}(s1, s2) ≡ 0) ∨
+ (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
+
+ }
+ */
+/*@ logic ℤ minimum(ℤ i, ℤ j) = i<j? i: j;
+ */
+/*@ logic ℤ maximum(ℤ i, ℤ j) = i<j? j: i;
+ */
+/*@
+predicate valid_string{L}(char *s) =
+ 0 ≤ strlen{L}(s) ∧ \valid{L}(s+(0 .. strlen{L}(s)));
+ */
+/*@
+predicate valid_string_or_null{L}(char *s) =
+ s ≡ \null ∨ valid_string{L}(s);
+ */
+/*@
+predicate valid_wstring{L}(wchar_t *s) =
+ 0 ≤ wcslen{L}(s) ∧ \valid{L}(s+(0 .. wcslen{L}(s)));
+ */
+/*@
+predicate valid_wstring_or_null{L}(wchar_t *s) =
+ s ≡ \null ∨ valid_wstring{L}(s);
+ */
+/*@ requires valid_string_src: valid_string(s);
+ ensures \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s+(0 ..));
+ */
+extern size_t strlen(char const *s);
+
+/*@ requires valid_string_src: valid_string(s);
+ ensures \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from *(s+(0 ..));
+ */
+size_t __e_acsl_strlen(char const *s)
+{
+ size_t __retres;
+ __store_block((void *)(& s),8U);
+ __retres = strlen(s);
+ __delete_block((void *)(& s));
+ return __retres;
+}
+
+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;
+ size_t tmp;
+ tmp = __e_acsl_strlen((char const *)*(argv + i));
+ len = (int)tmp;
+ /*@ 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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 0000000000000000000000000000000000000000..f282ee12097085436100411f7779ab08697c82df
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -0,0 +1,86 @@
+[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"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/mainargs.c"
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `strlen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
+ Ignoring annotation.
+[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.c: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.c:13:[value] Assertion got status valid.
+tests/e-acsl-runtime/mainargs.c: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.c: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.c: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.c:17:[value] Assertion got status unknown.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
+tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
+tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+FRAMAC_SHARE/libc/string.h:86:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+[value] using specification for function strlen
+FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: postcondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
+tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.c:22:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
+tests/e-acsl-runtime/mainargs.c:19:[kernel] warning: signed overflow. assert i+1 ≤ 2147483647;
+[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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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 0000000000000000000000000000000000000000..ba601298f45c187d0b8d4d207828d313040a72b3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -0,0 +1,61 @@
+[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"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/mainargs.c"
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `strlen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/string.h:86:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/string.h:86:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
+ Ignoring annotation.
+[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.c: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.c:13:[value] Assertion got status valid.
+tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.c:15:[value] Assertion got status unknown.
+[value] using specification for function __block_length
+tests/e-acsl-runtime/mainargs.c:17:[value] Assertion got status unknown.
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+FRAMAC_SHARE/libc/string.h:86:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+[value] using specification for function strlen
+FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: postcondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
+tests/e-acsl-runtime/mainargs.c:22:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+[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 a7dd86cb6c08b2b3a47e05c2518f47ab434b6dae..12755400d94b8a4e1494714674674a390b4679e0 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -110,7 +110,7 @@ class e_acsl_visitor prj generate = object (self)
with Exit ->
true
in
- if must_init then
+ if must_init then begin
let build_initializer () =
Options.feedback ~dkey ~level:2 "building global initializer.";
let return =
@@ -196,18 +196,44 @@ 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;
+ 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)
+ end; (* must_init *)
+ let must_init_args = match main_fct with
+ | Some main ->
+ let charPtrPtrType = TPtr(Cil.charPtrType,[]) in
+ (* this might not be valid in an embedded environment,
+ where int/char** arguments is not necessarily
+ valid *)
+ (match main.sformals with
+ | vi1::vi2::_ when
+ vi1.vtype = Cil.intType && vi2.vtype = charPtrPtrType
+ && Pre_analysis.must_model_vi vi2 -> true
+ | _ -> false)
+ | None -> false
+ in
+ if must_init_args then begin
+ (* init memory store, and then add program arguments if
+ there are any. must be called before global variables
+ are initialized. *)
+ let build_args_initializer () =
+ let main = Extlib.the main_fct in
+ let loc = Location.unknown in
+ let args = (List.map Cil.evar main.sformals) in
+ let call = Misc.mk_call loc "__init_args" args in
+ main.sbody.bstmts <- call :: main.sbody.bstmts;
+ in Project.on prj build_args_initializer ();
+ end;
+ (* reset copied states at the end to be observationally
+ equivalent to a standard visitor. *)
+ Project.clear ~selection ~project:prj ();
+ end; (* generate *)
+ f)
method !vglob_aux = function
| GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)