Changes between Initial Version and Version 4 of Ticket #42


Ignore:
Timestamp:
01/18/2019 01:30:45 PM (5 years ago)
Author:
mornfall
Comment:

This is not something we can really fix -- it is a genuine violation of the property you asked for. Basically, the question you pose is, 'can this program fail assuming memory might run out' and the answer is yes, it may fail in the above way, with an unhandled exception. Perhaps you mean to pass -o nofail:malloc, which would make this go away, because you then assume memory never runs out; alternately, you may want to say that you don't care about running out of memory in the constructors and you can set nofail:malloc using a high-priority constructor and reset it using a low-priority one (see also dios_configure_fault). Perhaps you do not consider an unhandled exception a problem: maybe use std::set_terminate with a handler that just calls vm_cancel in that case.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #42

    • Property Status changed from new to closed
    • Property Resolution changed from to invalid
  • Ticket #42 – Description

    initial v4  
    11I'm using the static binary version 4.1.20+2018.12.17 of DIVINE. I'm trying to debug my program by running "divine sim", but it seems that it crashes after ony six steps. I've tried with four different programs and it seems to always happen the same way. Here's my latest output:
    22
     3{{{
    34divine sim examples/ToyApplication/ToyApplication.bc
    45No entry for terminal type "xterm-256color";
     
    6869#        at /home/xrockai/src/divine/static/dios/sys/fault.cpp:60
    6970>
     71}}}