Skip to content
Snippets Groups Projects
Commit 6f7e6c00 authored by Arvid Jakobsson's avatar Arvid Jakobsson
Browse files

Fixes to Juliens remarks, clearer code 

 - fix indentation
 - follow the model of must_init, build_initializer
 - only generated code if generate is set,
 - generate code "on project".
 - rename mainargs.i -> mainargs.c
parent ee58e767
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 802 additions and 82 deletions
src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.i → src/plugins/e-acsl/tests/e-acsl-runtime/mainargs.c
+ 2
− 2
View file @ 6f7e6c00
/* run.config /* run.config
COMMENT: the contents of argv should be valid 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_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.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_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> #include <string.h>
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+ 351
− 5
View file @ 6f7e6c00
...@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 { ...@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 {
typedef struct __anonstruct___mpz_struct_1 __mpz_struct; typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1]; typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t; typedef unsigned int size_t;
typedef int wchar_t;
/*@ requires predicate ≢ 0; /*@ requires predicate ≢ 0;
assigns \nothing; */ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate, extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
...@@ -88,11 +89,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void); ...@@ -88,11 +89,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
predicate diffSize{L1, L2}(ℤ i) = predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i; \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/ */
/*@ assigns \result, *(x_0+(0 ..)); /*@
assigns \result \from *(x_0+(0 ..)); axiomatic
assigns *(x_0+(0 ..)) \from *(x_0+(0 ..)); 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) int main(int argc, char **argv)
{ {
...@@ -183,7 +527,9 @@ int main(int argc, char **argv) ...@@ -183,7 +527,9 @@ int main(int argc, char **argv)
while (i < argc) { while (i < argc) {
{ {
int len; int len;
len = strlen(*(argv + i)); size_t tmp;
tmp = __e_acsl_strlen((char const *)*(argv + i));
len = (int)tmp;
/*@ assert \valid(*(argv+i)); */ /*@ assert \valid(*(argv+i)); */
{ {
int __e_acsl_initialized_2; int __e_acsl_initialized_2;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
+ 351
− 5
View file @ 6f7e6c00
...@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 { ...@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_1 {
typedef struct __anonstruct___mpz_struct_1 __mpz_struct; typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1]; typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t; typedef unsigned int size_t;
typedef int wchar_t;
/*@ requires predicate ≢ 0; /*@ requires predicate ≢ 0;
assigns \nothing; */ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate, extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
...@@ -162,11 +163,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void); ...@@ -162,11 +163,354 @@ extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
predicate diffSize{L1, L2}(ℤ i) = predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i; \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/ */
/*@ assigns \result, *(x_0+(0 ..)); /*@
assigns \result \from *(x_0+(0 ..)); axiomatic
assigns *(x_0+(0 ..)) \from *(x_0+(0 ..)); 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) int main(int argc, char **argv)
{ {
...@@ -309,7 +653,9 @@ int main(int argc, char **argv) ...@@ -309,7 +653,9 @@ int main(int argc, char **argv)
while (i < argc) { while (i < argc) {
{ {
int len; int len;
len = strlen(*(argv + i)); size_t tmp;
tmp = __e_acsl_strlen((char const *)*(argv + i));
len = (int)tmp;
/*@ assert \valid(*(argv+i)); */ /*@ assert \valid(*(argv+i)); */
{ {
int __e_acsl_initialized_2; int __e_acsl_initialized_2;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+ 31
− 19
View file @ 6f7e6c00
...@@ -4,9 +4,17 @@ ...@@ -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_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_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. -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. [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". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
...@@ -19,13 +27,13 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat ...@@ -19,13 +27,13 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
[value] using specification for function __init_args [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 __store_block
[value] using specification for function __valid [value] using specification for function __valid
[value] using specification for function e_acsl_assert [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. 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.c:13:[value] Assertion got status valid.
tests/e-acsl-runtime/mainargs.i:14:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown.
[value] using specification for function __gmpz_init [value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. 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 [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 ...@@ -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. FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear [value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. 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 [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: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. 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 ...@@ -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: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: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. 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 __block_length
[value] using specification for function __gmpz_init_set_ui [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. 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 ...@@ -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: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: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. 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 [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.c: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:18:[value] Assertion got status unknown.
[value] using specification for function __initialized [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.c: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.c: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: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 [value] using specification for function strlen
tests/e-acsl-runtime/mainargs.i:21:[value] Assertion got status unknown. FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
tests/e-acsl-runtime/mainargs.i:21:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i); FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
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 __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] using specification for function __e_acsl_memory_clean
[value] done for function main [value] done for function main
[value] ====== VALUES COMPUTED ====== [value] ====== VALUES COMPUTED ======
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
+ 30
− 18
View file @ 6f7e6c00
...@@ -4,9 +4,17 @@ ...@@ -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_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_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. -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. [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". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
...@@ -19,31 +27,35 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat ...@@ -19,31 +27,35 @@ tests/e-acsl-runtime/mainargs.i:20:[kernel] warning: Neither code nor specificat
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
[value] using specification for function __init_args [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 __store_block
[value] using specification for function __valid [value] using specification for function __valid
[value] using specification for function e_acsl_assert [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. 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.c:13:[value] Assertion got status valid.
tests/e-acsl-runtime/mainargs.i:14:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c: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.c: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:15:[value] Assertion got status unknown.
[value] using specification for function __block_length [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 [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.c: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:18:[value] Assertion got status unknown.
[value] using specification for function __initialized [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.c: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.c: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: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 [value] using specification for function strlen
tests/e-acsl-runtime/mainargs.i:21:[value] Assertion got status unknown. FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
tests/e-acsl-runtime/mainargs.i:21:[kernel] warning: out of bounds read. assert \valid_read(argv+i); FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
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 __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] using specification for function __e_acsl_memory_clean
[value] done for function main [value] done for function main
[value] ====== VALUES COMPUTED ====== [value] ====== VALUES COMPUTED ======
src/plugins/e-acsl/visit.ml
+ 37
− 33
View file @ 6f7e6c00
...@@ -110,7 +110,7 @@ class e_acsl_visitor prj generate = object (self) ...@@ -110,7 +110,7 @@ class e_acsl_visitor prj generate = object (self)
with Exit -> with Exit ->
true true
in in
if must_init then if must_init then begin
let build_initializer () = let build_initializer () =
Options.feedback ~dkey ~level:2 "building global initializer."; Options.feedback ~dkey ~level:2 "building global initializer.";
let return = let return =
...@@ -198,38 +198,42 @@ class e_acsl_visitor prj generate = object (self) ...@@ -198,38 +198,42 @@ class e_acsl_visitor prj generate = object (self)
f.globals <- new_globals f.globals <- new_globals
| None -> | None ->
Kernel.warning "@[no entry point specified:@ \ Kernel.warning "@[no entry point specified:@ \
you must call function `%s' and `__e_acsl_memory_clean by yourself.@]" you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
fname; fname;
f.globals <- f.globals @ [ cil_fct ] f.globals <- f.globals @ [ cil_fct ]
in in
Project.on prj build_initializer () Project.on prj build_initializer ()
end; end; (* must_init *)
let must_init_args = match main_fct with
(* init memory store, and then add program arguments if there | Some main ->
are any. must be called before global variables are let charPtrPtrType = TPtr(Cil.charPtrType,[]) in
initialized. *) (* this might not be valid in an embedded environment,
if Pre_analysis.use_model () then begin where int/char** arguments is not necessarily
match main_fct with valid *)
| Some main -> (match main.sformals with
let charPtrPtrType = TPtr(Cil.charPtrType,[]) in | vi1::vi2::_ when
let loc = Location.unknown in vi1.vtype = Cil.intType && vi2.vtype = charPtrPtrType
(* this might not be valid in an embedded environment, && Pre_analysis.must_model_vi vi2 -> true
where int/char** arguments is not necessarily valid *) | _ -> false)
let stmts_pre = match main.sformals with | None -> false
| { vtype = t1 }::{ vtype = t2 }::_ when in
t1 = Cil.intType && t2 = charPtrPtrType -> if must_init_args then begin
let args = (List.map Cil.evar main.sformals) in (* init memory store, and then add program arguments if
[(Misc.mk_call loc "__init_args" args)] there are any. must be called before global variables
| _ -> [] are initialized. *)
in let build_args_initializer () =
main.sbody.bstmts <- stmts_pre @ main.sbody.bstmts; let main = Extlib.the main_fct in
| None -> () let loc = Location.unknown in
end; let args = (List.map Cil.evar main.sformals) in
let call = Misc.mk_call loc "__init_args" args in
(* reset copied states at the end to be observationally equivalent to a main.sbody.bstmts <- call :: main.sbody.bstmts;
standard visitor. *) in Project.on prj build_args_initializer ();
if generate then Project.clear ~selection ~project:prj (); end;
f) (* 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 method !vglob_aux = function
| GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _) | GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment