Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
4774cd29
Commit
4774cd29
authored
Oct 15, 2020
by
Basile Desloges
Browse files
[eacsl] Fix bittree model compilation
parent
159bca76
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
View file @
4774cd29
...
...
@@ -26,6 +26,7 @@
***************************************************************************/
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "e_acsl_bittree.h"
...
...
@@ -160,7 +161,7 @@ static bt_node * bt_get_leaf_from_block (bt_block * ptr) {
==
(
ptr
->
ptr
&
curr
->
left
->
mask
))
curr
=
curr
->
left
;
else
v
assert
(
0
,
"Unreachable"
,
NULL
);
private_
assert
(
0
,
"Unreachable"
,
NULL
);
}
DASSERT
(
curr
->
is_leaf
);
DASSERT
(
curr
->
leaf
==
ptr
);
...
...
src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
View file @
4774cd29
...
...
@@ -31,7 +31,7 @@
#include "../../internals/e_acsl_private_assert.h"
#include "../../instrumentation_model/e_acsl_temporal.h"
#include "../../numerical_model/e_acsl_floating_point.h"
#include "../internals/e_acsl_safe_locations.h"
"
#include "../internals/e_acsl_safe_locations.h"
#include "e_acsl_bittree.h"
#include "../e_acsl_observation_model.h"
...
...
@@ -231,12 +231,12 @@ int eacsl_valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
bt_block
*
blk
=
lookup_allocated
(
ptr
,
size
,
ptr_base
);
return
size
==
0
||
||
(
blk
!=
NULL
&&
!
blk
->
is_readonly
#ifdef E_ACSL_TEMPORAL
&&
temporal_valid
(
ptr_base
,
addrof_base
)
#endif
;
)
;
}
/* return whether the size bytes of ptr are readable */
...
...
@@ -244,12 +244,12 @@ int eacsl_valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base)
bt_block
*
blk
=
lookup_allocated
(
ptr
,
size
,
ptr_base
);
return
size
==
0
||
||
(
blk
!=
NULL
#ifdef E_ACSL_TEMPORAL
&&
temporal_valid
(
ptr_base
,
addrof_base
)
#endif
;
)
;
}
/* return the base address of the block containing ptr */
...
...
@@ -260,7 +260,7 @@ void* eacsl_base_addr(void* ptr) {
}
/* return the offset of `ptr` within its block */
size_t
offset
(
void
*
ptr
)
{
size_t
eacsl_
offset
(
void
*
ptr
)
{
bt_block
*
tmp
=
bt_find
(
ptr
);
private_assert
(
tmp
!=
NULL
,
"
\\
offset of unallocated memory"
,
NULL
);
return
((
uintptr_t
)
ptr
-
tmp
->
ptr
);
...
...
@@ -585,7 +585,7 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
/* Tracking safe locations */
collect_safe_locations
();
int
i
;
for
(
i
=
0
;
i
<
get_safe_location_count
();
i
++
)
{
for
(
i
=
0
;
i
<
get_safe_location
s
_count
();
i
++
)
{
memory_location
*
loc
=
get_safe_location
(
i
);
void
*
addr
=
(
void
*
)
loc
->
address
;
uintptr_t
len
=
loc
->
length
;
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment