From 75521ab49eb8555e251c412a2e062264b2b436a1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 28 Nov 2012 09:09:06 +0000
Subject: [PATCH] [E-ACSL] improve a bit mmodel external API
---
src/plugins/e-acsl/misc.ml | 44 +++---
.../e-acsl/memory_model/e_acsl_bittree.c | 28 ++--
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 107 +++++--------
.../share/e-acsl/memory_model/e_acsl_mmodel.h | 30 ++--
.../e-acsl/memory_model/e_acsl_mmodel_api.h | 33 ++--
.../e-acsl/tests/e-acsl-runtime/localvar.c | 2 +-
.../e-acsl-runtime/oracle/at.1.res.oracle | 8 +-
.../tests/e-acsl-runtime/oracle/at.res.oracle | 8 +-
.../oracle/bts1304.1.res.oracle | 14 +-
.../e-acsl-runtime/oracle/bts1304.res.oracle | 14 +-
.../oracle/bts1307.1.res.oracle | 18 +--
.../e-acsl-runtime/oracle/bts1307.res.oracle | 18 +--
.../oracle/comparison.1.res.oracle | 6 +-
.../oracle/comparison.res.oracle | 6 +-
.../tests/e-acsl-runtime/oracle/gen_at.c | 78 +++++-----
.../tests/e-acsl-runtime/oracle/gen_at2.c | 74 ++++-----
.../tests/e-acsl-runtime/oracle/gen_bts1304.c | 30 ++--
.../e-acsl-runtime/oracle/gen_bts13042.c | 30 ++--
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 146 +++++++++---------
.../e-acsl-runtime/oracle/gen_bts13072.c | 146 +++++++++---------
.../e-acsl-runtime/oracle/gen_comparison.c | 14 +-
.../e-acsl-runtime/oracle/gen_comparison2.c | 14 +-
.../oracle/gen_literal_string.c | 104 ++++++-------
.../oracle/gen_literal_string2.c | 100 ++++++------
.../e-acsl-runtime/oracle/gen_localvar.c | 30 ++--
.../e-acsl-runtime/oracle/gen_localvar2.c | 30 ++--
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 63 ++++----
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 44 +++---
.../tests/e-acsl-runtime/oracle/gen_valid.c | 132 ++++++++--------
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 132 ++++++++--------
.../e-acsl-runtime/oracle/gen_valid_alias.c | 78 +++++-----
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 70 ++++-----
.../oracle/gen_valid_in_contract.c | 14 +-
.../oracle/gen_valid_in_contract2.c | 14 +-
.../oracle/literal_string.1.res.oracle | 18 +--
.../oracle/literal_string.res.oracle | 18 +--
.../oracle/localvar.1.res.oracle | 14 +-
.../e-acsl-runtime/oracle/localvar.res.oracle | 14 +-
.../e-acsl-runtime/oracle/ptr.1.res.oracle | 8 +-
.../e-acsl-runtime/oracle/ptr.res.oracle | 16 +-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 16 +-
.../e-acsl-runtime/oracle/valid.res.oracle | 16 +-
.../oracle/valid_alias.1.res.oracle | 20 +--
.../oracle/valid_alias.res.oracle | 18 +--
.../oracle/valid_in_contract.1.res.oracle | 8 +-
.../oracle/valid_in_contract.res.oracle | 8 +-
.../e-acsl/tests/e-acsl-runtime/valid.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/valid_alias.c | 2 +-
.../tests/e-acsl-runtime/valid_in_contract.c | 2 +-
src/plugins/e-acsl/translate.ml | 8 +-
src/plugins/e-acsl/visit.ml | 2 +-
51 files changed, 917 insertions(+), 952 deletions(-)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 90acc4ebcca..5af291b0a16 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -70,13 +70,6 @@ let mk_call ?(loc=Location.unknown) ?result fname args =
in
mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
-let mk_debug_mmodel_stmt stmt =
- if Options.debug_atleast 2 then
- let debug = mk_call "__debug" [] in
- Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
- else
- stmt
-
type annotation_kind = Assertion | Precondition | Postcondition | Invariant
let kind_to_string loc k =
@@ -115,36 +108,41 @@ let result_vi kf = match result_lhost kf with
| Var vi -> vi
| Mem _ -> assert false
+(* TODO: convert -debug 2 into a new debugging category *)
+let mk_debug_mmodel_stmt stmt =
+ if Options.debug_atleast 2 then
+ let debug = mk_call "__debug" [] in
+ Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
+ else
+ stmt
+
let mk_full_init_stmt ?(addr=true) vi =
let loc = vi.vdecl in
let stmt = match addr, Cil.unrollType vi.vtype with
| _, TArray(_,Some _, _, _) | false, _ ->
- mk_call ~loc "_full_init" [ Cil.evar ~loc vi ]
- | _ -> mk_call ~loc "_full_init" [ Cil.mkAddrOfVi vi ]
+ mk_call ~loc "__full_init" [ Cil.evar ~loc vi ]
+ | _ -> mk_call ~loc "__full_init" [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
let mk_initialize ~loc (host, offset as lv) = match host, offset with
- | Var _, NoOffset -> mk_call ~loc "_full_init" [ Cil.mkAddrOf ~loc lv ]
+ | Var _, NoOffset -> mk_call ~loc "__full_init" [ Cil.mkAddrOf ~loc lv ]
| _ ->
let typ = Cil.typeOfLval lv in
mk_call ~loc
- "_initialize"
+ "__initialize"
[ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
let mk_store_stmt ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
+ let store = mk_call ~loc "__store_block" in
let stmt = match ty, str_size with
- | TArray(_, Some _,_,_), None ->
- mk_call ~loc "_store_block" [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
- | TPtr(TInt(IChar, _), _), Some size ->
- mk_call ~loc "_store_block" [ Cil.evar ~loc vi ; size ]
- | _, None ->
- mk_call ~loc "_store_block"
- [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
- | _, Some _ ->
- assert false
+ | TArray(_, Some _,_,_), None ->
+ store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
+ | TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
+ | _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
+ | _, Some _ -> assert false
in
mk_debug_mmodel_stmt stmt
@@ -152,15 +150,15 @@ let mk_delete_stmt vi =
let loc = vi.vdecl in
let stmt = match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
- mk_call ~loc "_delete_block" [ Cil.evar ~loc vi ]
+ mk_call ~loc "__delete_block" [ Cil.evar ~loc vi ]
(* | Tarray(_, None, _, _)*)
- | _ -> mk_call ~loc "_delete_block" [ Cil.mkAddrOfVi vi ]
+ | _ -> mk_call ~loc "__delete_block" [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
let mk_literal_string vi =
let loc = vi.vdecl in
- let stmt = mk_call ~loc "_literal_string" [ Cil.evar ~loc vi ] in
+ let stmt = mk_call ~loc "__literal_string" [ Cil.evar ~loc vi ] in
mk_debug_mmodel_stmt stmt
(*
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 7e685244e8d..71d5161f499 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
@@ -105,7 +105,6 @@ unsigned long mask(void * a, void * b) {
return Tmasks[-i];
}
-
/* logical AND of a bittree and a new node */
void* and(struct bittree * a, struct _block * b) {
return (void*) ((unsigned long)a->addr & (unsigned long)b->ptr);
@@ -116,9 +115,8 @@ int matches_mask(struct bittree * a, void * b) {
return ((unsigned long)a->addr & a->mask) == ((unsigned long)b & a->mask);
}
-
/* remove the block from the structure */
-void _remove_element (struct _block * ptr) {
+void __remove_element (struct _block * ptr) {
struct bittree * curr = __root;
assert(__root != NULL);
assert(ptr != NULL);
@@ -169,9 +167,8 @@ void _remove_element (struct _block * ptr) {
}
}
-
/* add a block in the structure */
-void _add_element (struct _block * ptr) {
+void __add_element (struct _block * ptr) {
struct bittree * new_leaf;
assert(ptr != NULL);
@@ -241,10 +238,9 @@ 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 */
-struct _block * _get_exact (void * ptr) {
+struct _block * __get_exact (void * ptr) {
struct bittree * tmp = __root;
if(__root == NULL || ptr == NULL) return NULL;
@@ -263,12 +259,11 @@ struct _block * _get_exact (void * ptr) {
}
}
-
/* return the block B containing ptr, starting from b and only exploring
left children, or NULL if such block does not exist
- THIS METHOD IS INVOKED FROM _get_cont ONLY
+ THIS METHOD IS INVOKED FROM __get_cont ONLY
DO NOT CALL IT FROM ANYWHERE ELSE */
-struct _block * _get_cont_by_left_child (void * ptr, struct bittree * b) {
+struct _block * __get_cont_by_left_child (void * ptr, struct bittree * b) {
struct bittree * tmp = b;
assert(((unsigned long)b->addr & b->mask) == ((unsigned long)ptr & b->mask));
@@ -285,11 +280,10 @@ struct _block * _get_cont_by_left_child (void * ptr, struct bittree * b) {
return (tmp->addr == ptr) ? tmp->leaf : NULL;
}
-
/* return the block B containing ptr, such as :
begin addr of B <= ptr < (begin addr + size) of B
or NULL if such a block does not exist */
-struct _block * _get_cont (void * ptr) {
+struct _block * __get_cont (void * ptr) {
struct bittree * tmp = __root;
if(__root == NULL || ptr == NULL) return NULL;
@@ -308,7 +302,7 @@ struct _block * _get_cont (void * ptr) {
if(((unsigned long)tmp->right->addr & tmp->right->mask)
== (unsigned long)ptr) {
- struct _block * r = _get_cont_by_left_child(ptr, tmp->right);
+ struct _block * r = __get_cont_by_left_child(ptr, tmp->right);
if(r == NULL)
tmp = tmp->left;
else
@@ -326,18 +320,16 @@ struct _block * _get_cont (void * ptr) {
}
}
-
/*******************/
/* CLEAN */
/*******************/
-
/* recursively erase the content of the structure,
do not call directly */
void __clean_rec (struct bittree * ptr) {
if(ptr == NULL) return;
else if(ptr->is_leaf) {
- _clean_block(ptr->leaf);
+ __clean_block(ptr->leaf);
ptr->leaf = NULL;
}
else {
@@ -354,19 +346,17 @@ void __clean_struct () {
__root = NULL;
}
-
/*********************/
/* DEBUG */
/*********************/
-
/* recursively print the content of the structure
do not call directly */
void __debug_rec (struct bittree * ptr) {
if(ptr == NULL) return;
else if(ptr->is_leaf) {
printf("\t\t\t");
- _print_block(ptr->leaf);
+ __print_block(ptr->leaf);
}
else {
__debug_rec(ptr->left);
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 568cfcdfafb..5db9d3cdd25 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
@@ -11,16 +11,12 @@ const int nbr_bits_to_1[256] = {
0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
};
-
-
size_t needed_bytes (size_t size) {
return (size % 8) == 0 ? (size/8) : (size/8 + 1);
}
-
-
/* store the block of size bytes starting at ptr */
-void* _store_block(void* ptr, size_t size) {
+void* __store_block(void* ptr, size_t size) {
struct _block * tmp;
assert(ptr != NULL);
tmp = malloc(sizeof(struct _block));
@@ -30,61 +26,57 @@ void* _store_block(void* ptr, size_t size) {
tmp->init_ptr = NULL;
tmp->init_cpt = 0;
tmp->is_litteral_string = false;
- _add_element(tmp);
+ __add_element(tmp);
return ptr;
}
-
/* remove the block starting at ptr */
-void _delete_block(void* ptr) {
+void __delete_block(void* ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_exact(ptr);
+ tmp = __get_exact(ptr);
assert(tmp != NULL);
- _clean_init(tmp);
- _remove_element(tmp);
+ __clean_init(tmp);
+ __remove_element(tmp);
free(tmp);
}
-
/* allocate size bytes and store the returned block
* for further information, see malloc */
-void* _malloc(size_t size) {
+void* __malloc(size_t size) {
void * tmp, * tmp2;
if(size <= 0) return NULL;
tmp = malloc(size);
if(tmp == NULL) return NULL;
- tmp2 = _store_block(tmp, size);
+ tmp2 = __store_block(tmp, size);
assert(tmp2 != NULL);
return tmp2;
}
-
/* free the block starting at ptr,
* for further information, see free */
-void _free(void* ptr) {
+void __free(void* ptr) {
struct _block * tmp;
if(ptr == NULL) return;
- tmp = _get_exact(ptr);
+ tmp = __get_exact(ptr);
assert(tmp != NULL);
free(ptr);
- _clean_init(tmp);
- _remove_element(tmp);
+ __clean_init(tmp);
+ __remove_element(tmp);
free(tmp);
}
-
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
-void* _realloc(void* ptr, size_t size) {
+void* __realloc(void* ptr, size_t size) {
struct _block * tmp;
void * new_ptr;
- if(ptr == NULL) return _malloc(size);
+ if(ptr == NULL) return __malloc(size);
if(size <= 0) {
- _free(ptr);
+ __free(ptr);
return NULL;
}
- tmp = _get_exact(ptr);
+ tmp = __get_exact(ptr);
assert(tmp != NULL);
new_ptr = realloc(tmp->ptr, size);
if(new_ptr == NULL) return NULL;
@@ -126,28 +118,26 @@ void* _realloc(void* ptr, size_t size) {
return tmp->ptr;
}
-
/* allocate memory for an array of nbr_block elements of size_block size,
* this memory is set to zero, the returned block is stored,
* for further information, see calloc */
-void* _calloc(size_t nbr_block, size_t size_block) {
+void* __calloc(size_t nbr_block, size_t size_block) {
void * tmp, * tmp2;
if(nbr_block * size_block <= 0) return NULL;
tmp = calloc(nbr_block, size_block);
if(tmp == NULL) return NULL;
- tmp2 = _store_block(tmp, nbr_block * size_block);
+ tmp2 = __store_block(tmp, nbr_block * size_block);
assert(tmp2 != NULL);
return tmp2;
}
-
/* mark the size bytes of ptr as initialized */
-void _initialize (void * ptr, size_t size) {
+void __initialize (void * ptr, size_t size) {
struct _block * tmp;
unsigned i;
assert(ptr != NULL);
assert(size > 0);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
assert(tmp != NULL);
/* already fully initialized, do nothing */
@@ -175,12 +165,11 @@ void _initialize (void * ptr, size_t size) {
}
}
-
/* mark all bytes of ptr as initialized */
-void _full_init (void * ptr) {
+void __full_init (void * ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_exact(ptr);
+ tmp = __get_exact(ptr);
assert(tmp != NULL);
if (tmp->init_ptr != NULL) {
@@ -191,24 +180,22 @@ void _full_init (void * ptr) {
tmp->init_cpt = tmp->size;
}
-
/* mark a block as litteral string */
-void _literal_string (void * ptr) {
+void __literal_string (void * ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_exact(ptr);
+ tmp = __get_exact(ptr);
assert(tmp != NULL);
tmp->is_litteral_string = true;
}
-
/* return whether the size bytes of ptr are initialized */
-int _initialized (void * ptr, size_t size) {
+int __initialized (void * ptr, size_t size) {
struct _block * tmp;
unsigned i;
assert(ptr != NULL);
assert(size > 0);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
if(tmp == NULL)
return false;
@@ -227,70 +214,62 @@ int _initialized (void * ptr, size_t size) {
return true;
}
-
/* return the length (in bytes) of the block containing ptr */
-size_t _block_length(void* ptr) {
+size_t __block_length(void* ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
assert(tmp != NULL);
return tmp->size;
}
-
/* return whether the size bytes of ptr are readable/writable */
-int _valid(void* ptr, size_t size) {
+int __valid(void* ptr, size_t size) {
struct _block * tmp;
if(ptr == NULL)
return false;
assert(size > 0);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
return (tmp == NULL) ?
false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size
&& !tmp->is_litteral_string);
}
-
/* return whether the size bytes of ptr are readable */
-int _valid_read(void* ptr, size_t size) {
+int __valid_read(void* ptr, size_t size) {
struct _block * tmp;
if(ptr == NULL)
return false;
assert(size > 0);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
return (tmp == NULL) ?
false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size );
}
-
/* return the base address of the block containing ptr */
-void* _base_addr(void* ptr) {
+void* __base_addr(void* ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
assert(tmp != NULL);
return tmp->ptr;
}
-
/* return the offset of ptr within its block */
-/* TODO: remove `size` parameter */
-int _offset(void* ptr, size_t size) {
+int _offset(void* ptr) {
struct _block * tmp;
assert(ptr != NULL);
- tmp = _get_cont(ptr);
+ tmp = __get_cont(ptr);
assert(tmp != NULL);
return ((char*)ptr - tmp->ptr);
}
-
/*******************/
/* PRINT */
/*******************/
-
/* print the information about a block */
-void _print_block (struct _block * ptr) {
+void __print_block (struct _block * ptr) {
if (ptr != NULL) {
printf("%p %zu (litt:%i); [init] : %li ",
ptr->ptr, ptr->size, ptr->is_litteral_string, ptr->init_cpt);
@@ -306,14 +285,12 @@ void _print_block (struct _block * ptr) {
}
}
-
/********************/
/* CLEAN */
/********************/
-
/* erase information about initialization of a block */
-void _clean_init (struct _block * ptr) {
+void __clean_init (struct _block * ptr) {
if(ptr->init_ptr != NULL) {
free(ptr->init_ptr);
ptr->init_ptr = NULL;
@@ -321,26 +298,22 @@ void _clean_init (struct _block * ptr) {
ptr->init_cpt = 0;
}
-
/* erase all information about a block */
-void _clean_block (struct _block * ptr) {
+void __clean_block (struct _block * ptr) {
if(ptr == NULL) return;
- _clean_init(ptr);
+ __clean_init(ptr);
free(ptr);
}
-
/* erase the content of the abstract structure */
void __clean() {
__clean_struct();
}
-
/**********************/
/* DEBUG */
/**********************/
-
/* print the content of the abstract structure */
void __debug() {
__debug_struct();
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 4636e3a4b32..11707e813a9 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
@@ -6,50 +6,50 @@
/* allocate size bytes and store the returned block
* for further information, see malloc */
-void * _malloc(size_t size)
+void * __malloc(size_t size)
__attribute__((FC_BUILTIN)) ;
/* free the block starting at ptr,
* for further information, see free */
-void _free(void * ptr)
+void __free(void * ptr)
__attribute__((FC_BUILTIN));
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
-void * _realloc(void * ptr, size_t size)
+void * __realloc(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* allocate memory for an array of nbr_block elements of size_block size,
* this memory is set to zero, the returned block is stored,
* for further information, see calloc */
-void * _calloc(size_t nbr_elt, size_t size_elt)
+void * __calloc(size_t nbr_elt, size_t size_elt)
__attribute__((FC_BUILTIN));
/* From outside the library, the following functions have no side effect */
/* store the block of size bytes starting at ptr */
/*@ assigns \nothing; */
-void * _store_block(void * ptr, size_t size)
+void * __store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* remove the block starting at ptr */
/*@ assigns \nothing; */
-void _delete_block(void * ptr)
+void __delete_block(void * ptr)
__attribute__((FC_BUILTIN));
/* mark the size bytes of ptr as initialized */
/*@ assigns \nothing; */
-void _initialize(void * ptr, size_t size)
+void __initialize(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* mark all bytes of ptr as initialized */
/*@ assigns \nothing; */
-void _full_init(void * ptr)
+void __full_init(void * ptr)
__attribute__((FC_BUILTIN));
/* marks a block as litteral string */
/*@ assigns \nothing; */
-void _literal_string(void * ptr)
+void __literal_string(void * ptr)
__attribute__((FC_BUILTIN));
/* ****************** */
@@ -58,34 +58,34 @@ void _literal_string(void * ptr)
/* return whether the first size bytes of ptr are readable/writable */
/*@ assigns \nothing; */
-int _valid(void * ptr, size_t size)
+int __valid(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* return whether the first size bytes of ptr are readable */
/*@ assigns \nothing; */
-int _valid_read(void * ptr, size_t size)
+int __valid_read(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* return the base address of the block containing ptr */
/*@ assigns \nothing; */
-void * _base_addr(void * ptr)
+void * __base_addr(void * ptr)
__attribute__((FC_BUILTIN));
/* return the length (in bytes) of the block containing ptr */
/*@ assigns \nothing; */
-size_t _block_length(void * ptr)
+size_t __block_length(void * ptr)
__attribute__((FC_BUILTIN));
/* return the offset of ptr within its block */
/*@ assigns \nothing; */
-int _offset(void * ptr, size_t size)
+int __offset(void * ptr)
__attribute__((FC_BUILTIN));
/* return whether the size bytes of ptr are initialized */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \initialized(((char *)ptr)+(0..size-1));
@ assigns \nothing; */
-int _initialized(void * ptr, size_t size)
+int __initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/* print the content of the abstract structure */
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 ab31e733eaf..44e9fc6b944 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
@@ -14,35 +14,38 @@ struct _block {
_Bool is_litteral_string;
};
-
/* print the information about a block */
-void _print_block ( struct _block * ptr );
-/* erase information about initialization of a block */
-void _clean_init ( struct _block * ptr );
-/* erase all information about a block */
-void _clean_block ( struct _block * ptr );
+void __print_block(struct _block * ptr );
+/* erase information about initialization of a block */
+void __clean_init(struct _block * ptr );
-/* functions to be implemented */
-
+/* erase all information about a block */
+void __clean_block(struct _block * ptr);
/* remove the block from the structure */
-void _remove_element ( struct _block * );
+void __remove_element(struct _block *);
+
/* add a block in the structure */
-void _add_element ( struct _block * );
+void __add_element(struct _block *);
+
/* 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 */
-struct _block * _get_exact ( void * );
+struct _block * __get_exact(void *);
+
/* return the block B such as : begin addr of B > ptr
or NULL if such a block does not exist */
-struct _block * _get_next ( void * );
+struct _block * __get_next(void *);
+
/* return the block B containing ptr, such as :
begin addr of B <= ptr < (begin addr + size) of B
or NULL if such a block does not exist */
-struct _block * _get_cont ( void * );
+struct _block * __get_cont(void *);
+
/* erase the content of the structure */
-void __clean_struct ( );
+void __clean_struct(void);
+
/* print the content of the structure */
-void __debug_struct ( );
+void __debug_struct(void);
#endif
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
index da412680b27..02904fa6222 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: allocation and de-allocation of local variables
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_localvar.c BIN gen_localvar.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar.c > /dev/null && ./gcc_test.sh localvar
EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_test.sh localvar2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index 97d0ca4f9c3..f624fcec6c7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -26,8 +26,8 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
@@ -63,12 +63,12 @@ tests/e-acsl-runtime/at.i:51:[value] cannot evaluate ACSL term, unsupported ACSL
tests/e-acsl-runtime/at.i:51:[value] Assertion got status unknown.
tests/e-acsl-runtime/at.i:52:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:52:[value] Assertion got status unknown.
-[value] using specification for function _initialize
+[value] using specification for function __initialize
tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
:0:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index a2cc6637b48..ea6731c7ef5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -26,8 +26,8 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/at.i:45:[value] Assertion got status valid.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/at.i:13:[value] Assertion got status valid.
@@ -43,12 +43,12 @@ tests/e-acsl-runtime/at.i:51:[value] cannot evaluate ACSL term, unsupported ACSL
tests/e-acsl-runtime/at.i:51:[value] Assertion got status unknown.
tests/e-acsl-runtime/at.i:52:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:52:[value] Assertion got status unknown.
-[value] using specification for function _initialize
+[value] using specification for function __initialize
tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
:0:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index e69cb55f9ff..115671f1a74 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -25,15 +25,15 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
+[value] using specification for function __store_block
tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function _full_init
-[value] using specification for function _initialize
-[value] using specification for function _delete_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
+[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index e69cb55f9ff..115671f1a74 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -25,15 +25,15 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
+[value] using specification for function __store_block
tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
-[value] using specification for function _full_init
-[value] using specification for function _initialize
-[value] using specification for function _delete_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
+[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index a67081f760d..17e1deb75fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -30,17 +30,17 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: missing guard for ensuring t
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
-[value] using specification for function _valid
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
-[value] using specification for function _initialize
+[value] using specification for function __initialize
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
@@ -58,12 +58,12 @@ tests/e-acsl-runtime/bts1307.i:13:[value] Assertion got status valid.
./share/e-acsl/e_acsl_gmp.h:154:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_get_ui
./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid_read
tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: assert(Ook)
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __gmpz_clear
./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index fb5fa874e1e..aa96b812135 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -28,23 +28,23 @@ tests/e-acsl-runtime/bts1307.i:31:[e-acsl] approximating a real number by a floa
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
-[value] using specification for function _valid
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
-[value] using specification for function _initialize
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __initialize
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid_read
tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: assert(Ook)
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
tests/e-acsl-runtime/bts1307.i:19:[value] Function bar: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:20:[value] Function bar: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index b5b39a0ff21..4fea204e899 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -39,9 +39,9 @@ tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid.
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _literal_string
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 13cf34f6bfc..0bbfc3dba2e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -30,9 +30,9 @@ tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid.
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _literal_string
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:18:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index bc018871bc9..553e15d8a5f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -53,15 +53,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
@@ -106,32 +106,32 @@ void g(int *p, int *q)
int __e_acsl_at_3;
int __e_acsl_at_2;
int __e_acsl_at;
- _store_block((void *)(& p),4U);
- _full_init((void *)(& p));
- _store_block((void *)(& q),4U);
- _full_init((void *)(& q));
- _initialize((void *)p,sizeof(int));
+ __store_block((void *)(& p),4U);
+ __full_init((void *)(& p));
+ __store_block((void *)(& q),4U);
+ __full_init((void *)(& q));
+ __initialize((void *)p,sizeof(int));
*p = 0;
- _initialize((void *)(p + 1),sizeof(int));
+ __initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 1;
- _initialize((void *)q,sizeof(int));
+ __initialize((void *)q,sizeof(int));
*q = 0;
- _initialize((void *)p,sizeof(int));
+ __initialize((void *)p,sizeof(int));
L1:
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = *q;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = *q;
*p = 2;
- _initialize((void *)(p + 1),sizeof(int));
+ __initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
- _initialize((void *)q,sizeof(int));
+ __initialize((void *)q,sizeof(int));
*q = 1;
L2:
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = *(p + __e_acsl_at);
A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */
@@ -139,13 +139,13 @@ void g(int *p, int *q)
(char *)"\\at(*(p+\\at(*q,L1)),L2) == 2",32);
L3:
/*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */
- _store_block((void *)(& __e_acsl_at_4),4U);
- _full_init((void *)(& __e_acsl_at_4));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = *(p + __e_acsl_at_3);
e_acsl_assert(__e_acsl_at_4 == 2,(char *)"Assertion",
(char *)"\\at(*(p+\\at(*q,L1)),Here) == 2",34);
- _delete_block((void *)(& p));
- _delete_block((void *)(& q));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& q));
return;
}
@@ -157,25 +157,25 @@ int main(void)
int __retres;
int x;
int t[2];
- _store_block((void *)(t),8U);
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
+ __store_block((void *)(t),8U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
x = 0;
L:
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = x;
- _store_block((void *)(& __e_acsl_at_2),8U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),8U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = (long long)x + (long long)1;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = x;
/*@ assert x ≡ 0; */
e_acsl_assert(x == 0,(char *)"Assertion",(char *)"x == 0",45);
- _full_init((void *)(& x));
+ __full_init((void *)(& x));
x = 1;
- _full_init((void *)(& x));
+ __full_init((void *)(& x));
x = 2;
f();
/*@ assert \at(x,L) ≡ 0; */
@@ -189,8 +189,8 @@ int main(void)
(char *)"Assertion",(char *)"\\at(x,L)+1 == 1",52);
g(t,& x);
__retres = 0;
- _delete_block((void *)(t));
- _delete_block((void *)(& x));
+ __delete_block((void *)(t));
+ __delete_block((void *)(& x));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index 9cf0eb0e4fa..0eb4912a2ac 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -102,15 +102,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
@@ -215,32 +215,32 @@ void g(int *p, int *q)
int __e_acsl_at_3;
int __e_acsl_at_2;
int __e_acsl_at;
- _store_block((void *)(& p),4U);
- _full_init((void *)(& p));
- _store_block((void *)(& q),4U);
- _full_init((void *)(& q));
- _initialize((void *)p,sizeof(int));
+ __store_block((void *)(& p),4U);
+ __full_init((void *)(& p));
+ __store_block((void *)(& q),4U);
+ __full_init((void *)(& q));
+ __initialize((void *)p,sizeof(int));
*p = 0;
- _initialize((void *)(p + 1),sizeof(int));
+ __initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 1;
- _initialize((void *)q,sizeof(int));
+ __initialize((void *)q,sizeof(int));
*q = 0;
- _initialize((void *)p,sizeof(int));
+ __initialize((void *)p,sizeof(int));
L1:
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = *q;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = *q;
*p = 2;
- _initialize((void *)(p + 1),sizeof(int));
+ __initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
- _initialize((void *)q,sizeof(int));
+ __initialize((void *)q,sizeof(int));
*q = 1;
L2:
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = *(p + (long)__e_acsl_at);
A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */
@@ -264,8 +264,8 @@ void g(int *p, int *q)
mpz_t __e_acsl_3;
mpz_t __e_acsl_4;
int __e_acsl_eq_2;
- _store_block((void *)(& __e_acsl_at_4),4U);
- _full_init((void *)(& __e_acsl_at_4));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = *(p + (long)__e_acsl_at_3);
__gmpz_init_set_si(__e_acsl_3,(long)__e_acsl_at_4);
__gmpz_init_set_si(__e_acsl_4,(long)2);
@@ -277,8 +277,8 @@ void g(int *p, int *q)
__gmpz_clear(__e_acsl_4);
}
- _delete_block((void *)(& p));
- _delete_block((void *)(& q));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& q));
return;
}
@@ -290,13 +290,13 @@ int main(void)
int __retres;
int x;
int t[2];
- _store_block((void *)(t),8U);
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
+ __store_block((void *)(t),8U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
x = 0;
L:
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = x;
{
mpz_t __e_acsl_x_2;
@@ -313,8 +313,8 @@ int main(void)
__gmpz_clear(__e_acsl_add);
}
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = x;
/*@ assert x ≡ 0; */
{
@@ -330,9 +330,9 @@ int main(void)
__gmpz_clear(__e_acsl);
}
- _full_init((void *)(& x));
+ __full_init((void *)(& x));
x = 1;
- _full_init((void *)(& x));
+ __full_init((void *)(& x));
x = 2;
f();
/*@ assert \at(x,L) ≡ 0; */
@@ -385,8 +385,8 @@ int main(void)
g(t,& x);
__retres = 0;
__gmpz_clear(__e_acsl_at_2);
- _delete_block((void *)(t));
- _delete_block((void *)(& x));
+ __delete_block((void *)(t));
+ __delete_block((void *)(& x));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index 152a92a8e0f..a6910b32407 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -69,31 +69,31 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
void read_sensor_4(unsigned int *m)
{
- _store_block((void *)(& m),4U);
- _full_init((void *)(& m));
- _initialize((void *)m,sizeof(unsigned int));
+ __store_block((void *)(& m),4U);
+ __full_init((void *)(& m));
+ __initialize((void *)m,sizeof(unsigned int));
*m = 0U;
- _delete_block((void *)(& m));
+ __delete_block((void *)(& m));
return;
}
@@ -102,7 +102,7 @@ int main(void)
int __retres;
unsigned char buf[12U];
int i;
- _store_block((void *)(buf),12U);
+ __store_block((void *)(buf),12U);
i = 0;
while ((unsigned int)i < 3U) {
read_sensor_4((unsigned int *)(buf) + i);
@@ -111,13 +111,13 @@ int main(void)
/*@ assert \initialized((union msg *)buf); */
{
int __e_acsl_initialized;
- __e_acsl_initialized = _initialized((void *)(buf),sizeof(union msg));
+ __e_acsl_initialized = __initialized((void *)(buf),sizeof(union msg));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized((union msg *)buf)",25);
}
__retres = 0;
- _delete_block((void *)(buf));
+ __delete_block((void *)(buf));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index 152a92a8e0f..a6910b32407 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -69,31 +69,31 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
void read_sensor_4(unsigned int *m)
{
- _store_block((void *)(& m),4U);
- _full_init((void *)(& m));
- _initialize((void *)m,sizeof(unsigned int));
+ __store_block((void *)(& m),4U);
+ __full_init((void *)(& m));
+ __initialize((void *)m,sizeof(unsigned int));
*m = 0U;
- _delete_block((void *)(& m));
+ __delete_block((void *)(& m));
return;
}
@@ -102,7 +102,7 @@ int main(void)
int __retres;
unsigned char buf[12U];
int i;
- _store_block((void *)(buf),12U);
+ __store_block((void *)(buf),12U);
i = 0;
while ((unsigned int)i < 3U) {
read_sensor_4((unsigned int *)(buf) + i);
@@ -111,13 +111,13 @@ int main(void)
/*@ assert \initialized((union msg *)buf); */
{
int __e_acsl_initialized;
- __e_acsl_initialized = _initialized((void *)(buf),sizeof(union msg));
+ __e_acsl_initialized = __initialized((void *)(buf),sizeof(union msg));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized((union msg *)buf)",25);
}
__retres = 0;
- _delete_block((void *)(buf));
+ __delete_block((void *)(buf));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index a88a7a45ddd..15fb4cc4625 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -53,28 +53,28 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
@@ -95,30 +95,30 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- _store_block((void *)(& Mtmax_in),4U);
- _full_init((void *)(& Mtmax_in));
- _store_block((void *)(& Mwmax),4U);
- _full_init((void *)(& Mwmax));
- _store_block((void *)(& Mtmax_out),4U);
- _full_init((void *)(& Mtmax_out));
- __e_acsl_valid = _valid((void *)Mtmax_in,sizeof(float));
+ __store_block((void *)(& Mtmax_in),4U);
+ __full_init((void *)(& Mtmax_in));
+ __store_block((void *)(& Mwmax),4U);
+ __full_init((void *)(& Mwmax));
+ __store_block((void *)(& Mtmax_out),4U);
+ __full_init((void *)(& Mtmax_out));
+ __e_acsl_valid = __valid((void *)Mtmax_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
(char *)"\\valid(Mtmax_in)",7);
- __e_acsl_valid_2 = _valid((void *)Mwmax,sizeof(float));
+ __e_acsl_valid_2 = __valid((void *)Mwmax,sizeof(float));
e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",
(char *)"\\valid(Mwmax)",8);
- __e_acsl_valid_3 = _valid((void *)Mtmax_out,sizeof(float));
+ __e_acsl_valid_3 = __valid((void *)Mtmax_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",
(char *)"\\valid(Mtmax_out)",9);
- _initialize((void *)Mtmax_out,sizeof(float));
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __initialize((void *)Mtmax_out,sizeof(float));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = Mwmax;
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = Mtmax_in;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = Mtmax_out;
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
@@ -131,32 +131,32 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __e_acsl_and_2;
int __e_acsl_initialized_3;
int __e_acsl_and_3;
- __e_acsl_initialized = _initialized((void *)(& __e_acsl_at_3),
- sizeof(float *));
+ __e_acsl_initialized = __initialized((void *)(& __e_acsl_at_3),
+ sizeof(float *));
if (__e_acsl_initialized) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)__e_acsl_at_3,sizeof(float));
+ __e_acsl_valid_read = __valid_read((void *)__e_acsl_at_3,sizeof(float));
__e_acsl_and = __e_acsl_valid_read;
}
else { __e_acsl_and = 0; }
e_acsl_assert(__e_acsl_and,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_3)",0);
- __e_acsl_initialized_2 = _initialized((void *)(& __e_acsl_at_2),
- sizeof(float *));
+ __e_acsl_initialized_2 = __initialized((void *)(& __e_acsl_at_2),
+ sizeof(float *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_read_2;
- __e_acsl_valid_read_2 = _valid_read((void *)__e_acsl_at_2,
- sizeof(float));
+ __e_acsl_valid_read_2 = __valid_read((void *)__e_acsl_at_2,
+ sizeof(float));
__e_acsl_and_2 = __e_acsl_valid_read_2;
}
else { __e_acsl_and_2 = 0; }
e_acsl_assert(__e_acsl_and_2,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_2)",0);
- __e_acsl_initialized_3 = _initialized((void *)(& __e_acsl_at),
- sizeof(float *));
+ __e_acsl_initialized_3 = __initialized((void *)(& __e_acsl_at),
+ sizeof(float *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_read_3;
- __e_acsl_valid_read_3 = _valid_read((void *)__e_acsl_at,sizeof(float));
+ __e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
__e_acsl_and_3 = __e_acsl_valid_read_3;
}
else { __e_acsl_and_3 = 0; }
@@ -166,9 +166,9 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(char *)"Postcondition",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
13);
- _delete_block((void *)(& Mtmax_in));
- _delete_block((void *)(& Mwmax));
- _delete_block((void *)(& Mtmax_out));
+ __delete_block((void *)(& Mtmax_in));
+ __delete_block((void *)(& Mwmax));
+ __delete_block((void *)(& Mtmax_out));
return;
}
@@ -196,39 +196,39 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- _store_block((void *)(& Mtmin_in),4U);
- _full_init((void *)(& Mtmin_in));
- _store_block((void *)(& Mwmin),4U);
- _full_init((void *)(& Mwmin));
- _store_block((void *)(& Mtmin_out),4U);
- _full_init((void *)(& Mtmin_out));
- __e_acsl_valid = _valid((void *)Mtmin_in,sizeof(float));
+ __store_block((void *)(& Mtmin_in),4U);
+ __full_init((void *)(& Mtmin_in));
+ __store_block((void *)(& Mwmin),4U);
+ __full_init((void *)(& Mwmin));
+ __store_block((void *)(& Mtmin_out),4U);
+ __full_init((void *)(& Mtmin_out));
+ __e_acsl_valid = __valid((void *)Mtmin_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
(char *)"\\valid(Mtmin_in)",19);
- __e_acsl_valid_2 = _valid((void *)Mwmin,sizeof(float));
+ __e_acsl_valid_2 = __valid((void *)Mwmin,sizeof(float));
e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",
(char *)"\\valid(Mwmin)",20);
- __e_acsl_valid_3 = _valid((void *)Mtmin_out,sizeof(float));
+ __e_acsl_valid_3 = __valid((void *)Mtmin_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",
(char *)"\\valid(Mtmin_out)",21);
- _initialize((void *)Mtmin_out,sizeof(float));
- _store_block((void *)(& __e_acsl_at_6),4U);
- _full_init((void *)(& __e_acsl_at_6));
+ __initialize((void *)Mtmin_out,sizeof(float));
+ __store_block((void *)(& __e_acsl_at_6),4U);
+ __full_init((void *)(& __e_acsl_at_6));
__e_acsl_at_6 = Mwmin;
- _store_block((void *)(& __e_acsl_at_5),4U);
- _full_init((void *)(& __e_acsl_at_5));
+ __store_block((void *)(& __e_acsl_at_5),4U);
+ __full_init((void *)(& __e_acsl_at_5));
__e_acsl_at_5 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at_4),4U);
- _full_init((void *)(& __e_acsl_at_4));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = Mwmin;
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = Mtmin_out;
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
}
@@ -245,9 +245,9 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
(char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.: 0.85**\\old(Mwmin) != 0.",
25);
- _delete_block((void *)(& Mtmin_in));
- _delete_block((void *)(& Mwmin));
- _delete_block((void *)(& Mtmin_out));
+ __delete_block((void *)(& Mtmin_in));
+ __delete_block((void *)(& Mwmin));
+ __delete_block((void *)(& Mtmin_out));
return;
}
@@ -259,19 +259,19 @@ int main(void)
float f;
float g;
float h;
- _store_block((void *)(& h),4U);
- _store_block((void *)(& g),4U);
- _store_block((void *)(& f),4U);
- _full_init((void *)(& f));
+ __store_block((void *)(& h),4U);
+ __store_block((void *)(& g),4U);
+ __store_block((void *)(& f),4U);
+ __full_init((void *)(& f));
f = (float)1.0;
- _full_init((void *)(& g));
+ __full_init((void *)(& g));
g = (float)1.0;
foo(& f,& g,& h);
bar(& f,& g,& h);
__retres = 0;
- _delete_block((void *)(& h));
- _delete_block((void *)(& g));
- _delete_block((void *)(& f));
+ __delete_block((void *)(& h));
+ __delete_block((void *)(& g));
+ __delete_block((void *)(& f));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index ae4eb5d5003..a9bcd84bb2d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -105,28 +105,28 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
@@ -147,30 +147,30 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- _store_block((void *)(& Mtmax_in),4U);
- _full_init((void *)(& Mtmax_in));
- _store_block((void *)(& Mwmax),4U);
- _full_init((void *)(& Mwmax));
- _store_block((void *)(& Mtmax_out),4U);
- _full_init((void *)(& Mtmax_out));
- __e_acsl_valid = _valid((void *)Mtmax_in,sizeof(float));
+ __store_block((void *)(& Mtmax_in),4U);
+ __full_init((void *)(& Mtmax_in));
+ __store_block((void *)(& Mwmax),4U);
+ __full_init((void *)(& Mwmax));
+ __store_block((void *)(& Mtmax_out),4U);
+ __full_init((void *)(& Mtmax_out));
+ __e_acsl_valid = __valid((void *)Mtmax_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
(char *)"\\valid(Mtmax_in)",7);
- __e_acsl_valid_2 = _valid((void *)Mwmax,sizeof(float));
+ __e_acsl_valid_2 = __valid((void *)Mwmax,sizeof(float));
e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",
(char *)"\\valid(Mwmax)",8);
- __e_acsl_valid_3 = _valid((void *)Mtmax_out,sizeof(float));
+ __e_acsl_valid_3 = __valid((void *)Mtmax_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",
(char *)"\\valid(Mtmax_out)",9);
- _initialize((void *)Mtmax_out,sizeof(float));
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __initialize((void *)Mtmax_out,sizeof(float));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = Mwmax;
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = Mtmax_in;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = Mtmax_out;
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
@@ -201,32 +201,32 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpz_tdiv_q(__e_acsl_div,(__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_2));
__e_acsl_4 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_div));
- __e_acsl_initialized = _initialized((void *)(& __e_acsl_at_3),
- sizeof(float *));
+ __e_acsl_initialized = __initialized((void *)(& __e_acsl_at_3),
+ sizeof(float *));
if (__e_acsl_initialized) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)__e_acsl_at_3,sizeof(float));
+ __e_acsl_valid_read = __valid_read((void *)__e_acsl_at_3,sizeof(float));
__e_acsl_and = __e_acsl_valid_read;
}
else { __e_acsl_and = 0; }
e_acsl_assert(__e_acsl_and,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_3)",0);
- __e_acsl_initialized_2 = _initialized((void *)(& __e_acsl_at_2),
- sizeof(float *));
+ __e_acsl_initialized_2 = __initialized((void *)(& __e_acsl_at_2),
+ sizeof(float *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_read_2;
- __e_acsl_valid_read_2 = _valid_read((void *)__e_acsl_at_2,
- sizeof(float));
+ __e_acsl_valid_read_2 = __valid_read((void *)__e_acsl_at_2,
+ sizeof(float));
__e_acsl_and_2 = __e_acsl_valid_read_2;
}
else { __e_acsl_and_2 = 0; }
e_acsl_assert(__e_acsl_and_2,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_2)",0);
- __e_acsl_initialized_3 = _initialized((void *)(& __e_acsl_at),
- sizeof(float *));
+ __e_acsl_initialized_3 = __initialized((void *)(& __e_acsl_at),
+ sizeof(float *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_read_3;
- __e_acsl_valid_read_3 = _valid_read((void *)__e_acsl_at,sizeof(float));
+ __e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
__e_acsl_and_3 = __e_acsl_valid_read_3;
}
else { __e_acsl_and_3 = 0; }
@@ -236,9 +236,9 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(char *)"Postcondition",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
13);
- _delete_block((void *)(& Mtmax_in));
- _delete_block((void *)(& Mwmax));
- _delete_block((void *)(& Mtmax_out));
+ __delete_block((void *)(& Mtmax_in));
+ __delete_block((void *)(& Mwmax));
+ __delete_block((void *)(& Mtmax_out));
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
@@ -270,39 +270,39 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __e_acsl_valid;
int __e_acsl_valid_2;
int __e_acsl_valid_3;
- _store_block((void *)(& Mtmin_in),4U);
- _full_init((void *)(& Mtmin_in));
- _store_block((void *)(& Mwmin),4U);
- _full_init((void *)(& Mwmin));
- _store_block((void *)(& Mtmin_out),4U);
- _full_init((void *)(& Mtmin_out));
- __e_acsl_valid = _valid((void *)Mtmin_in,sizeof(float));
+ __store_block((void *)(& Mtmin_in),4U);
+ __full_init((void *)(& Mtmin_in));
+ __store_block((void *)(& Mwmin),4U);
+ __full_init((void *)(& Mwmin));
+ __store_block((void *)(& Mtmin_out),4U);
+ __full_init((void *)(& Mtmin_out));
+ __e_acsl_valid = __valid((void *)Mtmin_in,sizeof(float));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
(char *)"\\valid(Mtmin_in)",19);
- __e_acsl_valid_2 = _valid((void *)Mwmin,sizeof(float));
+ __e_acsl_valid_2 = __valid((void *)Mwmin,sizeof(float));
e_acsl_assert(__e_acsl_valid_2,(char *)"Precondition",
(char *)"\\valid(Mwmin)",20);
- __e_acsl_valid_3 = _valid((void *)Mtmin_out,sizeof(float));
+ __e_acsl_valid_3 = __valid((void *)Mtmin_out,sizeof(float));
e_acsl_assert(__e_acsl_valid_3,(char *)"Precondition",
(char *)"\\valid(Mtmin_out)",21);
- _initialize((void *)Mtmin_out,sizeof(float));
- _store_block((void *)(& __e_acsl_at_6),4U);
- _full_init((void *)(& __e_acsl_at_6));
+ __initialize((void *)Mtmin_out,sizeof(float));
+ __store_block((void *)(& __e_acsl_at_6),4U);
+ __full_init((void *)(& __e_acsl_at_6));
__e_acsl_at_6 = Mwmin;
- _store_block((void *)(& __e_acsl_at_5),4U);
- _full_init((void *)(& __e_acsl_at_5));
+ __store_block((void *)(& __e_acsl_at_5),4U);
+ __full_init((void *)(& __e_acsl_at_5));
__e_acsl_at_5 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at_4),4U);
- _full_init((void *)(& __e_acsl_at_4));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = Mwmin;
- _store_block((void *)(& __e_acsl_at_3),4U);
- _full_init((void *)(& __e_acsl_at_3));
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
__e_acsl_at_3 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at_2),4U);
- _full_init((void *)(& __e_acsl_at_2));
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = Mtmin_in;
- _store_block((void *)(& __e_acsl_at),4U);
- _full_init((void *)(& __e_acsl_at));
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = Mtmin_out;
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
}
@@ -325,9 +325,9 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
(char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.: 0.85**\\old(Mwmin) != 0.",
25);
- _delete_block((void *)(& Mtmin_in));
- _delete_block((void *)(& Mwmin));
- _delete_block((void *)(& Mtmin_out));
+ __delete_block((void *)(& Mtmin_in));
+ __delete_block((void *)(& Mwmin));
+ __delete_block((void *)(& Mtmin_out));
__gmpz_clear(__e_acsl_and);
return;
}
@@ -340,19 +340,19 @@ int main(void)
float f;
float g;
float h;
- _store_block((void *)(& h),4U);
- _store_block((void *)(& g),4U);
- _store_block((void *)(& f),4U);
- _full_init((void *)(& f));
+ __store_block((void *)(& h),4U);
+ __store_block((void *)(& g),4U);
+ __store_block((void *)(& f),4U);
+ __full_init((void *)(& f));
f = (float)1.0;
- _full_init((void *)(& g));
+ __full_init((void *)(& g));
g = (float)1.0;
foo(& f,& g,& h);
bar(& f,& g,& h);
__retres = 0;
- _delete_block((void *)(& h));
- _delete_block((void *)(& g));
- _delete_block((void *)(& f));
+ __delete_block((void *)(& h));
+ __delete_block((void *)(& g));
+ __delete_block((void *)(& f));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 0ec0be1ab7c..998753278e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -53,12 +53,12 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _literal_string(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -78,9 +78,9 @@ int main(void)
/*@ assert y ≥ 1; */
e_acsl_assert(y >= 1,(char *)"Assertion",(char *)"y >= 1",12);
__e_acsl_literal_string = "toto";
- _store_block((void *)__e_acsl_literal_string,sizeof("toto"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
+ __store_block((void *)__e_acsl_literal_string,sizeof("toto"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
s = (char *)__e_acsl_literal_string;
/*@ assert s ≡ s; */
e_acsl_assert(s == s,(char *)"Assertion",(char *)"s == s",14);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index e2126928f8e..1fea02cc9ed 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -89,12 +89,12 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _literal_string(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -162,9 +162,9 @@ int main(void)
}
__e_acsl_literal_string = "toto";
- _store_block((void *)__e_acsl_literal_string,sizeof("toto"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
+ __store_block((void *)__e_acsl_literal_string,sizeof("toto"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
s = (char *)__e_acsl_literal_string;
/*@ assert s ≡ s; */
e_acsl_assert(s == s,(char *)"Assertion",(char *)"s == s",14);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index c5298635ab2..3d159d5b0bf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -53,27 +53,27 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _literal_string(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void);
char *T;
@@ -83,7 +83,7 @@ void f(void)
/*@ assert *(T+G) ≡ 'b'; */
{
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)(T + G),sizeof(char));
+ __e_acsl_valid_read = __valid_read((void *)(T + G),sizeof(char));
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",
(char *)"mem_access: \\valid_read(T+G)",0);
e_acsl_assert((int)*(T + G) == 'b',(char *)"Assertion",
@@ -104,31 +104,31 @@ void e_acsl_global_init(void)
char *__e_acsl_literal_string_3;
char *__e_acsl_literal_string_2;
char *__e_acsl_literal_string;
- _store_block((void *)(& S2),4U);
- __e_acsl_literal_string = "bar";
- _store_block((void *)__e_acsl_literal_string,sizeof("bar"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
- __e_acsl_literal_string_2 = "foo";
- _store_block((void *)__e_acsl_literal_string_2,sizeof("foo"));
- _full_init((void *)__e_acsl_literal_string_2);
- _literal_string((void *)__e_acsl_literal_string_2);
- __e_acsl_literal_string_3 = "foo2";
- _store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
- _full_init((void *)__e_acsl_literal_string_3);
- _literal_string((void *)__e_acsl_literal_string_3);
- _full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_3;
- _store_block((void *)(& S),4U);
- _full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_2;
- _store_block((void *)(& G),4U);
- _full_init((void *)(& G));
- _store_block((void *)(& T),4U);
- _full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string;
- _store_block((void *)(& G2),4U);
- _full_init((void *)(& G2));
+ __store_block((void *)(& S),4U);
+ __e_acsl_literal_string = "foo2";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo2"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "bar";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string_3 = "foo";
+ __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string_3);
+ __literal_string((void *)__e_acsl_literal_string_3);
+ __full_init((void *)(& S));
+ S = (char *)__e_acsl_literal_string_3;
+ __store_block((void *)(& G),4U);
+ __full_init((void *)(& G));
+ __store_block((void *)(& T),4U);
+ __full_init((void *)(& T));
+ T = (char *)__e_acsl_literal_string_2;
+ __store_block((void *)(& G2),4U);
+ __full_init((void *)(& G2));
+ __store_block((void *)(& S2),4U);
+ __full_init((void *)(& S2));
+ S2 = (char *)__e_acsl_literal_string;
return;
}
@@ -138,17 +138,17 @@ int main(void)
int __retres;
char *SS;
e_acsl_global_init();
- _store_block((void *)(& SS),4U);
+ __store_block((void *)(& SS),4U);
__e_acsl_literal_string = "ss";
- _store_block((void *)__e_acsl_literal_string,sizeof("ss"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
- _full_init((void *)(& SS));
+ __store_block((void *)__e_acsl_literal_string,sizeof("ss"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __full_init((void *)(& SS));
SS = (char *)__e_acsl_literal_string;
/*@ assert *(S+G2) ≡ 'o'; */
{
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)(S + G2),sizeof(char));
+ __e_acsl_valid_read = __valid_read((void *)(S + G2),sizeof(char));
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",
(char *)"mem_access: \\valid_read(S+G2)",0);
e_acsl_assert((int)*(S + G2) == 'o',(char *)"Assertion",
@@ -158,7 +158,7 @@ int main(void)
/*@ assert \initialized(S); */
{
int __e_acsl_initialized;
- __e_acsl_initialized = _initialized((void *)S,sizeof(char));
+ __e_acsl_initialized = __initialized((void *)S,sizeof(char));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized(S)",25);
}
@@ -166,7 +166,7 @@ int main(void)
/*@ assert \valid_read(S2); */
{
int __e_acsl_valid_read_2;
- __e_acsl_valid_read_2 = _valid_read((void *)S2,sizeof(char));
+ __e_acsl_valid_read_2 = __valid_read((void *)S2,sizeof(char));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"Assertion",
(char *)"\\valid_read(S2)",26);
}
@@ -175,10 +175,10 @@ int main(void)
{
int __e_acsl_initialized_2;
int __e_acsl_and;
- __e_acsl_initialized_2 = _initialized((void *)(& SS),sizeof(char *));
+ __e_acsl_initialized_2 = __initialized((void *)(& SS),sizeof(char *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)SS,sizeof(char));
+ __e_acsl_valid = __valid((void *)SS,sizeof(char));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
@@ -187,12 +187,12 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& G2));
- _delete_block((void *)(& S2));
- _delete_block((void *)(& S));
- _delete_block((void *)(& G));
- _delete_block((void *)(& T));
- _delete_block((void *)(& SS));
+ __delete_block((void *)(& G2));
+ __delete_block((void *)(& S2));
+ __delete_block((void *)(& S));
+ __delete_block((void *)(& G));
+ __delete_block((void *)(& T));
+ __delete_block((void *)(& SS));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index 7dbebcdfd44..dca4b1cccc1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -73,27 +73,27 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _literal_string(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void);
char *T;
@@ -129,31 +129,31 @@ void e_acsl_global_init(void)
char *__e_acsl_literal_string_3;
char *__e_acsl_literal_string_2;
char *__e_acsl_literal_string;
- _store_block((void *)(& S2),4U);
- __e_acsl_literal_string = "bar";
- _store_block((void *)__e_acsl_literal_string,sizeof("bar"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
- __e_acsl_literal_string_2 = "foo";
- _store_block((void *)__e_acsl_literal_string_2,sizeof("foo"));
- _full_init((void *)__e_acsl_literal_string_2);
- _literal_string((void *)__e_acsl_literal_string_2);
- __e_acsl_literal_string_3 = "foo2";
- _store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
- _full_init((void *)__e_acsl_literal_string_3);
- _literal_string((void *)__e_acsl_literal_string_3);
- _full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_3;
- _store_block((void *)(& S),4U);
- _full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_2;
- _store_block((void *)(& G),4U);
- _full_init((void *)(& G));
- _store_block((void *)(& T),4U);
- _full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string;
- _store_block((void *)(& G2),4U);
- _full_init((void *)(& G2));
+ __store_block((void *)(& S),4U);
+ __e_acsl_literal_string = "foo2";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo2"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "bar";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string_3 = "foo";
+ __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string_3);
+ __literal_string((void *)__e_acsl_literal_string_3);
+ __full_init((void *)(& S));
+ S = (char *)__e_acsl_literal_string_3;
+ __store_block((void *)(& G),4U);
+ __full_init((void *)(& G));
+ __store_block((void *)(& T),4U);
+ __full_init((void *)(& T));
+ T = (char *)__e_acsl_literal_string_2;
+ __store_block((void *)(& G2),4U);
+ __full_init((void *)(& G2));
+ __store_block((void *)(& S2),4U);
+ __full_init((void *)(& S2));
+ S2 = (char *)__e_acsl_literal_string;
return;
}
@@ -163,12 +163,12 @@ int main(void)
int __retres;
char *SS;
e_acsl_global_init();
- _store_block((void *)(& SS),4U);
+ __store_block((void *)(& SS),4U);
__e_acsl_literal_string = "ss";
- _store_block((void *)__e_acsl_literal_string,sizeof("ss"));
- _full_init((void *)__e_acsl_literal_string);
- _literal_string((void *)__e_acsl_literal_string);
- _full_init((void *)(& SS));
+ __store_block((void *)__e_acsl_literal_string,sizeof("ss"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __full_init((void *)(& SS));
SS = (char *)__e_acsl_literal_string;
/*@ assert *(S+G2) ≡ 'o'; */
{
@@ -188,7 +188,7 @@ int main(void)
/*@ assert \initialized(S); */
{
int __e_acsl_initialized;
- __e_acsl_initialized = _initialized((void *)S,sizeof(char));
+ __e_acsl_initialized = __initialized((void *)S,sizeof(char));
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized(S)",25);
}
@@ -196,7 +196,7 @@ int main(void)
/*@ assert \valid_read(S2); */
{
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)S2,sizeof(char));
+ __e_acsl_valid_read = __valid_read((void *)S2,sizeof(char));
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",
(char *)"\\valid_read(S2)",26);
}
@@ -205,10 +205,10 @@ int main(void)
{
int __e_acsl_initialized_2;
int __e_acsl_and;
- __e_acsl_initialized_2 = _initialized((void *)(& SS),sizeof(char *));
+ __e_acsl_initialized_2 = __initialized((void *)(& SS),sizeof(char *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)SS,sizeof(char));
+ __e_acsl_valid = __valid((void *)SS,sizeof(char));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
@@ -217,12 +217,12 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& G2));
- _delete_block((void *)(& S2));
- _delete_block((void *)(& S));
- _delete_block((void *)(& G));
- _delete_block((void *)(& T));
- _delete_block((void *)(& SS));
+ __delete_block((void *)(& G2));
+ __delete_block((void *)(& S2));
+ __delete_block((void *)(& S));
+ __delete_block((void *)(& G));
+ __delete_block((void *)(& T));
+ __delete_block((void *)(& SS));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 55a2b13b762..155fc10a7b1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -57,7 +57,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -78,38 +78,38 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
struct list *add(struct list *l, int i)
{
struct list *new;
- _store_block((void *)(& new),4U);
- _full_init((void *)(& new));
- new = (struct list *)_malloc(sizeof(struct list));
+ __store_block((void *)(& new),4U);
+ __full_init((void *)(& new));
+ new = (struct list *)__malloc(sizeof(struct list));
/*@ assert \valid(new); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __e_acsl_initialized = _initialized((void *)(& new),
- sizeof(struct list *));
+ __e_acsl_initialized = __initialized((void *)(& new),
+ sizeof(struct list *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)new,sizeof(struct list));
+ __e_acsl_valid = __valid((void *)new,sizeof(struct list));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
@@ -118,7 +118,7 @@ struct list *add(struct list *l, int i)
new->element = i;
new->next = l;
- _delete_block((void *)(& new));
+ __delete_block((void *)(& new));
return (new);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 55a2b13b762..155fc10a7b1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -57,7 +57,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -78,38 +78,38 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
struct list *add(struct list *l, int i)
{
struct list *new;
- _store_block((void *)(& new),4U);
- _full_init((void *)(& new));
- new = (struct list *)_malloc(sizeof(struct list));
+ __store_block((void *)(& new),4U);
+ __full_init((void *)(& new));
+ new = (struct list *)__malloc(sizeof(struct list));
/*@ assert \valid(new); */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __e_acsl_initialized = _initialized((void *)(& new),
- sizeof(struct list *));
+ __e_acsl_initialized = __initialized((void *)(& new),
+ sizeof(struct list *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)new,sizeof(struct list));
+ __e_acsl_valid = __valid((void *)new,sizeof(struct list));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
@@ -118,7 +118,7 @@ struct list *add(struct list *l, int i)
new->element = i;
new->next = l;
- _delete_block((void *)(& new));
+ __delete_block((void *)(& new));
return (new);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 55a21266abb..350ad96022e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -53,26 +53,26 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -80,27 +80,27 @@ int main(void)
int x;
int t[3];
int *p;
- _store_block((void *)(& p),4U);
- _store_block((void *)(t),12U);
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(t),12U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
x = 1;
- _initialize((void *)(t),sizeof(int));
+ __initialize((void *)(t),sizeof(int));
t[0] = 2;
- _initialize((void *)(& t[1]),sizeof(int));
+ __initialize((void *)(& t[1]),sizeof(int));
t[1] = 3;
- _initialize((void *)(& t[2]),sizeof(int));
+ __initialize((void *)(& t[2]),sizeof(int));
t[2] = 4;
- _full_init((void *)(& p));
+ __full_init((void *)(& p));
p = & x;
/*@ assert *p ≡ 1; */
{
int __e_acsl_initialized;
int __e_acsl_and;
- __e_acsl_initialized = _initialized((void *)(& p),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)p,sizeof(int));
+ __e_acsl_valid_read = __valid_read((void *)p,sizeof(int));
__e_acsl_and = __e_acsl_valid_read;
}
else { __e_acsl_and = 0; }
@@ -118,8 +118,8 @@ int main(void)
(char *)"t[(2*sizeof(int))/sizeof((int)0x0)] == 4",16);
{
int i;
- _store_block((void *)(& i),4U);
- _full_init((void *)(& i));
+ __store_block((void *)(& i),4U);
+ __full_init((void *)(& i));
i = 0;
while (i < 2) {
/*@ assert t[i] ≡ i+2; */
@@ -142,30 +142,31 @@ int main(void)
/*@ assert *(&t[2]-i) ≡ 4-i; */
{
int __e_acsl_valid_read_2;
- __e_acsl_valid_read_2 = _valid_read((void *)(& t[2] - i),sizeof(int));
+ __e_acsl_valid_read_2 = __valid_read((void *)(& t[2] - i),
+ sizeof(int));
e_acsl_assert(__e_acsl_valid_read_2,(char *)"Assertion",
(char *)"mem_access: \\valid_read(&t[2]-i)",0);
e_acsl_assert((long long)*(& t[2] - i) == (long long)4 - (long long)i,
(char *)"Assertion",(char *)"*(&t[2]-i) == 4-i",21);
}
- _full_init((void *)(& i));
+ __full_init((void *)(& i));
i ++;
}
- _delete_block((void *)(& i));
+ __delete_block((void *)(& i));
}
- _full_init((void *)(& p));
+ __full_init((void *)(& p));
p = & t[2];
t[2] = 5;
/*@ assert *p ≡ 5; */
{
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = _initialized((void *)(& p),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& p),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_read_3;
- __e_acsl_valid_read_3 = _valid_read((void *)p,sizeof(int));
+ __e_acsl_valid_read_3 = __valid_read((void *)p,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_read_3;
}
else { __e_acsl_and_2 = 0; }
@@ -175,9 +176,9 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& p));
- _delete_block((void *)(t));
- _delete_block((void *)(& x));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(t));
+ __delete_block((void *)(& x));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index cafacffdd11..a58a8694f9e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -124,15 +124,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -140,18 +140,18 @@ int main(void)
int x;
int t[3];
int *p;
- _store_block((void *)(& p),4U);
- _store_block((void *)(t),12U);
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(t),12U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
x = 1;
- _initialize((void *)(t),sizeof(int));
+ __initialize((void *)(t),sizeof(int));
t[0] = 2;
- _initialize((void *)(& t[1]),sizeof(int));
+ __initialize((void *)(& t[1]),sizeof(int));
t[1] = 3;
- _initialize((void *)(& t[2]),sizeof(int));
+ __initialize((void *)(& t[2]),sizeof(int));
t[2] = 4;
- _full_init((void *)(& p));
+ __full_init((void *)(& p));
p = & x;
/*@ assert *p ≡ 1; */
{
@@ -244,8 +244,8 @@ int main(void)
{
int i;
- _store_block((void *)(& i),4U);
- _full_init((void *)(& i));
+ __store_block((void *)(& i),4U);
+ __full_init((void *)(& i));
i = 0;
while (i < 2) {
/*@ assert t[i] ≡ i+2; */
@@ -327,13 +327,13 @@ int main(void)
__gmpz_clear(__e_acsl_sub_3);
}
- _full_init((void *)(& i));
+ __full_init((void *)(& i));
i ++;
}
- _delete_block((void *)(& i));
+ __delete_block((void *)(& i));
}
- _full_init((void *)(& p));
+ __full_init((void *)(& p));
p = & t[2];
t[2] = 5;
/*@ assert *p ≡ 5; */
@@ -352,9 +352,9 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& p));
- _delete_block((void *)(t));
- _delete_block((void *)(& x));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(t));
+ __delete_block((void *)(& x));
__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 d448f90008a..b2526df20c3 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
@@ -53,7 +53,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ frees p;
assigns __fc_heap_status;
@@ -72,7 +72,7 @@ extern void *_malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
-extern void _free(void *p);
+extern void __free(void *p);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -93,22 +93,22 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int *X;
/*@ requires \valid(x);
@@ -116,21 +116,21 @@ int *X;
int *f(int *x)
{
int *y;
- _store_block((void *)(& y),4U);
+ __store_block((void *)(& y),4U);
/*@ assert ¬\valid(y); */
{
int __e_acsl_valid;
int __e_acsl_initialized;
int __e_acsl_and;
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
- __e_acsl_valid = _valid((void *)x,sizeof(int));
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
+ __e_acsl_valid = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"\\valid(x)",
15);
- __e_acsl_initialized = _initialized((void *)(& y),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)y,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid_2;
}
else { __e_acsl_and = 0; }
@@ -138,23 +138,23 @@ int *f(int *x)
19);
}
- _full_init((void *)(& y));
+ __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)x,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"\\valid(x)",
21);
}
{
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)y,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)y,sizeof(int));
e_acsl_assert(__e_acsl_valid_4,(char *)"Postcondition",
(char *)"\\valid(\\result)",16);
- _delete_block((void *)(& x));
- _delete_block((void *)(& y));
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
return (y);
}
@@ -162,8 +162,8 @@ int *f(int *x)
void e_acsl_global_init(void)
{
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ __store_block((void *)(& X),4U);
+ __full_init((void *)(& X));
return;
}
@@ -174,10 +174,10 @@ int main(void)
int *b;
int n;
e_acsl_global_init();
- _store_block((void *)(& n),4U);
- _store_block((void *)(& b),4U);
- _store_block((void *)(& a),4U);
- _full_init((void *)(& n));
+ __store_block((void *)(& n),4U);
+ __store_block((void *)(& b),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
@@ -185,20 +185,20 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else { __e_acsl_and_2 = 0; }
@@ -207,7 +207,7 @@ int main(void)
else { __e_acsl_and_3 = 0; }
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else { __e_acsl_and_4 = 0; }
@@ -215,28 +215,28 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",27);
}
- _full_init((void *)(& a));
- a = (int *)_malloc(sizeof(int));
+ __full_init((void *)(& a));
+ a = (int *)__malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else { __e_acsl_and_5 = 0; }
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else { __e_acsl_and_6 = 0; }
@@ -245,7 +245,7 @@ int main(void)
else { __e_acsl_and_7 = 0; }
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else { __e_acsl_and_8 = 0; }
@@ -253,7 +253,7 @@ int main(void)
(char *)"(\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",29);
}
- _full_init((void *)(& X));
+ __full_init((void *)(& X));
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
{
@@ -261,20 +261,20 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else { __e_acsl_and_9 = 0; }
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else { __e_acsl_and_10 = 0; }
@@ -283,7 +283,7 @@ int main(void)
else { __e_acsl_and_11 = 0; }
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else { __e_acsl_and_12 = 0; }
@@ -291,7 +291,7 @@ int main(void)
(char *)"(\\valid(a) && !\\valid(b)) &&\n\\valid(X)",31);
}
- _full_init((void *)(& b));
+ __full_init((void *)(& b));
b = f(& n);
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -299,20 +299,20 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else { __e_acsl_and_13 = 0; }
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else { __e_acsl_and_14 = 0; }
@@ -321,7 +321,7 @@ int main(void)
else { __e_acsl_and_15 = 0; }
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else { __e_acsl_and_16 = 0; }
@@ -329,7 +329,7 @@ int main(void)
(char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",33);
}
- _full_init((void *)(& X));
+ __full_init((void *)(& X));
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -337,20 +337,20 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else { __e_acsl_and_17 = 0; }
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else { __e_acsl_and_18 = 0; }
@@ -359,7 +359,7 @@ int main(void)
else { __e_acsl_and_19 = 0; }
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else { __e_acsl_and_20 = 0; }
@@ -367,27 +367,27 @@ int main(void)
(char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",35);
}
- _free((void *)a);
+ __free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
int __e_acsl_initialized_11;
int __e_acsl_and_21;
int __e_acsl_and_23;
int __e_acsl_and_24;
- __e_acsl_initialized_11 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_11 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_11) {
int __e_acsl_valid_16;
- __e_acsl_valid_16 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_16 = __valid((void *)a,sizeof(int));
__e_acsl_and_21 = __e_acsl_valid_16;
}
else { __e_acsl_and_21 = 0; }
if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
int __e_acsl_and_22;
- __e_acsl_initialized_12 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_12 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_12) {
int __e_acsl_valid_17;
- __e_acsl_valid_17 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_17 = __valid((void *)b,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_17;
}
else { __e_acsl_and_22 = 0; }
@@ -396,7 +396,7 @@ int main(void)
else { __e_acsl_and_23 = 0; }
if (__e_acsl_and_23) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_18 = __valid((void *)X,sizeof(int));
__e_acsl_and_24 = __e_acsl_valid_18;
}
else { __e_acsl_and_24 = 0; }
@@ -405,10 +405,10 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& X));
- _delete_block((void *)(& n));
- _delete_block((void *)(& b));
- _delete_block((void *)(& a));
+ __delete_block((void *)(& X));
+ __delete_block((void *)(& n));
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
__clean();
return (__retres);
}
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 d448f90008a..b2526df20c3 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
@@ -53,7 +53,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ frees p;
assigns __fc_heap_status;
@@ -72,7 +72,7 @@ extern void *_malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
-extern void _free(void *p);
+extern void __free(void *p);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -93,22 +93,22 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int *X;
/*@ requires \valid(x);
@@ -116,21 +116,21 @@ int *X;
int *f(int *x)
{
int *y;
- _store_block((void *)(& y),4U);
+ __store_block((void *)(& y),4U);
/*@ assert ¬\valid(y); */
{
int __e_acsl_valid;
int __e_acsl_initialized;
int __e_acsl_and;
- _store_block((void *)(& x),4U);
- _full_init((void *)(& x));
- __e_acsl_valid = _valid((void *)x,sizeof(int));
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
+ __e_acsl_valid = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"\\valid(x)",
15);
- __e_acsl_initialized = _initialized((void *)(& y),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& y),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)y,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid_2;
}
else { __e_acsl_and = 0; }
@@ -138,23 +138,23 @@ int *f(int *x)
19);
}
- _full_init((void *)(& y));
+ __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)x,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)x,sizeof(int));
e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"\\valid(x)",
21);
}
{
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)y,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)y,sizeof(int));
e_acsl_assert(__e_acsl_valid_4,(char *)"Postcondition",
(char *)"\\valid(\\result)",16);
- _delete_block((void *)(& x));
- _delete_block((void *)(& y));
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
return (y);
}
@@ -162,8 +162,8 @@ int *f(int *x)
void e_acsl_global_init(void)
{
- _store_block((void *)(& X),4U);
- _full_init((void *)(& X));
+ __store_block((void *)(& X),4U);
+ __full_init((void *)(& X));
return;
}
@@ -174,10 +174,10 @@ int main(void)
int *b;
int n;
e_acsl_global_init();
- _store_block((void *)(& n),4U);
- _store_block((void *)(& b),4U);
- _store_block((void *)(& a),4U);
- _full_init((void *)(& n));
+ __store_block((void *)(& n),4U);
+ __store_block((void *)(& b),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& n));
n = 0;
/*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
@@ -185,20 +185,20 @@ int main(void)
int __e_acsl_and;
int __e_acsl_and_3;
int __e_acsl_and_4;
- __e_acsl_initialized = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else { __e_acsl_and_2 = 0; }
@@ -207,7 +207,7 @@ int main(void)
else { __e_acsl_and_3 = 0; }
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
else { __e_acsl_and_4 = 0; }
@@ -215,28 +215,28 @@ int main(void)
(char *)"(!\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",27);
}
- _full_init((void *)(& a));
- a = (int *)_malloc(sizeof(int));
+ __full_init((void *)(& a));
+ a = (int *)__malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
int __e_acsl_and_7;
int __e_acsl_and_8;
- __e_acsl_initialized_3 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else { __e_acsl_and_5 = 0; }
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
- __e_acsl_initialized_4 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
else { __e_acsl_and_6 = 0; }
@@ -245,7 +245,7 @@ int main(void)
else { __e_acsl_and_7 = 0; }
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
else { __e_acsl_and_8 = 0; }
@@ -253,7 +253,7 @@ int main(void)
(char *)"(\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",29);
}
- _full_init((void *)(& X));
+ __full_init((void *)(& X));
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
{
@@ -261,20 +261,20 @@ int main(void)
int __e_acsl_and_9;
int __e_acsl_and_11;
int __e_acsl_and_12;
- __e_acsl_initialized_5 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_7;
- __e_acsl_valid_7 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
else { __e_acsl_and_9 = 0; }
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_8;
- __e_acsl_valid_8 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
else { __e_acsl_and_10 = 0; }
@@ -283,7 +283,7 @@ int main(void)
else { __e_acsl_and_11 = 0; }
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
- __e_acsl_valid_9 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
else { __e_acsl_and_12 = 0; }
@@ -291,7 +291,7 @@ int main(void)
(char *)"(\\valid(a) && !\\valid(b)) &&\n\\valid(X)",31);
}
- _full_init((void *)(& b));
+ __full_init((void *)(& b));
b = f(& n);
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -299,20 +299,20 @@ int main(void)
int __e_acsl_and_13;
int __e_acsl_and_15;
int __e_acsl_and_16;
- __e_acsl_initialized_7 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_10;
- __e_acsl_valid_10 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
else { __e_acsl_and_13 = 0; }
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
- __e_acsl_initialized_8 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_8 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_8) {
int __e_acsl_valid_11;
- __e_acsl_valid_11 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
else { __e_acsl_and_14 = 0; }
@@ -321,7 +321,7 @@ int main(void)
else { __e_acsl_and_15 = 0; }
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
- __e_acsl_valid_12 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
else { __e_acsl_and_16 = 0; }
@@ -329,7 +329,7 @@ int main(void)
(char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",33);
}
- _full_init((void *)(& X));
+ __full_init((void *)(& X));
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -337,20 +337,20 @@ int main(void)
int __e_acsl_and_17;
int __e_acsl_and_19;
int __e_acsl_and_20;
- __e_acsl_initialized_9 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_9 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_9) {
int __e_acsl_valid_13;
- __e_acsl_valid_13 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
else { __e_acsl_and_17 = 0; }
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
- __e_acsl_initialized_10 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_10 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_10) {
int __e_acsl_valid_14;
- __e_acsl_valid_14 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
else { __e_acsl_and_18 = 0; }
@@ -359,7 +359,7 @@ int main(void)
else { __e_acsl_and_19 = 0; }
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
- __e_acsl_valid_15 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
else { __e_acsl_and_20 = 0; }
@@ -367,27 +367,27 @@ int main(void)
(char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",35);
}
- _free((void *)a);
+ __free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
int __e_acsl_initialized_11;
int __e_acsl_and_21;
int __e_acsl_and_23;
int __e_acsl_and_24;
- __e_acsl_initialized_11 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_11 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_11) {
int __e_acsl_valid_16;
- __e_acsl_valid_16 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_16 = __valid((void *)a,sizeof(int));
__e_acsl_and_21 = __e_acsl_valid_16;
}
else { __e_acsl_and_21 = 0; }
if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
int __e_acsl_and_22;
- __e_acsl_initialized_12 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_12 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_12) {
int __e_acsl_valid_17;
- __e_acsl_valid_17 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_17 = __valid((void *)b,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_17;
}
else { __e_acsl_and_22 = 0; }
@@ -396,7 +396,7 @@ int main(void)
else { __e_acsl_and_23 = 0; }
if (__e_acsl_and_23) {
int __e_acsl_valid_18;
- __e_acsl_valid_18 = _valid((void *)X,sizeof(int));
+ __e_acsl_valid_18 = __valid((void *)X,sizeof(int));
__e_acsl_and_24 = __e_acsl_valid_18;
}
else { __e_acsl_and_24 = 0; }
@@ -405,10 +405,10 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& X));
- _delete_block((void *)(& n));
- _delete_block((void *)(& b));
- _delete_block((void *)(& a));
+ __delete_block((void *)(& X));
+ __delete_block((void *)(& n));
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
__clean();
return (__retres);
}
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 1e438a21df5..bd2c5f40514 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
@@ -53,7 +53,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ frees p;
assigns __fc_heap_status;
@@ -72,7 +72,7 @@ extern void *_malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
-extern void _free(void *p);
+extern void __free(void *p);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -93,28 +93,28 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid_read(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -122,30 +122,30 @@ int main(void)
int *a;
int *b;
int n;
- _store_block((void *)(& n),4U);
- _store_block((void *)(& b),4U);
- _store_block((void *)(& a),4U);
- _full_init((void *)(& n));
+ __store_block((void *)(& n),4U);
+ __store_block((void *)(& b),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& n));
n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
int __e_acsl_initialized;
int __e_acsl_and;
int __e_acsl_and_3;
- __e_acsl_initialized = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else { __e_acsl_and_2 = 0; }
@@ -156,31 +156,31 @@ int main(void)
(char *)"!\\valid(a) &&\n!\\valid(b)",12);
}
- _full_init((void *)(& a));
- a = (int *)_malloc(sizeof(int));
- _initialize((void *)a,sizeof(int));
+ __full_init((void *)(& a));
+ a = (int *)__malloc(sizeof(int));
+ __initialize((void *)a,sizeof(int));
*a = n;
- _full_init((void *)(& b));
+ __full_init((void *)(& b));
b = a;
/*@ assert \valid(a) ∧ \valid(b); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_4;
int __e_acsl_and_6;
- __e_acsl_initialized_3 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)a,sizeof(int));
__e_acsl_and_4 = __e_acsl_valid_3;
}
else { __e_acsl_and_4 = 0; }
if (__e_acsl_and_4) {
int __e_acsl_initialized_4;
int __e_acsl_and_5;
- __e_acsl_initialized_4 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)b,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else { __e_acsl_and_5 = 0; }
@@ -195,10 +195,10 @@ int main(void)
{
int __e_acsl_initialized_5;
int __e_acsl_and_7;
- __e_acsl_initialized_5 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_read;
- __e_acsl_valid_read = _valid_read((void *)b,sizeof(int));
+ __e_acsl_valid_read = __valid_read((void *)b,sizeof(int));
__e_acsl_and_7 = __e_acsl_valid_read;
}
else { __e_acsl_and_7 = 0; }
@@ -207,26 +207,26 @@ int main(void)
e_acsl_assert(*b == n,(char *)"Assertion",(char *)"*b == n",17);
}
- _free((void *)b);
+ __free((void *)b);
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
int __e_acsl_initialized_6;
int __e_acsl_and_8;
int __e_acsl_and_10;
- __e_acsl_initialized_6 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)a,sizeof(int));
__e_acsl_and_8 = __e_acsl_valid_5;
}
else { __e_acsl_and_8 = 0; }
if (! __e_acsl_and_8) {
int __e_acsl_initialized_7;
int __e_acsl_and_9;
- __e_acsl_initialized_7 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_7 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_7) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)b,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_6;
}
else { __e_acsl_and_9 = 0; }
@@ -238,9 +238,9 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& n));
- _delete_block((void *)(& b));
- _delete_block((void *)(& a));
+ __delete_block((void *)(& n));
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
__clean();
return (__retres);
}
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 7f94c1e0039..abafc070936 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
@@ -73,7 +73,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
-extern void *_malloc(size_t size);
+extern void *__malloc(size_t size);
/*@ frees p;
assigns __fc_heap_status;
@@ -92,7 +92,7 @@ extern void *_malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
-extern void _free(void *p);
+extern void __free(void *p);
/*@ ensures \false;
assigns \nothing; */
extern void exit(int status);
@@ -113,25 +113,25 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void *_store_block(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _delete_block(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _initialize(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) void _full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
{
@@ -139,30 +139,30 @@ int main(void)
int *a;
int *b;
int n;
- _store_block((void *)(& n),4U);
- _store_block((void *)(& b),4U);
- _store_block((void *)(& a),4U);
- _full_init((void *)(& n));
+ __store_block((void *)(& n),4U);
+ __store_block((void *)(& b),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& n));
n = 0;
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
int __e_acsl_initialized;
int __e_acsl_and;
int __e_acsl_and_3;
- __e_acsl_initialized = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
- __e_acsl_valid = _valid((void *)a,sizeof(int));
+ __e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else { __e_acsl_and = 0; }
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
- __e_acsl_initialized_2 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_2 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_2) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
else { __e_acsl_and_2 = 0; }
@@ -173,31 +173,31 @@ int main(void)
(char *)"!\\valid(a) &&\n!\\valid(b)",12);
}
- _full_init((void *)(& a));
- a = (int *)_malloc(sizeof(int));
- _initialize((void *)a,sizeof(int));
+ __full_init((void *)(& a));
+ a = (int *)__malloc(sizeof(int));
+ __initialize((void *)a,sizeof(int));
*a = n;
- _full_init((void *)(& b));
+ __full_init((void *)(& b));
b = a;
/*@ assert \valid(a) ∧ \valid(b); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_4;
int __e_acsl_and_6;
- __e_acsl_initialized_3 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_3) {
int __e_acsl_valid_3;
- __e_acsl_valid_3 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_3 = __valid((void *)a,sizeof(int));
__e_acsl_and_4 = __e_acsl_valid_3;
}
else { __e_acsl_and_4 = 0; }
if (__e_acsl_and_4) {
int __e_acsl_initialized_4;
int __e_acsl_and_5;
- __e_acsl_initialized_4 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_4) {
int __e_acsl_valid_4;
- __e_acsl_valid_4 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_4 = __valid((void *)b,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
else { __e_acsl_and_5 = 0; }
@@ -222,26 +222,26 @@ int main(void)
__gmpz_clear(__e_acsl_n);
}
- _free((void *)b);
+ __free((void *)b);
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
int __e_acsl_initialized_5;
int __e_acsl_and_7;
int __e_acsl_and_9;
- __e_acsl_initialized_5 = _initialized((void *)(& a),sizeof(int *));
+ __e_acsl_initialized_5 = __initialized((void *)(& a),sizeof(int *));
if (__e_acsl_initialized_5) {
int __e_acsl_valid_5;
- __e_acsl_valid_5 = _valid((void *)a,sizeof(int));
+ __e_acsl_valid_5 = __valid((void *)a,sizeof(int));
__e_acsl_and_7 = __e_acsl_valid_5;
}
else { __e_acsl_and_7 = 0; }
if (! __e_acsl_and_7) {
int __e_acsl_initialized_6;
int __e_acsl_and_8;
- __e_acsl_initialized_6 = _initialized((void *)(& b),sizeof(int *));
+ __e_acsl_initialized_6 = __initialized((void *)(& b),sizeof(int *));
if (__e_acsl_initialized_6) {
int __e_acsl_valid_6;
- __e_acsl_valid_6 = _valid((void *)b,sizeof(int));
+ __e_acsl_valid_6 = __valid((void *)b,sizeof(int));
__e_acsl_and_8 = __e_acsl_valid_6;
}
else { __e_acsl_and_8 = 0; }
@@ -253,9 +253,9 @@ int main(void)
}
__retres = 0;
- _delete_block((void *)(& n));
- _delete_block((void *)(& b));
- _delete_block((void *)(& a));
+ __delete_block((void *)(& n));
+ __delete_block((void *)(& b));
+ __delete_block((void *)(& a));
__clean();
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 298076cb9f6..ebd76810a39 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -57,15 +57,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior B1:
assumes l ≡ \null;
@@ -89,15 +89,15 @@ struct list *f(struct list *l)
{
int __e_acsl_valid;
int __e_acsl_and_2;
- __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_valid = __valid((void *)l,sizeof(struct list));
if (! __e_acsl_valid) {
int __e_acsl_initialized;
int __e_acsl_and;
- __e_acsl_initialized = _initialized((void *)(& l->next),
- sizeof(struct list *));
+ __e_acsl_initialized = __initialized((void *)(& l->next),
+ sizeof(struct list *));
if (__e_acsl_initialized) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)l->next,sizeof(struct list));
+ __e_acsl_valid_2 = __valid((void *)l->next,sizeof(struct list));
__e_acsl_and = __e_acsl_valid_2;
}
else { __e_acsl_and = 0; }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 298076cb9f6..ebd76810a39 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -57,15 +57,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
/*@ assigns \nothing; */
-extern __attribute__((__FC_BUILTIN__)) int _valid(void *ptr, size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒
\initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
*/
-extern __attribute__((__FC_BUILTIN__)) int _initialized(void *ptr,
- size_t size);
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior B1:
assumes l ≡ \null;
@@ -89,15 +89,15 @@ struct list *f(struct list *l)
{
int __e_acsl_valid;
int __e_acsl_and_2;
- __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_valid = __valid((void *)l,sizeof(struct list));
if (! __e_acsl_valid) {
int __e_acsl_initialized;
int __e_acsl_and;
- __e_acsl_initialized = _initialized((void *)(& l->next),
- sizeof(struct list *));
+ __e_acsl_initialized = __initialized((void *)(& l->next),
+ sizeof(struct list *));
if (__e_acsl_initialized) {
int __e_acsl_valid_2;
- __e_acsl_valid_2 = _valid((void *)l->next,sizeof(struct list));
+ __e_acsl_valid_2 = __valid((void *)l->next,sizeof(struct list));
__e_acsl_and = __e_acsl_valid_2;
}
else { __e_acsl_and = 0; }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index e4d8cf7fae6..a9a18b8eceb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -32,9 +32,9 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _literal_string
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
@@ -47,17 +47,17 @@ tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_clear
./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __valid_read
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
-[value] using specification for function _valid
-[value] using specification for function _delete_block
+[value] using specification for function __valid
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 0fffee74141..f487f529243 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -32,24 +32,24 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _literal_string
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __valid_read
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
-[value] using specification for function _valid
-[value] using specification for function _delete_block
+[value] using specification for function __valid
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index ce097ddfef0..f983b03d7d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -26,18 +26,18 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index ce097ddfef0..f983b03d7d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -26,18 +26,18 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 265e11d2f7b..73e028b813b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -27,9 +27,9 @@ tests/e-acsl-runtime/ptr.i:20:[e-acsl] warning: missing guard for ensuring that
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _initialize
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
@@ -75,7 +75,7 @@ tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid.
tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown.
tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index bcdd7327c88..cc723a7f6d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -25,14 +25,14 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
-[value] using specification for function _initialize
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid_read
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
@@ -48,7 +48,7 @@ tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid.
tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown.
tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
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 710bbf3c59d..ed68c68c714 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
@@ -27,12 +27,12 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of function call expression argument
@@ -41,10 +41,10 @@ tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-v
tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of function call expression argument
(void *)b
-[value] using specification for function _valid
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
tests/e-acsl-runtime/valid.c:29:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:29:[value] Non-termination in evaluation of function call expression argument
@@ -65,7 +65,7 @@ tests/e-acsl-runtime/valid.c:19:[value] Non-termination in evaluation of functio
(void *)y
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
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 710bbf3c59d..ed68c68c714 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
@@ -27,12 +27,12 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of function call expression argument
@@ -41,10 +41,10 @@ tests/e-acsl-runtime/valid.c:27:[kernel] warning: accessing uninitialized left-v
tests/e-acsl-runtime/valid.c:27:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of function call expression argument
(void *)b
-[value] using specification for function _valid
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
tests/e-acsl-runtime/valid.c:29:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid.c:29:[value] Non-termination in evaluation of function call expression argument
@@ -65,7 +65,7 @@ tests/e-acsl-runtime/valid.c:19:[value] Non-termination in evaluation of functio
(void *)y
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
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 0f54dc48630..441409292a7 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
@@ -26,12 +26,12 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of function call expression argument
@@ -41,16 +41,16 @@ tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate
tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of function call expression argument
(void *)b
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
-[value] using specification for function _initialize
+[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
-[value] using specification for function _valid_read
+[value] using specification for function __valid_read
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 a that contains escaping addresses; assert(Ook)
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
@@ -60,7 +60,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value b t
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid_alias.c:19:[value] Non-termination in evaluation of function call expression argument
(void *)b
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
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 d30b74e5ce3..94a331edd26 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
@@ -26,12 +26,12 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _store_block
-[value] using specification for function _full_init
+[value] using specification for function __store_block
+[value] using specification for function __full_init
tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of function call expression argument
@@ -41,10 +41,10 @@ tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate
tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of function call expression argument
(void *)b
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
-[value] using specification for function _initialize
+[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status valid.
-[value] using specification for function _valid
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function __valid
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function printf
[value] using specification for function exit
@@ -68,7 +68,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value b t
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid_alias.c:19:[value] Non-termination in evaluation of function call expression argument
(void *)b
-[value] using specification for function _delete_block
+[value] using specification for function __delete_block
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 8a128db8614..54c1424c327 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -26,10 +26,10 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _valid
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __valid
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluation of function call expression argument
(void *)l->next
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 8a128db8614..54c1424c327 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -26,10 +26,10 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function _valid
-[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function _initialized: postcondition got status unknown.
+[value] using specification for function __valid
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluation of function call expression argument
(void *)l->next
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index c74dc7aff5c..1571c0b8a46 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \valid
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_valid.c BIN gen_valid.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
index 00b6add3803..169d1377861 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \valid in presence of aliasing
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_valid_alias.c BIN gen_valid_alias.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias.c > /dev/null && ./gcc_test.sh valid_alias
EXECNOW: LOG gen_valid_alias2.c BIN gen_valid_alias2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias2.c > /dev/null && ./gcc_test.sh valid_alias2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
index 63c607d1e83..dd9f7243e28 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: function contract involving \valid
- STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free"
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_test.sh valid_in_contract
EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_test.sh valid_in_contract2
*/
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 6e038a9cebc..28014734685 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -329,8 +329,7 @@ and context_insensitive_term_to_exp env t =
mmodel_call ~loc "base_addr" Cil.voidPtrType env t
| Tbase_addr _ -> Error.not_yet "labeled \\base_addr"
| Toffset(LogicLabel(_, label), t) when label = "Here" ->
- let e, env = mmodel_call_with_size ~loc "offset" Cil.intType env t in
- e, env, false, "offset"
+ mmodel_call ~loc "offset" Cil.intType env t
| Toffset _ -> Error.not_yet "labeled \\offset"
| Tblock_length(LogicLabel(_, label), t) when label = "Here" ->
mmodel_call ~loc "block_length" Cil.ulongType env t
@@ -404,7 +403,8 @@ and mmodel_call ~loc name ctx env t =
env
None
ctx
- (fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) ("_" ^ name) [ e ] ])
+ (fun v _ ->
+ [ Misc.mk_call ~loc ~result:(Cil.var v) ("__" ^ name) [ e ] ])
in
res, env, false, name
@@ -424,7 +424,7 @@ and mmodel_call_with_size ~loc name ctx env t =
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
in
- [ Misc.mk_call ~loc ~result:(Cil.var v) ("_" ^ name) [ e; sizeof ] ])
+ [ Misc.mk_call ~loc ~result:(Cil.var v) ("__" ^ name) [ e; sizeof ] ])
in
res, env
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 769b53a53ec..8424e6b55ae 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -62,7 +62,7 @@ let rename_alloc_function stmt =
match stmt.skind with
| Instr(Call(_, { enode = Lval(Var vi, _) }, _, _))
when is_alloc_name vi.vname ->
- vi.vname <- "_" ^ vi.vname;
+ vi.vname <- "__" ^ vi.vname;
Misc.mk_debug_mmodel_stmt stmt
|_ ->
stmt
--
GitLab