diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
similarity index 88%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i
rename to src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
index a08234b3a939269036ceff11b76b3dd9b6a1a5e7..3a4801a487cc7fba78f9fa718a888b79217f02d9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
@@ -1,7 +1,7 @@
/* 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
+ 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>
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 8e31ea4ce12678e42d0902ebbcd644cb67af9abf..b741ebe03b2ecdfe3cfe29da6ccfca233aa931b5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 {
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,
@@ -88,11 +89,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
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 ..));
+/*@
+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));
+
+ }
*/
-extern int ( /* missing proto */ strlen)(char *x_0);
+/*@
+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)
{
@@ -183,7 +527,9 @@ int main(int argc, char **argv)
while (i < argc) {
{
int len;
- len = strlen(*(argv + i));
+ size_t tmp;
+ tmp = __e_acsl_strlen((char const *)*(argv + i));
+ len = (int)tmp;
/*@ assert \valid(*(argv+i)); */
{
int __e_acsl_initialized_2;
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
index 00f3f226a99f39b19d95cb6c8c87617bdf6148a1..cf644234f2a23491775ec663d077c6419fa887ec 100644
--- 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
@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 {
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,
@@ -162,11 +163,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
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 ..));
+/*@
+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));
+
+ }
*/
-extern int ( /* missing proto */ strlen)(char *x_0);
+/*@
+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)
{
@@ -309,7 +653,9 @@ int main(int argc, char **argv)
while (i < argc) {
{
int len;
- len = strlen(*(argv + i));
+ size_t tmp;
+ tmp = __e_acsl_strlen((char const *)*(argv + i));
+ len = (int)tmp;
/*@ assert \valid(*(argv+i)); */
{
int __e_acsl_initialized_2;
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
index 10628751ac5fcd5aaadd420ec007bc403fa627fc..f282ee12097085436100411f7779ab08697c82df 100644
--- 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
@@ -4,9 +4,17 @@
[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?
+[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.
-tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specification for function strlen, generating default assigns from the prototype
+[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
@@ -19,13 +27,13 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat
__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.
+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.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/mainargs.i:14:[value] Assertion 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
@@ -35,7 +43,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
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
+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.
@@ -45,7 +53,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
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.
+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.
@@ -53,22 +61,26 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precond
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.
+tests/e-acsl-runtime/mainargs.c: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.
+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.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);
+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
-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;
+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.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
index 0919a4463468ef302a761bb5f71ec5c04c397a30..ba601298f45c187d0b8d4d207828d313040a72b3 100644
--- 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
@@ -4,9 +4,17 @@
[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?
+[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.
-tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specification for function strlen, generating default assigns from the prototype
+[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
@@ -19,31 +27,35 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat
__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.
+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.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.
+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.i:17:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c: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.
+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.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);
+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
-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);
+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 850e9faf10f9d5e1a0f6a918f0c9125c5315a0d8..88781aa15c8d61663a3234748a34e28d9c480fbc 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 =
@@ -198,38 +198,42 @@ class e_acsl_visitor prj generate = object (self)
f.globals <- new_globals
| 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;
-
- (* 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)
+ 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; (* 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 }, _)