Catching “Out of Memory” Errors
Handling “Out of Memory” errors is tricky for Yices. When memory cannot be allocated, the internal data structures maintained by Yices may be left in an inconsistent state, and there is little one can do to recover from such a state.
When memory allocation fails, the default behavior of the Yices
library is to print an error message on stderr
and then call
exit(YICES_EXIT_OUT_OF_MEMORY)
. This kills the whole process.
Since Yices 2.4.2, it is possible to change this behavior. One can register a callback function to be invoked if Yices runs out or memory. The callback function is called when memory allocation fails and can do something less brutal than killing the process.
To install an out-of-memory callback, use the following function:
-
void yices_set_out_of_mem_callback(void (*callback)(void))
The unique argument is a pointer to the callback function. This function takes no argument and returns nothing.
The code that handles out-of-memory errors stores the function pointer in a global variable. If memory allocation fails, the following function is called:
void out_of_memory(void) {
if (__out_of_mem_callback != NULL) {
__out_of_mem_callback();
} else {
fprintf(stderr, "Out of memory\n");
}
exit(YICES_EXIT_OUT_OF_MEMORY);
}
If there’s no callback, then Yices kills the whole process as
mentioned before, otherwise, Yices invokes the callback function. This
function is not expected to return. If it does, Yices will call
exit
.
Warning
The callback function must not make any call to the Yices API. Even
a call to yices_exit
could cause a segmentation fault.
Note
Yices depends on the GMP library, which also makes use of malloc
and may also call exit
if malloc
fails. Consult the GMP
documentation if you want to also intercept out-of-memory errors
triggered by GMP.