mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-09-04 14:50:19 -07:00
parent 3d9120c745 23af977d68
commit 19a8fa8a25
1 changed files with 15 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/util/memory_manager.cpp
View file

@ -35,6 +35,7 @@ static long long g_memory_max_used_size = 0;
static long long g_memory_watermark = 0;
static bool g_exit_when_out_of_memory = false;
static char const * g_out_of_memory_msg = "ERROR: out of memory";
static volatile bool g_memory_fully_initialized = false;
void memory::exit_when_out_of_memory(bool flag, char const * msg) {
g_exit_when_out_of_memory = flag;
@ -83,10 +84,18 @@ void memory::initialize(size_t max_size) {
initialize = true;
}
}
if (!initialize)
return;
g_memory_out_of_memory = false;
mem_initialize();
if (initialize) {
g_memory_out_of_memory = false;
mem_initialize();
g_memory_fully_initialized = true;
}
else {
// Delay the current thread until the DLL is fully initialized
// Without this, multiple threads can start to call API functions
// before memory::initialize(...) finishes.
while (!g_memory_fully_initialized)
/* wait */ ;
}
}
bool memory::is_out_of_memory() {
@ -98,9 +107,9 @@ bool memory::is_out_of_memory() {
return r;
}
void memory::set_high_watermark(size_t watermak) {
void memory::set_high_watermark(size_t watermark) {
// This method is only safe to invoke at initialization time, that is, before the threads are created.
g_memory_watermark = watermak;
g_memory_watermark = watermark;
}
bool memory::above_high_watermark() {