Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
fd4ff9dd
Commit
fd4ff9dd
authored
9 years ago
by
Kostyantyn Vorobyov
Browse files
Options
Downloads
Patches
Plain Diff
Rebase
parent
04a524ca
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
+7
-23
7 additions, 23 deletions
...lugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
with
7 additions
and
23 deletions
src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
+
7
−
23
View file @
fd4ff9dd
...
@@ -355,34 +355,19 @@ static struct _block * get_cont (void * ptr) {
...
@@ -355,34 +355,19 @@ static struct _block * get_cont (void * ptr) {
struct
bittree
*
tmp
=
__root
;
struct
bittree
*
tmp
=
__root
;
if
(
__root
==
NULL
||
ptr
==
NULL
)
return
NULL
;
if
(
__root
==
NULL
||
ptr
==
NULL
)
return
NULL
;
struct
bittree
*
t
[
WORDBITS
];
struct
bittree
*
other_choice
=
NULL
;
short
ind
=
-
1
;
while
(
1
)
{
while
(
1
)
{
if
(
tmp
->
is_leaf
)
{
if
(
tmp
->
is_leaf
)
{
/* tmp cannot contain ptr because its begin addr is higher */
/* tmp cannot contain ptr because its begin addr is higher */
if
(
tmp
->
addr
>
(
size_t
)
ptr
)
{
if
(
tmp
->
addr
>
(
size_t
)
ptr
)
return
NULL
;
if
(
ind
==
-
1
)
return
NULL
;
else
{
tmp
=
t
[
ind
];
ind
--
;
continue
;
}
}
/* tmp->addr <= ptr, tmp may contain ptr
/* tmp->addr <= ptr, tmp may contain ptr
ptr is contained if tmp is large enough (begin addr + size) */
ptr is contained if tmp is large enough (begin addr + size) */
else
if
((
size_t
)
ptr
<
tmp
->
leaf
->
size
+
tmp
->
addr
else
if
((
size_t
)
ptr
<
tmp
->
leaf
->
size
+
tmp
->
addr
||
(
tmp
->
leaf
->
size
==
0
&&
(
size_t
)
ptr
==
tmp
->
leaf
->
ptr
))
||
(
tmp
->
leaf
->
size
==
0
&&
(
size_t
)
ptr
==
tmp
->
leaf
->
ptr
))
return
tmp
->
leaf
;
return
tmp
->
leaf
;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
/* tmp->addr <= ptr, but tmp->addr is not large enough */
else
if
(
ind
==
-
1
)
else
return
NULL
;
return
NULL
;
else
{
tmp
=
t
[
ind
];
ind
--
;
continue
;
}
}
}
assert
(
tmp
->
left
!=
NULL
&&
tmp
->
right
!=
NULL
);
assert
(
tmp
->
left
!=
NULL
&&
tmp
->
right
!=
NULL
);
...
@@ -390,19 +375,18 @@ static struct _block * get_cont (void * ptr) {
...
@@ -390,19 +375,18 @@ static struct _block * get_cont (void * ptr) {
/* the right child has the highest address, so we test it first */
/* the right child has the highest address, so we test it first */
if
(((
size_t
)
tmp
->
right
->
addr
&
tmp
->
right
->
mask
)
if
(((
size_t
)
tmp
->
right
->
addr
&
tmp
->
right
->
mask
)
<=
((
size_t
)
ptr
&
tmp
->
right
->
mask
))
{
<=
((
size_t
)
ptr
&
tmp
->
right
->
mask
))
{
ind
++
;
other_choice
=
tmp
->
left
;
t
[
ind
]
=
tmp
->
left
;
tmp
=
tmp
->
right
;
tmp
=
tmp
->
right
;
}
}
else
if
(((
size_t
)
tmp
->
left
->
addr
&
tmp
->
left
->
mask
)
else
if
(((
size_t
)
tmp
->
left
->
addr
&
tmp
->
left
->
mask
)
<=
((
size_t
)
ptr
&
tmp
->
left
->
mask
))
<=
((
size_t
)
ptr
&
tmp
->
left
->
mask
))
tmp
=
tmp
->
left
;
tmp
=
tmp
->
left
;
else
{
else
{
if
(
ind
==
-
1
)
if
(
other_choice
==
NULL
)
return
NULL
;
return
NULL
;
else
{
else
{
tmp
=
t
[
ind
]
;
tmp
=
other_choice
;
ind
--
;
other_choice
=
NULL
;
}
}
}
}
}
}
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment