diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c index 886159e1d67611a4203924e4b7b49269a98975fd..143514ebbcd2d183f2dedcb8d4e64ee93c191b64 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c @@ -34,26 +34,26 @@ int main(void) { /* Local variables also initialized by assignments */ b = 0; d[0] = 1; - /*@assert \initialized(&b) ; */ - /*@assert \initialized(q) ; */ - /*@assert ! \initialized(&d) ; */ + /*@assert \initialized(&b); */ + /*@assert \initialized(q); */ + /*@assert ! \initialized(&d); */ d[1] = 1; - /*@assert \initialized(&d) ; */ + /*@assert \initialized(&d); */ /* Malloc allocates un-initialized memory */ p = (int*)malloc(sizeof(int*)); - /*@assert ! \initialized(p) ; */ + /*@assert ! \initialized(p); */ /* Calloc allocates initialized memory */ q = (int*)calloc(1, sizeof(int)); - /*@ assert \initialized(q) ; */ + /*@ assert \initialized(q); */ /* Block reallocared using `realloc' carries initialization of the of the * existing fragment but does not initialize the newly allocated one */ q = (int*)realloc(q, 2*sizeof(int)); - /*@assert \initialized(q) ; */ + /*@assert \initialized(q); */ q++; - /*@assert ! \initialized(q) ; */ + /*@assert ! \initialized(q); */ q--; /* Initialized on un-allocated regions is always false. This does not lead @@ -61,6 +61,17 @@ int main(void) { * mode. */ free(p); free(q); - /*@assert ! \initialized(p) ; */ - /*@assert ! \initialized(q) ; */ -} + /*@assert ! \initialized(p); */ + /*@assert ! \initialized(q); */ + + /* Spoofing access to non-existing stack address */ + q = (int*)(&q - 1024*5); + /*assert ! \initialized(q); */ + + /* Spoofing access to non-existing global address */ + q = (int*)128; + /*@assert ! \initialized(q); */ + + p = NULL; + /*@assert ! \initialized(p); */ +} \ No newline at end of file diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c index dd211269b422d37f9ceb8edde052bd70d606b28d..c5cd0f5e667f4839ade860d6a307d09517b2188b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c @@ -191,6 +191,26 @@ int main(void) __e_acsl_assert(! __e_acsl_initialized_18,(char *)"Assertion", (char *)"main",(char *)"!\\initialized(q)",65); } + __full_init((void *)(& q)); + q = (int *)(& q - 1024 * 5); + __full_init((void *)(& q)); + q = (int *)128; + /*@ assert ¬\initialized(q); */ + { + int __e_acsl_initialized_19; + __e_acsl_initialized_19 = __initialized((void *)q,sizeof(int)); + __e_acsl_assert(! __e_acsl_initialized_19,(char *)"Assertion", + (char *)"main",(char *)"!\\initialized(q)",73); + } + __full_init((void *)(& p)); + p = (int *)0; + /*@ assert ¬\initialized(p); */ + { + int __e_acsl_initialized_20; + __e_acsl_initialized_20 = __initialized((void *)p,sizeof(int)); + __e_acsl_assert(! __e_acsl_initialized_20,(char *)"Assertion", + (char *)"main",(char *)"!\\initialized(p)",76); + } __retres = 0; __delete_block((void *)(& B)); __delete_block((void *)(& A)); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle index 843ddc6ecd98085e71b63586cba0c3c2774d8af0..9384d673883c42da48b63379eb72cac98be50b4d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle @@ -58,3 +58,5 @@ FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \poi FRAMAC_SHARE/libc/stdlib.h:177:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0); tests/e-acsl-runtime/initialized.c:64:[value] warning: assertion got status unknown. tests/e-acsl-runtime/initialized.c:65:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/initialized.c:73:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/initialized.c:76:[value] warning: assertion got status unknown.