diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5eefc9d5eaa3432dc1ba3ee66b0d8146b5d2a4c3..e0f1930a8e435fd51f538c5470f5a18caab2a0c0 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2015/06/01] Support of \freeable. Thus illegal calls to
+ free (e.g. double free) are detected.
-* E-ACSL [2015/05/28] Fix types of \block_length and \offset.
- E-ACSL [2015/05/27] Search .h in the E-ACSL memory model by
default (easier to use declarations like __memory_size).
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index e2b407e15a02f66b65697f34c83ebbf1d4840def..416480e6e48783746bbdd1fe81599cd103311d92 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,12 @@
\subsection{Version \version}
+\begin{itemize}
+\item \changeinsection{alloc-dealloc}{include this section}
+\end{itemize}
+
+\subsection{Version 1.8}
+
\begin{itemize}
\item \changeinsection{locations}{Fix example \ref{ex:tset}}
\item \changeinsection{pointers}{Add grammar of memory-related terms and
@@ -88,6 +94,13 @@ in \lstinline|\\at|}
{
\section{Changes in \eacsl Implementation}
+\subsection{Version \eacslversion}
+
+\begin{itemize}
+\item \changeinsection{alloc-dealloc}{support of
+ \lstinline|\\freeable|}
+\end{itemize}
+
\subsection{Version 0.3}
\begin{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index c0a25d556aa20064bd9f4384fbbfca0e0eaafe18..86b8cd8244b4805b854fb1d1ea5450ab67ab370e 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.tex
@@ -31,6 +31,8 @@
you would not wonder if most tools do not support them (or support
them partially).}}
+\newcommand{\mywarning}[1]{\paragraph{Warning:} #1}
+
\newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
index 863199e5275dd5d195d156121c6875d2ea220eea..7626c08e864f13b87a275c02a23aac5f06aaef5e 100644
--- a/src/plugins/e-acsl/doc/refman/memory.tex
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -6,7 +6,7 @@
| { "\allocation" one-label? "(" term ")" };
\
pred ::= { "\allocable" one-label? "(" term ")" };
- | { "\freeable" one-label? "(" term ")" };
+ | "\freeable" { one-label? } "(" term ")" ;
| { "\fresh" two-labels? "(" term, term ")" };
| "\valid" { one-label? } "(" location-address ")" ;
| "\valid_read" { one-label? } "(" location-address ")";
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 71de79df78646bec39e0e573533827c748036b15..d86f2ae0aa473b0806f1de3844930a588b7aec08 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -650,7 +650,7 @@ axiomatics.
\section{Pointers and physical adressing}
\label{sec:pointers}
-\except{separation, allocation and deallocation is unsupported}
+\except{separation}
Figure~\ref{fig:gram:memory} shows the additional constructs for terms and
predicates which are related to memory location.
@@ -684,7 +684,11 @@ predicates which are related to memory location.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Allocation and deallocation}
-\absentexperimental
+\difficultswhy{All these constructs}{the implementation of a memory model}
+\label{sec:alloc-dealloc}
+
+\mywarning{this section is still almost experimental in \acsl. Thus it might still
+evolve in the future.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index 041c705681a7155a892db02645a0ed962d78926a..99d548f25039ec7ca07c37825237d546c0ed2e5e 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -302,12 +302,11 @@ 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) ->
+ | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t) | Pfreeable(_, t) ->
(* Options.feedback "REGISTER %a" Cil.d_term t;*)
state_ref := register_term kf !state_ref t;
Cil.DoChildren
| Pallocable _ -> Error.not_yet "\\allocable"
- | Pfreeable _ -> Error.not_yet "\\freeable"
| Pfresh _ -> Error.not_yet "\\fresh"
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index e38e2dfb3f63a53aeb64b7909e1dc66d90511768..1ab256f0b6655b131a7bad31ad715881335ce8bb 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -312,11 +312,11 @@ void __add_element (struct _block * ptr) {
}
-/* return the block B such as : begin addr of B == ptr
- we suppose that such a block exists, but we could return NULL if not */
+/* return the block B such as: begin addr of B == ptr if such a block exists,
+ return NULL otherwise */
/*@ assigns \nothing;
@ ensures \valid(\result);
- @ ensures \result->ptr == (size_t)ptr;
+ @ ensures \result == \null || \result->ptr == (size_t)ptr;
@*/
struct _block * __get_exact (void * ptr) {
struct bittree * tmp = __root;
@@ -326,8 +326,8 @@ struct _block * __get_exact (void * ptr) {
/*@ loop assigns tmp;
@*/
while(!tmp->is_leaf) {
- // prefix is consistent
- assert((tmp->addr & tmp->mask) == ((size_t)ptr & tmp->mask));
+ // if the ptr we are looking for does not share the prefix of tmp
+ if((tmp->addr & tmp->mask) != ((size_t)ptr & tmp->mask)) return NULL;
// two sons
assert(tmp->left != NULL && tmp->right != NULL);
// the prefix of one son is consistent
@@ -337,12 +337,10 @@ struct _block * __get_exact (void * ptr) {
else if((tmp->left->addr & tmp->left->mask)
== ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
- else
- assert(0);
+ else return NULL;
}
- assert(tmp->is_leaf);
- assert(tmp->leaf->ptr == (size_t)ptr);
+ if(tmp->leaf->ptr != (size_t)ptr) return NULL;
return tmp->leaf;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 9f252b1a2e1d3655a9dd71d1c9afb24d6b3147a5..f8ea8707d4145c86f9e607cdb3394df2c0e83746 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -56,6 +56,7 @@ void* __e_acsl_mmodel_memset (void* dest, int val, size_t len) {
size_t __memory_size = 0;
+struct _block * last_added_block = NULL; /* proceed with caution */
/*unsigned cpt_store_block = 0;*/
const int nbr_bits_to_1[256] = {
@@ -103,7 +104,9 @@ void* __store_block(void* ptr, size_t size) {
tmp->init_cpt = 0;
tmp->is_litteral_string = false;
tmp->is_out_of_bound = false;
+ tmp->freeable = false;
__add_element(tmp);
+ last_added_block = tmp;
/*cpt_store_block++;*/
return ptr;
}
@@ -128,7 +131,8 @@ void* __malloc(size_t size) {
if(tmp == NULL) return NULL;
tmp2 = __store_block(tmp, size);
__memory_size += size;
- assert(tmp2 != NULL);
+ assert(tmp2 != NULL && last_added_block != NULL);
+ last_added_block->freeable = true;
return tmp2;
}
@@ -146,6 +150,14 @@ void __free(void* ptr) {
free(tmp);
}
+int __freeable(void* ptr) {
+ struct _block * tmp;
+ if(ptr == NULL) return false;
+ tmp = __get_exact(ptr);
+ if(tmp == NULL) return false;
+ return tmp->freeable;
+}
+
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
void* __realloc(void* ptr, size_t size) {
@@ -197,6 +209,7 @@ void* __realloc(void* ptr, size_t size) {
}
}
tmp->size = size;
+ tmp->freeable = true;
__memory_size += size;
return (void*)tmp->ptr;
}
@@ -211,7 +224,8 @@ void* __calloc(size_t nbr_block, size_t size_block) {
if(tmp == NULL) return NULL;
tmp2 = __store_block(tmp, nbr_block * size_block);
__memory_size += nbr_block * size_block;
- assert(tmp2 != NULL);
+ assert(tmp2 != NULL && last_added_block != NULL);
+ last_added_block->freeable = true;
return tmp2;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 7dd28d91f6c9b086d45f154f997266a29fef3211..052bde62c82e2c9cc9d508fe7ce1ccd2074abfc0 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -38,6 +38,10 @@ void * __malloc(size_t size)
void __free(void * ptr)
__attribute__((FC_BUILTIN));
+/*@ assigns \result \from ptr; */
+int __freeable(void * ptr)
+ __attribute__((FC_BUILTIN));
+
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index d4cfb55ebf1da59d762fa7dca8de45b08c43a859..2805f60fb51a05929cf95ed9d5630ac9b2f0fdef 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -47,6 +47,7 @@ struct _block {
size_t init_cpt;
_Bool is_litteral_string;
_Bool is_out_of_bound;
+ _Bool freeable;
};
/* print the information about a block */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index ca19d80fd5e1d2cc8f6702a91db8ee236cfd2dd3..6f6d9fcd1fa3cf015fc6c7abdc389964526d8411 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -18,7 +17,6 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -46,6 +44,12 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __initialized
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 98e36f797bf76c4368c6ed1fed39c0bfcf247f89..82a233d27b8d702d8c56201c0bde049227b8e8ba 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -10,7 +9,6 @@ tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in beh
Ignoring annotation.
tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -54,6 +52,12 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
[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/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 1b1a391506d5596cc35477a5cb9de301c250ea98..85bbf2a6348c6c11fba231768c1f6d7f15459eb7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -41,6 +41,10 @@ void __free(void *p);
/*@ ghost extern int __e_acsl_init; */
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -136,8 +140,22 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
index 84b12d496e0a8cfe716211c0b95df80c4427ee8d..ca20c71ad132c237527507b2f932abd8676b54b1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
@@ -97,6 +97,10 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -183,8 +187,22 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
new file mode 100644
index 0000000000000000000000000000000000000000..c5b020ec82962791d740c0e7d57134f1209c63ca
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
@@ -0,0 +1,22 @@
+/* run.config
+ COMMENT: \freeable
+ STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ EXECNOW: LOG gen_freeable.c BIN gen_freeable.out @frama-c@ -machdep gcc_x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/freeable.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_freeable.c > /dev/null && ./gcc_runtime.sh freeable
+ EXECNOW: LOG gen_freeable2.c BIN gen_freeable2.out @frama-c@ -machdep gcc_x86_64 -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/freeable.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_freeable2.c > /dev/null && ./gcc_runtime.sh freeable2
+*/
+
+#include "stdlib.h"
+
+extern void *malloc(size_t p);
+extern void free(void* p);
+
+int main(void) {
+ int *p;
+ /*@ assert ! \freeable(p); */
+ /*@ assert ! \freeable((void*)0); */
+ p = (int*)malloc(4*sizeof(int));
+ /*@ assert ! \freeable(p+1); */
+ /*@ assert \freeable(p); */
+ free(p);
+ /*@ assert ! \freeable(p); */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b9c89336962420a8d643ab863f843abc02a31b82
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
@@ -0,0 +1,40 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' 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
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value: assert \initialized(&p);
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: completely indeterminate value in p.
+tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
+ argument (void *)p
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a44bd0d80cce17f792783a396d9050757fd94893
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
@@ -0,0 +1,32 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' 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
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value: assert \initialized(&p);
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: completely indeterminate value in p.
+tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
+ argument (void *)p
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
new file mode 100644
index 0000000000000000000000000000000000000000..0c1f458a6bcd371fe763ffaa8b17a1419b8510b9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -0,0 +1,188 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned long size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+void *__malloc(size_t size);
+
+void __free(void *p);
+
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires freeable: \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
+ return;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+int main(void)
+{
+ int __retres;
+ int *p;
+ __store_block((void *)(& p),8UL);
+ /*@ assert ¬\freeable(p); */
+ {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable((void *)p);
+ e_acsl_assert(! __e_acsl_freeable,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p)",15);
+ }
+ /*@ assert ¬\freeable((void *)0); */
+ {
+ int __e_acsl_freeable_2;
+ __e_acsl_freeable_2 = __freeable((void *)0);
+ e_acsl_assert(! __e_acsl_freeable_2,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable((void *)0)",16);
+ }
+ __full_init((void *)(& p));
+ p = (int *)__e_acsl_malloc((unsigned long)4 * sizeof(int));
+ /*@ assert ¬\freeable(p+1); */
+ {
+ int __e_acsl_freeable_3;
+ __e_acsl_freeable_3 = __freeable((void *)(p + 1));
+ e_acsl_assert(! __e_acsl_freeable_3,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p+1)",18);
+ }
+ /*@ assert \freeable(p); */
+ {
+ int __e_acsl_freeable_4;
+ __e_acsl_freeable_4 = __freeable((void *)p);
+ e_acsl_assert(__e_acsl_freeable_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\freeable(p)",19);
+ }
+ __e_acsl_free((void *)p);
+ /*@ assert ¬\freeable(p); */
+ {
+ int __e_acsl_freeable_5;
+ __e_acsl_freeable_5 = __freeable((void *)p);
+ e_acsl_assert(! __e_acsl_freeable_5,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p)",21);
+ }
+ __retres = 0;
+ __delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c
new file mode 100644
index 0000000000000000000000000000000000000000..a17fefbf8e56d0053450688d3783ffb053506817
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c
@@ -0,0 +1,188 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned long size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+void *__malloc(size_t size);
+
+void __free(void *p);
+
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires freeable: \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
+ return;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+int main(void)
+{
+ int __retres;
+ int *p;
+ __store_block((void *)(& p),8UL);
+ /*@ assert ¬\freeable(p); */
+ {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable((void *)p);
+ e_acsl_assert(! __e_acsl_freeable,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p)",15);
+ }
+ /*@ assert ¬\freeable((void *)0); */
+ {
+ int __e_acsl_freeable_2;
+ __e_acsl_freeable_2 = __freeable((void *)0);
+ e_acsl_assert(! __e_acsl_freeable_2,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable((void *)0)",16);
+ }
+ __full_init((void *)(& p));
+ p = (int *)__e_acsl_malloc((unsigned long)4 * sizeof(int));
+ /*@ assert ¬\freeable(p+1); */
+ {
+ int __e_acsl_freeable_3;
+ __e_acsl_freeable_3 = __freeable((void *)(p + (long)1));
+ e_acsl_assert(! __e_acsl_freeable_3,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p+1)",18);
+ }
+ /*@ assert \freeable(p); */
+ {
+ int __e_acsl_freeable_4;
+ __e_acsl_freeable_4 = __freeable((void *)p);
+ e_acsl_assert(__e_acsl_freeable_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\freeable(p)",19);
+ }
+ __e_acsl_free((void *)p);
+ /*@ assert ¬\freeable(p); */
+ {
+ int __e_acsl_freeable_5;
+ __e_acsl_freeable_5 = __freeable((void *)p);
+ e_acsl_assert(! __e_acsl_freeable_5,(char *)"Assertion",(char *)"main",
+ (char *)"!\\freeable(p)",21);
+ }
+ __retres = 0;
+ __delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index e63da0d3e7f1bc518389643fe8979d952ffa35f4..dcc4d484b7f6283d650ec413f496980d6445f9fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -35,6 +35,10 @@ void __free(void *p);
/*@ ghost extern int __e_acsl_init; */
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -133,10 +137,21 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),8UL);
- __store_block((void *)(& __e_acsl_at),4UL);
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
__delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index e63da0d3e7f1bc518389643fe8979d952ffa35f4..dcc4d484b7f6283d650ec413f496980d6445f9fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -35,6 +35,10 @@ void __free(void *p);
/*@ ghost extern int __e_acsl_init; */
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -133,10 +137,21 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),8UL);
- __store_block((void *)(& __e_acsl_at),4UL);
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),8UL);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4UL);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
__delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index db243d2e0634cc22715f601251b5ff36a36cc0ec..10af13f2e360850ea43249bda447adb4f9069955 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -35,6 +35,10 @@ void __free(void *p);
/*@ ghost extern int __e_acsl_init; */
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -137,10 +141,21 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
__delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 9379b88d9eadade5907f91250963b1720d5419d7..cf0bb965e72581f735959516c000c36db19922fa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -58,6 +58,10 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -151,10 +155,21 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __store_block((void *)(& __e_acsl_at),4U);
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
__delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 15e875caf18ba38d5a720d286d23772f65b28510..a1d838101aa902d8a9bd9f0dc957e5d71fbcda95 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -35,6 +35,10 @@ void __free(void *p);
/*@ ghost extern int __e_acsl_init; */
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -121,8 +125,22 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index 497c9c7411765223c95d5484dc65bd4446844f4a..32d2a13179a31c3770171c949c69fdd29e2342da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -58,6 +58,10 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+/*@ assigns \result;
+ assigns \result \from ptr; */
+extern __attribute__((__FC_BUILTIN__)) int __freeable(void *ptr);
+
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
@@ -144,8 +148,22 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __e_acsl_at = p != (void *)0;
- __free(p);
+ {
+ int __e_acsl_implies;
+ __store_block((void *)(& p),4U);
+ if (! (p != (void *)0)) __e_acsl_implies = 1;
+ else {
+ int __e_acsl_freeable;
+ __e_acsl_freeable = __freeable(p);
+ __e_acsl_implies = __e_acsl_freeable;
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
+ (char *)"p != \\null ==> \\freeable(p)",175);
+ __store_block((void *)(& __e_acsl_at),4U);
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ }
+ __delete_block((void *)(& p));
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index c3ae2925bf66404400ca61ec2ad1022913b0f420..b11b7ad11d58125ba6afc96b6b6e403953309bc1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -18,7 +17,6 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -60,6 +58,12 @@ tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 4a818423ac9b74967a108c77eade101b009c80b8..d99668b5130fc96bedecee592ddd534f0ef3cb12 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -10,7 +9,6 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clau
Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -52,6 +50,12 @@ tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 2da3ea9dfb651306b992df2918507b1df5bf83d1..34053c15663dcf89a7f9dd71f615988aa9e226d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -18,7 +17,6 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -49,6 +47,12 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
[value] using specification for function __valid_read
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index fcddec8a4b8ac3654748d38a2c02de2cf0f28eef..c589cbf216c4495f3a40ba7965584d37d4c77430 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -10,7 +9,6 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assign
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -47,6 +45,12 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition g
[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/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 3eea9bdbc1b63e7a7b5b51de74128965213daacb..310ecf7583605f389a039cd9869bcd051d7303cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -18,7 +17,6 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -49,6 +47,12 @@ tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 4eb0ff3fad7ca205c259b7d273f5b85443e36682..f7377306b50608aa2f54a9fc0e1f0e1d9a77b8a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
@@ -10,7 +9,6 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns cla
Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
@@ -48,6 +46,12 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition g
[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/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+[value] using specification for function __freeable
+:0:[value] Assigning imprecise value to __e_acsl_implies.
+ The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:175}
+FRAMAC_SHARE/libc/stdlib.h:175:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:175}.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index b177a968fcdbf9fa7463b5988de4b06fc19bbc43..c12d0c8c28a4f1602252a654525ef976288bbc38 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -456,7 +456,7 @@ and comparison_to_exp
else
Cil.new_exp ~loc (BinOp(bop, e1, e2, Cil.intType)), env
-(* \base_addr and \block_length annotations *)
+(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) None t in
let _, res, env =
@@ -657,7 +657,10 @@ and named_predicate_content_to_exp ?name kf env p =
| _ -> mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
- | Pfreeable _ -> not_yet env "\\free"
+ | Pfreeable(LogicLabel(_, label), t) when label = "Here" ->
+ let res, env, _, _ = mmodel_call ~loc kf "freeable" Cil.intType env t in
+ res, env
+ | Pfreeable _ -> not_yet env "labeled \\freeable"
| Pfresh _ -> not_yet env "\\fresh"
| Psubtype _ -> Error.untypable "subtyping relation" (* Jessie specific *)