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
5aaf0a6a
Commit
5aaf0a6a
authored
9 years ago
by
Kostyantyn Vorobyov
Browse files
Options
Downloads
Patches
Plain Diff
[RTL] Reworked macros in e_acsl_bits.h header to be faster
parent
5193f454
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+4
-4
4 additions, 4 deletions
...lugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
+42
-72
42 additions, 72 deletions
src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
with
46 additions
and
76 deletions
src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+
4
−
4
View file @
5aaf0a6a
...
...
@@ -173,7 +173,7 @@ void* __realloc(void* ptr, size_t size) {
/* Allocate memory to store partial initialization */
tmp
->
init_ptr
=
native_calloc
(
1
,
nb
);
/* Carry out initialization of the old block */
bitwise_memset
(
tmp
->
init_ptr
,
tmp
->
size
,
1
,
0
);
setbits
(
tmp
->
init_ptr
,
tmp
->
size
);
}
}
/* contains initialized and uninitialized parts */
...
...
@@ -256,8 +256,8 @@ void __initialize (void * ptr, size_t size) {
/* bit-offset within the above byte, i.e., bit to be toggled */
int
bit
=
offset
%
8
;
if
(
!
bit
check
(
bit
,
tmp
->
init_ptr
[
byte
]))
{
/* if bit is unset ... */
bitse
t
(
bit
,
tmp
->
init_ptr
[
byte
]);
/* ... set the bit ... */
if
(
!
check
bit
(
bit
,
tmp
->
init_ptr
[
byte
]))
{
/* if bit is unset ... */
setbi
t
(
bit
,
tmp
->
init_ptr
[
byte
]);
/* ... set the bit ... */
tmp
->
init_cpt
++
;
/* ... and increment initialized bytes count */
}
}
...
...
@@ -317,7 +317,7 @@ int __initialized (void * ptr, size_t size) {
size_t
offset
=
(
uintptr_t
)
ptr
-
tmp
->
ptr
+
i
;
int
byte
=
offset
/
8
;
int
bit
=
offset
%
8
;
if
(
!
bit
check
(
bit
,
tmp
->
init_ptr
[
byte
]))
if
(
!
check
bit
(
bit
,
tmp
->
init_ptr
[
byte
]))
return
false
;
}
return
true
;
...
...
This diff is collapsed.
Click to expand it.
src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
+
42
−
72
View file @
5aaf0a6a
...
...
@@ -26,6 +26,8 @@
#ifndef E_ACSL_BITS
#define E_ACSL_BITS
#include
<stdint.h>
/* FIXME: Present implementation is built for little-endian byte order. That
* is, the implementation assumes that least significant bytes are stored at
* the highest memory addresses. In future support for big-endian/PDP byte
...
...
@@ -41,91 +43,59 @@
#endif
/* Bit-level manipulations {{{ */
/* 64-bit type with all bits set to zeroes */
const
uint64_t
ZERO
=
0
;
/* 64-bit type with all bits set to ones */
const
uint64_t
ONE
=
~
0
;
/* Set a given bit in a number to '1'.
* Example: bitset(7, x) changes 7th lowest bit of x to 1 */
#define
bitse
t(_bit,_number) (_number |= 1 << _bit)
#define
setbi
t(_bit,_number) (_number |= 1 << _bit)
/* Same as bitset but the bit is set of 0 */
#define
bit
clear(_bit, _number) (_number &= ~(1 << _bit))
#define clear
bit
(_bit, _number) (_number &= ~(1 << _bit))
/* Evaluates to a true value if a given bit in a number is set to 1. */
#define
bit
check(_bit, _number) ((_number >> _bit) & 1)
#define check
bit
(_bit, _number) ((_number >> _bit) & 1)
/* Toggle a given bit. */
#define
bit
toggle(_bit, _number) (_number ^= 1 << _bit)
#define toggle
bit
(_bit, _number) (_number ^= 1 << _bit)
/* Set a given bit to a specified value (e.g., 0 or 1). */
#define
bit
change(_bit, _val, _number) \
#define change
bit
(_bit, _val, _number) \
(_number ^= (-_val ^ _number) & (1 << _bit))
/* Fill the first n + skip bits of the memory area pointed to by s with ones
* (c != 0) or zeroes (c == 0).
*
* Example:
* let p1 be a pointer to 1111 1111 1111 1111 and
* p0 be a pointer to 0000 0000 0000 0000, then
*
* bitwise_memset(p0, 4, 1, 0)
* 1111 0000 0000 0000
* bitwise_memset(p1, 3, 0, 2)
* 1100 0111 1111 1111
*
* NB: In the grand scheme of things it is convenient to have a function that
* can set bits in a universal manner (such as the function below). On the other
* hand for blocks smaller than 64 bits using integers may be a faster way of
* dealing with bitwise operations. */
static
void
bitwise_memset
(
void
*
s
,
size_t
n
,
int
c
,
unsigned
int
skip
)
{
char
*
p
=
(
char
*
)
s
;
if
(
skip
)
{
p
+=
(
skip
/
8
);
skip
=
skip
%
8
;
if
(
skip
)
{
int
mask
=
255
;
if
(
skip
)
mask
=
(
mask
<<
skip
);
if
(
n
<
8
-
skip
)
mask
=
mask
&
(
255
>>
(
8
-
skip
-
n
));
n
=
(
n
>=
8
-
skip
)
?
n
-
8
+
skip
:
0
;
if
(
c
)
p
[
0
]
=
p
[
0
]
|
mask
;
else
p
[
0
]
=
p
[
0
]
&
(
mask
^
255
);
p
++
;
}
}
if
(
n
)
{
size_t
bytes
=
n
/
8
;
if
(
bytes
)
memset
(
p
,
c
?
255
:
0
,
bytes
);
if
(
c
)
p
[
bytes
]
=
p
[
bytes
]
|
(
255
>>
(
8
-
n
%
8
));
else
p
[
bytes
]
=
p
[
bytes
]
&
(
255
<<
n
%
8
);
}
/* Set up to 64-bit in given number (from the left)
* Example: setbits64(x, 7) sets first 7 bits in x to ones */
#define setbits64(_number, _bits) (_number |= ~(ONE << _bits))
/* Same as setbits64 but clears bits (sets to zeroes) */
#define clearbits64(_number, _bits) (_number &= ONE << _bits)
/* Assume _number is a 64-bit number and sets _bits from the right to ones
* Example: let x is a 64-bit zero, then setbits64(x, 7) will yield:
* 00000000 00000000 00000000 00000000 00000000 00000000 00000000 01111111 */
#define setbits64_right(_number, _bits) (_number |= ~(ONE >> _bits))
/* Same as setbits64_right but clears bits (sets to zeroes) */
#define clearbits64_right(_number, _bits) (_number &= ONE >> _bits)
void
setbits
(
void
*
ptr
,
size_t
size
)
{
size_t
i
;
int64_t
*
lp
=
(
int64_t
*
)
ptr
;
for
(
i
=
0
;
i
<
size
/
64
;
i
++
)
*
(
lp
+
i
)
|=
ONE
;
setbits64
(
*
(
lp
+
i
),
size
%
64
);
}
/* Same as bitwise_memset with skip parameter 0 but sets the bits from right
* to left. Example:
* let p1 be a pointer to 1111 1111 1111 1111, then
* bitwise_memset_backwards(p1, 5, 0) will lead to
* 1111 1111 1110 0000 */
static
void
bitwise_memset_backwards
(
void
*
s
,
size_t
n
,
int
c
)
{
char
*
p
=
(
char
*
)
s
;
int
bytes
=
n
/
8
;
p
-=
bytes
;
memset
(
p
,
c
?
255
:
0
,
bytes
);
p
--
;
if
(
!
c
)
p
[
0
]
=
p
[
0
]
&
(
255
>>
n
%
8
);
else
p
[
0
]
=
p
[
0
]
|
(
255
<<
(
8
-
n
%
8
));
void
clearbits
(
void
*
ptr
,
size_t
size
)
{
size_t
i
;
int64_t
*
lp
=
(
int64_t
*
)
ptr
;
for
(
i
=
0
;
i
<
size
/
64
;
i
++
)
*
(
lp
+
i
)
&=
ZERO
;
clearbits64
(
*
(
lp
+
i
),
size
%
64
);
}
/* }}} */
#endif
#endif
\ No newline at end of file
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