diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index a8ccb4ffa76dedab4fcdfb60debd80d7c79a945e..e0f1930a8e435fd51f538c5470f5a18caab2a0c0 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,9 @@
# 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).
- E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
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.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index 5815cb1a61a5ca27578fd306824218f07cc48de4..4e61f70824a6f00644b83b2c698a6f5f84566b49 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:164:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index 86f84d89e21dffd565e7876659912b5e2595211f..41d37202e1a2364377ea88bf76532baf6918eb09 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:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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 fadc654284101121087fbae00b593429bdf12553..01d3b783fc56c1667b3c24cbe3aad8cdcc7912ef 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)",177);
+ __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 8b8a774cefe1a13f5908cc1587ca88907d1e56ad..22adeadaf337860713521be9c19ff340196b9803 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)",177);
+ __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.0.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1fd71344f0524cd97e4576973179306832d58b1c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
@@ -0,0 +1,40 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:155:[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:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:176:[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.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..23809a9f749e448e651d882452f6846a0984d71e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
@@ -0,0 +1,32 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:155:[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:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:176:[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..6663b24b9c945279c62ba5cb5c54f545fde4acb5
--- /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)",177);
+ __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..057f2dc23acf663dcebd6e5a1899bcf53cb543d4
--- /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)",177);
+ __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_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index c6dfb921e26a0368051322f07da8279faf1be6a7..cb9e2c5662cc9c03f14a4df0b1d00c07585d11f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -32,6 +32,39 @@ axiomatic dynamic_allocation {
*/
/*@ ghost extern int __e_acsl_init; */
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
+ unsigned long n);
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x;
+ assigns *x \from *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
+ assigns \result;
+ assigns \result \from *z1, *z2;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __init_args(int argc_ref,
char **argv_ref);
@@ -408,11 +441,19 @@ int main(int argc, char **argv)
/*@ assert \block_length(argv) ≡ (argc+1)*sizeof(char *); */
{
unsigned long __e_acsl_block_length;
+ mpz_t __e_acsl_block_length_2;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
__e_acsl_block_length = __block_length((void *)argv);
- e_acsl_assert(__e_acsl_block_length == (unsigned long)(((long)argc + (long)1) * 8L),
- (char *)"Assertion",(char *)"main",
+ __gmpz_init_set_ui(__e_acsl_block_length_2,__e_acsl_block_length);
+ __gmpz_init_set_si(__e_acsl,((long)argc + (long)1) * 8L);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_2),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"\\block_length(argv) == (argc+1)*sizeof(char *)",
15);
+ __gmpz_clear(__e_acsl_block_length_2);
+ __gmpz_clear(__e_acsl);
}
/*@ assert *(argv+argc) ≡ \null; */
{
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..e12f0483d9db710f0cc76ed0ce3141ee44465f74 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)",177);
+ __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..e12f0483d9db710f0cc76ed0ce3141ee44465f74 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)",177);
+ __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..6a21c2b0fdc1a35bb3e2616691ed72acd2a5152f 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)",177);
+ __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..02a86bbfc5b473640e690e0c1f6d812ebf5c79a5 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)",177);
+ __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..29c90249380ed4acc9dcb95b33eb09625df49d6f 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)",177);
+ __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..26735ad303626362343dbb7766776a0023843194 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)",177);
+ __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.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
index c292e7da4aa6959b31bf16306e81c4bbb7cccc2e..f01e69e5f86e1dd89184c7ecfc682896c30604b2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:164:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index b2510e830643b83751994851213f6b5522daf457..86217cc65455a1ec847418186c65173ef2922963 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:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
index 6ac96615ec8ce6c2c375c4beca003434a22687e0..db2c36636361940020b0252b0603e6d562f5768a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:164:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index e17b9826f4f82da61cf058f034ad2c9d86745948..19562f0d282d2c4d0dbcc5a4931b8b0bf43837f3 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:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
index e63dff47ba26ef47c5264f376ba7b09a5b6905a4..7a659870d1b546125c1b21c222fbcca085a08535 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:164:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index e46a99bed937bea2afe6718f0dc9e413d355b65e..be983fa8f53e2255d4396ae30f5be4e158f20c2d 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:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:155:[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:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[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:177:[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:177}
+FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __e_acsl_implies.
+ It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
+ {FRAMAC_SHARE/libc/stdlib.h:177}.
FRAMAC_SHARE/libc/stdlib.h:179:[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 824eb210ff2d10dbb2dea99dbdbdcec33bb1761e..c12d0c8c28a4f1602252a654525ef976288bbc38 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -84,7 +84,7 @@ let name_of_mpz_arith_bop = function
let constant_to_exp ~loc = function
| Integer(n, repr) ->
(try
- let kind = Typing.typ_of_integer n (Integer.ge n Integer.zero) in
+ let kind = Typing.ikind_of_integer n (Integer.ge n Integer.zero) in
if Typing.is_representable n kind then
Cil.kinteger64 ~loc ~kind ?repr n, false
else
@@ -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 *)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 89ae8344e8ffdc894c07b2d230689d65add3567d..36a1af9f2ec5111cc5c1cba82d7379ba9d6071d9 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -57,7 +57,7 @@ let pretty_eacsl_typ fmt = function
| Z -> Format.fprintf fmt "Z"
| No_integral lty -> Format.fprintf fmt "%a" Printer.pp_logic_type lty
-let typ_of_integer i unsigned =
+let ikind_of_integer i unsigned =
(* int whenever possible to prevent superfluous casts in the generated code *)
if Cil.fitsInInt IInt i then IInt else Cil.intKindForValue i unsigned
@@ -65,8 +65,8 @@ let typ_of_eacsl_typ = function
| Interv(l, u) ->
let is_pos = Z.ge l Z.zero in
(try
- let ty_l = TInt(typ_of_integer l is_pos, []) in
- let ty_u = TInt(typ_of_integer u is_pos, []) in
+ let ty_l = TInt(ikind_of_integer l is_pos, []) in
+ let ty_u = TInt(ikind_of_integer u is_pos, []) in
Cil.arithmeticConversion ty_l ty_u
with Cil.Not_representable ->
Mpz.t ())
@@ -322,12 +322,22 @@ let rec type_term t =
dup (join ty2) ty3
| Tat(t, _)
| Tbase_addr(_, t) -> dup type_term t
- | Toffset(_, t)
- | Tblock_length(_, t) ->
+ | Toffset(_, t) ->
ignore (type_term t);
- (* TODO: to be improved by computing the length of the type of the
- pointer *)
- dup eacsl_typ_of_typ Cil.theMachine.Cil.typeOfSizeOf
+ let n = Z.div (Bit_utils.max_bit_address ()) (Z.of_int 8) in
+ let ty =
+ try TInt(ikind_of_integer n true, [])
+ with Cil.Not_representable -> Mpz.t ()
+ in
+ dup eacsl_typ_of_typ ty
+ | Tblock_length(_, t) ->
+ ignore (type_term t);
+ let n = Z.div (Bit_utils.max_bit_size ()) (Z.of_int 8) in
+ let ty =
+ try TInt(ikind_of_integer n true, [])
+ with Cil.Not_representable -> Mpz.t ()
+ in
+ dup eacsl_typ_of_typ ty
| Tnull -> dup int_to_interv 0
| TLogic_coerce(_, t) -> dup type_term t
| TCoerce(t, ty) ->
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index f2cbdab0616d411200d2705bca34134c5e80935c..71cd5d84e6b29cf27d4857eb63a3d404441a8649 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -26,7 +26,7 @@ open Cil_types
(** {2 Typing} *)
(******************************************************************************)
-val typ_of_integer: Integer.t -> bool -> ikind
+val ikind_of_integer: Integer.t -> bool -> ikind
(** Compute the best type of a bigint. The boolean must be [true] for unsigned
and [false] for signed.
@raise Cil.Not_representable if the integer does not fit in any C type. *)