[E-ACSL] do not monitor anymore memory locations involved in constructs not...

[E-ACSL] do not monitor anymore memory locations involved in constructs not yet supported like \freeable

src/plugins/e-acsl/pre_analysis.ml

@@ -197,12 +197,12 @@ module rec Transfer
   let register_object kf state_ref = object
     inherit Visitor.frama_c_inplace
     method vpredicate = function
-    | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t)
-    | Pallocable(_, t) | Pfreeable(_, t) | Pfresh(_, _, t, _) ->
+    | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t) ->
       (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
       state_ref := register_term kf !state_ref t;
       Cil.SkipChildren
-    | Pseparated _ -> Error.not_yet "\\separated"
+    | Pallocable _ | Pfreeable _ | Pfresh _ | Pseparated _ -> 
+      Error.not_yet "\\separated"
     | Ptrue | Pfalse | Papp _ | Prel _
     | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _ 
     | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c

@@ -106,13 +106,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c

@@ -106,13 +106,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c

@@ -123,13 +123,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 
@@ -155,13 +149,8 @@ void *__e_acsl_malloc(size_t size)
 void __e_acsl_free(void *p)
 {
   int __e_acsl_at;
-  __store_block((void *)(& p),4U);
-  __full_init((void *)(& p));
-  __store_block((void *)(& __e_acsl_at),4U);
-  __full_init((void *)(& __e_acsl_at));
   __e_acsl_at = p != (void *)0;
   __free(p);
-  __delete_block((void *)(& p));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c

@@ -123,13 +123,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 
@@ -155,13 +149,8 @@ void *__e_acsl_malloc(size_t size)
 void __e_acsl_free(void *p)
 {
   int __e_acsl_at;
-  __store_block((void *)(& p),4U);
-  __full_init((void *)(& p));
-  __store_block((void *)(& __e_acsl_at),4U);
-  __full_init((void *)(& __e_acsl_at));
   __e_acsl_at = p != (void *)0;
   __free(p);
-  __delete_block((void *)(& p));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c

@@ -131,13 +131,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 
@@ -163,13 +157,8 @@ void *__e_acsl_malloc(size_t size)
 void __e_acsl_free(void *p)
 {
   int __e_acsl_at;
-  __store_block((void *)(& p),4U);
-  __full_init((void *)(& p));
-  __store_block((void *)(& __e_acsl_at),4U);
-  __full_init((void *)(& __e_acsl_at));
   __e_acsl_at = p != (void *)0;
   __free(p);
-  __delete_block((void *)(& p));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c

@@ -147,13 +147,7 @@ extern size_t __memory_size;
 void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
-  __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
-  __full_init((void *)(& size));
-  __full_init((void *)(& __retres));
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
-  __delete_block((void *)(& __retres));
   return __retres;
 }
 
@@ -179,13 +173,8 @@ void *__e_acsl_malloc(size_t size)
 void __e_acsl_free(void *p)
 {
   int __e_acsl_at;
-  __store_block((void *)(& p),4U);
-  __full_init((void *)(& p));
-  __store_block((void *)(& __e_acsl_at),4U);
-  __full_init((void *)(& __e_acsl_at));
   __e_acsl_at = p != (void *)0;
   __free(p);
-  __delete_block((void *)(& p));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle

@@ -5,6 +5,7 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/localvar.c"
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -21,7 +22,6 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
         __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
@@ -31,6 +31,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
 [value] using specification for function __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.
+[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

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle

@@ -5,6 +5,7 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/localvar.c"
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -21,7 +22,6 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
         __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
@@ -31,6 +31,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
 [value] using specification for function __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.
+[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

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle

@@ -5,6 +5,8 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +41,6 @@ tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function
 [value] using specification for function __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.
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
@@ -62,6 +63,7 @@ tests/e-acsl-runtime/valid.c:19:[value] all evaluations are invalid for function
         (void *)y
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle

@@ -5,6 +5,8 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +41,6 @@ tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function
 [value] using specification for function __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.
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
@@ -62,6 +63,7 @@ tests/e-acsl-runtime/valid.c:19:[value] all evaluations are invalid for function
         (void *)y
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle

@@ -5,6 +5,8 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_alias.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -37,7 +39,6 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
         (void *)b
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
@@ -58,6 +59,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value tha
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)b
+[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

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle

@@ -5,6 +5,8 @@
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
 [kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
 [kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_alias.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -37,7 +39,6 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
         (void *)b
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-[value] using specification for function __delete_block
 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 invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
@@ -66,6 +67,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value tha
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
         (void *)b
+[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