Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
divine-ltsmin-deb
Commits
aa87eed2
Commit
aa87eed2
authored
Sep 04, 2017
by
Alexandre Duret-Lutz
Browse files
Fix two errors reported by gcc.
parent
df2b7bf8
Changes
2
Hide whitespace changes
Inline
Side-by-side
divine/legacy/common/bit_string.hh
View file @
aa87eed2
...
...
@@ -22,7 +22,7 @@ using std::cerr; using std::endl;
static
const
ulong_int_t
bit_values
[
32
]
=
{
1
,
2
,
4
,
8
,
16
,
32
,
64
,
128
,
256
,
1
<<
9
,
1
<<
10
,
1
<<
11
,
1
<<
12
,
1
<<
13
,
1
<<
14
,
1
<<
15
,
1
<<
16
,
1
<<
17
,
1
<<
18
,
1
<<
19
,
1
<<
20
,
1
<<
21
,
1
<<
22
,
1
<<
23
,
1
<<
24
,
1
<<
25
,
1
<<
26
,
1
<<
27
,
1
<<
28
,
1
<<
29
,
1
<<
30
,
1
<<
31
};
1
<<
25
,
1
<<
26
,
1
<<
27
,
1
<<
28
,
1
<<
29
,
1
<<
30
,
1
U
<<
31
};
//!Class for impementation of field of bits
...
...
@@ -116,11 +116,11 @@ class bit_string_t
*/
size_int_t
get_allocated_4bytes_count
()
const
{
return
allocated
;
}
//!Returns a count of allocated bits
size_int_t
get_bit_count
()
const
{
return
bits
;
}
//!Prints a sequence of zeros and ones representing a content
//! to output stream `outs'.
void
DBG_print
(
std
::
ostream
&
outs
=
cerr
)
const
...
...
@@ -131,14 +131,14 @@ class bit_string_t
if
(
get_bit
(
i
))
outs
<<
'1'
;
else
outs
<<
'0'
;
outs
<<
endl
;
}
//!Bitwisely adds `from' to (*this)
void
add
(
const
bit_string_t
&
from
)
{
for
(
size_int_t
i
=
0
;
i
!=
allocated
;
++
i
)
mem
[
i
]
=
mem
[
i
]
|
from
.
mem
[
i
];
}
//!Returns true iff (`bs1' & `bs2') != 0
friend
bool
operator
&
(
const
bit_string_t
&
bs1
,
const
bit_string_t
&
bs2
)
{
...
...
@@ -146,7 +146,7 @@ class bit_string_t
if
(
bs1
.
mem
[
i
]
&
bs2
.
mem
[
i
])
return
false
;
return
true
;
}
//!Returns true iff (`bs1' | `bs2') != 0
friend
bool
operator
|
(
const
bit_string_t
&
bs1
,
const
bit_string_t
&
bs2
)
{
...
...
@@ -154,7 +154,7 @@ class bit_string_t
if
(
bs1
.
mem
[
i
]
|
bs2
.
mem
[
i
])
return
false
;
return
true
;
}
//!Returns true iff (`bs1' xor `bs2') != 0
friend
bool
operator
^
(
const
bit_string_t
&
bs1
,
const
bit_string_t
&
bs2
)
{
...
...
divine/legacy/storage/explicit_storage.cc
View file @
aa87eed2
...
...
@@ -4,7 +4,7 @@
using
namespace
divine
;
// {{{ state_ref_t
// {{{ state_ref_t
state_ref_t
::
state_ref_t
()
{
...
...
@@ -22,7 +22,7 @@ bool state_ref_t::is_valid()
// if (page_id != id || id != hres || hres != 1024*1024+1)
if
(
id
!=
hres
||
hres
!=
1024
*
1024
+
1
)
return
true
;
else
else
return
false
;
}
...
...
@@ -41,7 +41,7 @@ std::string state_ref_t::to_string()
}
// }}}
// {{{ constructor
// {{{ constructor
explicit_storage_t
::
explicit_storage_t
(
error_vector_t
&
errorvector
)
:
errvec
(
errorvector
)
{
...
...
@@ -62,7 +62,7 @@ explicit_storage_t::explicit_storage_t(error_vector_t& errorvector):errvec(error
}
// }}}
// {{{ init
// {{{ init
void
explicit_storage_t
::
init
(
explicit_system_t
&
sys
)
{
...
...
@@ -70,7 +70,7 @@ void explicit_storage_t::init(explicit_system_t& sys)
memset
(
&
storage
,
0
,
sizeof
(
storage_t
));
mem_counting
(
ht_size
*
sizeof
(
ht_member_t
));
mem_counting
(
ht_size
*
sizeof
(
ht_member_t
));
storage
.
ht_base
=
new
ht_member_t
[
ht_size
];
memset
(
storage
.
ht_base
,
0
,
ht_size
*
sizeof
(
ht_member_t
));
...
...
@@ -79,7 +79,7 @@ void explicit_storage_t::init(explicit_system_t& sys)
}
// }}}
// {{{ set_functions
// {{{ set_functions
void
explicit_storage_t
::
set_col_init_size
(
size_t
coltable_init_size
)
{
...
...
@@ -92,7 +92,7 @@ void explicit_storage_t::set_col_init_size(size_t coltable_init_size)
{
errvec
<<
"storage: cannot initialize colision table size to 0"
<<
thr
(
EXPLICIT_STORAGE_ERR_TYPE
);
}
}
col_init_size
=
coltable_init_size
;
}
...
...
@@ -121,7 +121,7 @@ void explicit_storage_t::set_compression_method(size_t compression_method_id)
compression_method
=
compression_method_id
;
}
else
{
{
errvec
<<
"storage: unknown compression method"
<<
thr
(
EXPLICIT_STORAGE_ERR_TYPE
);
}
...
...
@@ -170,7 +170,7 @@ void explicit_storage_t::set_appendix_size(size_t appendix_size_in)
}
// }}}
// {{{ get_stats
// {{{ get_stats
size_t
explicit_storage_t
::
get_mem_used
()
{
...
...
@@ -208,19 +208,19 @@ size_t explicit_storage_t::get_ht_occupancy()
}
// }}}
// {{{ mem_counting
// {{{ mem_counting
void
explicit_storage_t
::
mem_counting
(
int
modify_mem_counter_by
)
{
if
((
mem_used
+
modify_mem_counter_by
>
mem_limit
)
&&
(
mem_limit
>
0
))
{
{
errvec
<<
"Memory limit reached."
<<
thr
(
EXPLICIT_STORAGE_ERR_TYPE
);
}
else
{
mem_used
+=
modify_mem_counter_by
;
if
(
mem_max_used
<
mem_used
)
if
(
mem_max_used
<
mem_used
)
{
mem_max_used
=
mem_used
;
}
...
...
@@ -228,7 +228,7 @@ void explicit_storage_t::mem_counting(int modify_mem_counter_by)
}
// }}}
// {{{ insert
// {{{ insert
void
explicit_storage_t
::
insert
(
state_t
state
)
{
...
...
@@ -251,10 +251,10 @@ void explicit_storage_t::insert (state_t state, state_ref_t& state_reference)
int
cstate_size
=
0
;
hresult
=
hasher
.
get_hash
(
reinterpret_cast
<
unsigned
char
*>
(
state
.
ptr
),
state
.
size
,
EXPLICIT_STORAGE_HASH_SEED
);
EXPLICIT_STORAGE_HASH_SEED
);
hresult
=
hresult
%
ht_size
;
// compress state
// compress state
if
(
!
compressor
.
compress
(
state
,
cstate
,
cstate_size
))
{
...
...
@@ -263,7 +263,7 @@ void explicit_storage_t::insert (state_t state, state_ref_t& state_reference)
return
;
}
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
//the first state to be hashed here
{
mem_counting
(
col_init_size
*
sizeof
(
col_member_t
));
...
...
@@ -297,13 +297,13 @@ void explicit_storage_t::insert (state_t state, state_ref_t& state_reference)
{
//already inserted ...
delete
[]
cstate
;
//
std::cout <<" Storage.insert ... done (inserted before)"<<endl;
// std::cout <<" Storage.insert ... done (inserted before)"<<endl;
return
;
}
}
}
}
// if a free slot wasn't found then resize col_table
if
(
!
free_slot
)
{
...
...
@@ -326,12 +326,12 @@ void explicit_storage_t::insert (state_t state, state_ref_t& state_reference)
storage
.
states_max_col
=
storage
.
ht_base
[
hresult
].
col_size
;
}
}
}
}
// pos points to first free slot
mem_counting
(
cstate_size
+
appendix_size
);
mem_counting
(
cstate_size
+
appendix_size
);
storage
.
ht_base
[
hresult
].
col_table
[
pos
].
ptr
=
cstate
;
storage
.
ht_base
[
hresult
].
col_table
[
pos
].
size
=
cstate_size
;
...
...
@@ -362,7 +362,7 @@ void explicit_storage_t::insert (state_t state, state_ref_t& state_reference)
{
storage
.
states_max_stored
=
storage
.
states_stored
;
}
// std::cout <<" Storage.insert ... done"<<endl;
return
;
}
...
...
@@ -382,9 +382,9 @@ bool explicit_storage_t::is_stored_if_not_insert(state_t state,state_ref_t& stat
bool
already_stored
=
false
;
hresult
=
hasher
.
get_hash
(
reinterpret_cast
<
unsigned
char
*>
(
state
.
ptr
),
state
.
size
,
EXPLICIT_STORAGE_HASH_SEED
);
EXPLICIT_STORAGE_HASH_SEED
);
hresult
=
hresult
%
ht_size
;
if
(
!
compressor
.
compress
(
state
,
cstate
,
cstate_size
))
{
...
...
@@ -393,7 +393,7 @@ bool explicit_storage_t::is_stored_if_not_insert(state_t state,state_ref_t& stat
return
false
;
}
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
//the first state to be hashed here
{
mem_counting
(
col_init_size
*
sizeof
(
col_member_t
));
...
...
@@ -435,7 +435,7 @@ bool explicit_storage_t::is_stored_if_not_insert(state_t state,state_ref_t& stat
}
}
}
// if a free slot wasn't found then resize col_table
if
(
!
free_slot
)
{
...
...
@@ -458,8 +458,8 @@ bool explicit_storage_t::is_stored_if_not_insert(state_t state,state_ref_t& stat
storage
.
states_max_col
=
storage
.
ht_base
[
hresult
].
col_size
;
}
}
}
}
// pos points to first free slot
mem_counting
(
cstate_size
+
appendix_size
);
storage
.
ht_base
[
hresult
].
col_table
[
pos
].
ptr
=
cstate
;
...
...
@@ -494,7 +494,7 @@ bool explicit_storage_t::is_stored_if_not_insert(state_t state,state_ref_t& stat
}
// }}}
// {{{ is_stored
// {{{ is_stored
bool
explicit_storage_t
::
is_stored
(
state_t
state
)
{
...
...
@@ -509,18 +509,18 @@ bool explicit_storage_t::is_stored (state_t state, state_ref_t& state_reference)
char
*
cstate
=
0
;
int
cstate_size
=
0
;
hresult
=
hasher
.
get_hash
(
reinterpret_cast
<
unsigned
char
*>
(
state
.
ptr
),
state
.
size
,
EXPLICIT_STORAGE_HASH_SEED
);
EXPLICIT_STORAGE_HASH_SEED
);
hresult
=
hresult
%
ht_size
;
if
(
!
compressor
.
compress
(
state
,
cstate
,
cstate_size
))
{
// std::cout <<" Storage.is_stored ... done (false)"<<endl;
return
false
;
}
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
if
(
!
(
storage
.
ht_base
[
hresult
].
col_table
))
{
delete
[]
cstate
;
// std::cout <<" Storage.is_stored ... done (false)"<<endl;
...
...
@@ -528,9 +528,9 @@ bool explicit_storage_t::is_stored (state_t state, state_ref_t& state_reference)
}
for
(
size_t
i
=
0
;
i
<
storage
.
ht_base
[
hresult
].
col_size
;
i
++
)
{
if
(
cstate_size
==
storage
.
ht_base
[
hresult
].
col_table
[
i
].
size
&&
storage
.
ht_base
[
hresult
].
col_table
[
i
].
ptr
)
if
(
cstate_size
==
storage
.
ht_base
[
hresult
].
col_table
[
i
].
size
&&
storage
.
ht_base
[
hresult
].
col_table
[
i
].
ptr
)
{
if
(
memcmp
(
cstate
,
storage
.
ht_base
[
hresult
].
col_table
[
i
].
ptr
,
...
...
@@ -540,7 +540,7 @@ bool explicit_storage_t::is_stored (state_t state, state_ref_t& state_reference)
state_reference
.
hres
=
hresult
;
state_reference
.
id
=
i
;
delete
[]
cstate
;
//
std::cout <<" Storage.is_stored ... done (true)"<<endl;
// std::cout <<" Storage.is_stored ... done (true)"<<endl;
return
true
;
}
}
...
...
@@ -551,11 +551,11 @@ bool explicit_storage_t::is_stored (state_t state, state_ref_t& state_reference)
}
// }}}
// {{{ delete_by_ref
// {{{ delete_by_ref
bool
explicit_storage_t
::
delete_by_ref
(
state_ref_t
state_reference
)
{
if
(
!
(
storage
.
ht_base
[
state_reference
.
hres
].
col_table
))
{
errvec
<<
"delet_by_ref(): invalid reference ..."
...
...
@@ -578,21 +578,21 @@ bool explicit_storage_t::delete_by_ref (state_ref_t state_reference)
storage
.
ht_base
[
state_reference
.
hres
].
col_table
[
state_reference
.
id
].
ptr
=
0
;
storage
.
ht_base
[
state_reference
.
hres
].
col_table
[
state_reference
.
id
].
size
=
0
;
}
}
}
storage
.
states_stored
--
;
return
true
;
return
true
;
}
// }}}
// {{{ delete_all_states
// {{{ delete_all_states
void
explicit_storage_t
::
delete_all_states
(
bool
leave_collision_lists
)
{
size_t
tmp_col_size
;
for
(
size_t
ht_row
=
0
;
ht_row
<
ht_size
;
ht_row
++
)
{
tmp_col_size
=
storage
.
ht_base
[
ht_row
].
col_size
;
tmp_col_size
=
storage
.
ht_base
[
ht_row
].
col_size
;
/* if tmp_col_size == 0 then the following loop is skipped */
for
(
size_t
pos_in_row
=
0
;
pos_in_row
<
tmp_col_size
;
pos_in_row
++
)
{
...
...
@@ -612,21 +612,21 @@ void explicit_storage_t::delete_all_states(bool leave_collision_lists)
storage
.
ht_base
[
ht_row
].
col_table
=
NULL
;
storage
.
ht_base
[
ht_row
].
col_size
=
0
;
}
}
if
(
!
leave_collision_lists
)
{
storage
.
collisions
=
0
;
storage
.
states_col
=
0
;
}
storage
.
states_stored
=
0
;
storage
.
collisions
=
0
;
storage
.
ht_occupancy
=
0
;
}
// }}}
// {{{ reconstruct
// {{{ reconstruct
state_t
explicit_storage_t
::
reconstruct
(
state_ref_t
state_reference
)
{
...
...
@@ -640,24 +640,24 @@ state_t explicit_storage_t::reconstruct(state_ref_t state_reference)
if
(
storage
.
ht_base
[
state_reference
.
hres
].
col_table
)
{
if
(
storage
.
ht_base
[
state_reference
.
hres
].
col_table
[
state_reference
.
id
].
ptr
)
{
{
compressor
.
decompress
(
result
,
storage
.
ht_base
[
state_reference
.
hres
].
col_table
[
state_reference
.
id
].
ptr
,
storage
.
ht_base
[
state_reference
.
hres
].
col_table
[
state_reference
.
id
].
size
);
//
std::cout <<" Storage.reconstruct ... done "<<endl;
// std::cout <<" Storage.reconstruct ... done "<<endl;
return
result
;
}
}
}
errvec
<<
"reconstruct(): invalid reference ..."
<<
psh
(
EXPLICIT_STORAGE_ERR_TYPE
);
return
result
;
}
// }}}
// {{{ appendix
// {{{ appendix
void
*
explicit_storage_t
::
app_by_ref
(
state_ref_t
refer
)
{
...
...
@@ -672,7 +672,7 @@ void* explicit_storage_t::app_by_ref(state_ref_t refer)
{
errvec
<<
"Invalid reference used in set_app_by_ref()."
<<
psh
(
EXPLICIT_STORAGE_ERR_TYPE
);
return
false
;
return
0
;
}
else
{
...
...
@@ -680,7 +680,7 @@ void* explicit_storage_t::app_by_ref(state_ref_t refer)
{
errvec
<<
"Invalid reference used in set_app_by_ref()."
<<
psh
(
EXPLICIT_STORAGE_ERR_TYPE
);
return
false
;
return
0
;
}
else
{
...
...
@@ -688,7 +688,7 @@ void* explicit_storage_t::app_by_ref(state_ref_t refer)
(
storage
.
ht_base
[
refer
.
hres
].
col_table
[
refer
.
id
].
ptr
+
storage
.
ht_base
[
refer
.
hres
].
col_table
[
refer
.
id
].
size
);
}
}
}
}
// }}}
...
...
Write
Preview
Supports
Markdown
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