From fbbd4716d19ade7f11b0aada36d752b6c32ddf24 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 22 Apr 2013 13:54:14 +0000
Subject: [PATCH] [E-ACSL] improve test
---
.../e-acsl-runtime/oracle/gen_ptr_init.c | 39 ++++++-------------
.../e-acsl-runtime/oracle/gen_ptr_init2.c | 39 ++++++-------------
.../oracle/ptr_init.1.res.oracle | 22 +++++++++--
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 22 +++++++++--
.../e-acsl/tests/e-acsl-runtime/ptr_init.c | 2 +-
5 files changed, 61 insertions(+), 63 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 9f336692a29..48ad882af35 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -119,14 +119,16 @@ void f(void)
void g(int *C, int *D)
{
- __store_block((void *)(& C),4U);
- __full_init((void *)(& C));
- __store_block((void *)(& D),4U);
- __full_init((void *)(& D));
- __full_init((void *)(& C));
- C = D;
+ /*@ assert \initialized(&C); */
+ {
+ int __e_acsl_initialized;
+ __store_block((void *)(& C),4U);
+ __full_init((void *)(& C));
+ __e_acsl_initialized = __initialized((void *)(& C),sizeof(int *));
+ e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"g",
+ (char *)"\\initialized(&C)",19);
+ }
__delete_block((void *)(& C));
- __delete_block((void *)(& D));
return;
}
@@ -144,51 +146,34 @@ int main(void)
int __retres;
int *x;
int *y;
- int *z;
- int *t;
e_acsl_global_init();
- __store_block((void *)(& t),4U);
- __store_block((void *)(& z),4U);
__store_block((void *)(& y),4U);
__store_block((void *)(& x),4U);
__full_init((void *)(& B));
B = (int *)__e_acsl_malloc(sizeof(int));
__full_init((void *)(& y));
y = (int *)__e_acsl_malloc(sizeof(int));
- __full_init((void *)(& t));
- t = (int *)__e_acsl_malloc(sizeof(int));
__full_init((void *)(& x));
x = y;
f();
- __full_init((void *)(& z));
- __full_init((void *)(& t));
- g(z,t);
/*@ assert \initialized(&A); */
{
int __e_acsl_initialized;
__e_acsl_initialized = __initialized((void *)(& A),sizeof(int *));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&A)",30);
+ (char *)"\\initialized(&A)",28);
}
/*@ assert \initialized(&x); */
{
int __e_acsl_initialized_2;
__e_acsl_initialized_2 = __initialized((void *)(& x),sizeof(int *));
e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&x)",31);
- }
- /*@ assert \initialized(&z); */
- {
- int __e_acsl_initialized_3;
- __e_acsl_initialized_3 = __initialized((void *)(& z),sizeof(int *));
- e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&z)",32);
+ (char *)"\\initialized(&x)",29);
}
+ g(x,y);
__retres = 0;
__delete_block((void *)(& B));
__delete_block((void *)(& A));
- __delete_block((void *)(& t));
- __delete_block((void *)(& z));
__delete_block((void *)(& y));
__delete_block((void *)(& x));
__clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index 9f336692a29..48ad882af35 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -119,14 +119,16 @@ void f(void)
void g(int *C, int *D)
{
- __store_block((void *)(& C),4U);
- __full_init((void *)(& C));
- __store_block((void *)(& D),4U);
- __full_init((void *)(& D));
- __full_init((void *)(& C));
- C = D;
+ /*@ assert \initialized(&C); */
+ {
+ int __e_acsl_initialized;
+ __store_block((void *)(& C),4U);
+ __full_init((void *)(& C));
+ __e_acsl_initialized = __initialized((void *)(& C),sizeof(int *));
+ e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"g",
+ (char *)"\\initialized(&C)",19);
+ }
__delete_block((void *)(& C));
- __delete_block((void *)(& D));
return;
}
@@ -144,51 +146,34 @@ int main(void)
int __retres;
int *x;
int *y;
- int *z;
- int *t;
e_acsl_global_init();
- __store_block((void *)(& t),4U);
- __store_block((void *)(& z),4U);
__store_block((void *)(& y),4U);
__store_block((void *)(& x),4U);
__full_init((void *)(& B));
B = (int *)__e_acsl_malloc(sizeof(int));
__full_init((void *)(& y));
y = (int *)__e_acsl_malloc(sizeof(int));
- __full_init((void *)(& t));
- t = (int *)__e_acsl_malloc(sizeof(int));
__full_init((void *)(& x));
x = y;
f();
- __full_init((void *)(& z));
- __full_init((void *)(& t));
- g(z,t);
/*@ assert \initialized(&A); */
{
int __e_acsl_initialized;
__e_acsl_initialized = __initialized((void *)(& A),sizeof(int *));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&A)",30);
+ (char *)"\\initialized(&A)",28);
}
/*@ assert \initialized(&x); */
{
int __e_acsl_initialized_2;
__e_acsl_initialized_2 = __initialized((void *)(& x),sizeof(int *));
e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&x)",31);
- }
- /*@ assert \initialized(&z); */
- {
- int __e_acsl_initialized_3;
- __e_acsl_initialized_3 = __initialized((void *)(& z),sizeof(int *));
- e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&z)",32);
+ (char *)"\\initialized(&x)",29);
}
+ g(x,y);
__retres = 0;
__delete_block((void *)(& B));
__delete_block((void *)(& A));
- __delete_block((void *)(& t));
- __delete_block((void *)(& z));
__delete_block((void *)(& y));
__delete_block((void *)(& x));
__clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 5e20a64ef64..22bf1abe67b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -29,9 +29,17 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: p
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&z);
-tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluation of
- argument z
+tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function __e_acsl_malloc:
@@ -41,5 +49,11 @@ tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluatio
[value] Values at end of function e_acsl_global_init:
[value] Values at end of function f:
A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+[value] Values at end of function g:
[value] Values at end of function main:
- NON TERMINATING FUNCTION
+ __fc_heap_status ∈ [--..--]
+ A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 5e20a64ef64..22bf1abe67b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -29,9 +29,17 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: p
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&z);
-tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluation of
- argument z
+tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function __e_acsl_malloc:
@@ -41,5 +49,11 @@ tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluatio
[value] Values at end of function e_acsl_global_init:
[value] Values at end of function f:
A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+[value] Values at end of function g:
[value] Values at end of function main:
- NON TERMINATING FUNCTION
+ __fc_heap_status ∈ [--..--]
+ A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+ __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
index cc1d4258b19..90576a4b9df 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
@@ -27,6 +27,6 @@ int main(void) {
f();
/*@ assert \initialized(&A); */
/*@ assert \initialized(&x); */
- g(y, x);
+ g(x, y);
return 0;
}
--
GitLab