Commit 0fd8636f authored by Matthew Fernandez's avatar Matthew Fernandez
Browse files

fix: use setjmp when we have assume statements

7dda1203 changed the way global assumptions were
emitted to return a boolean rather than signaling assumption failure via
siglongjmp. Following this, 603f1809 optimised
sigsetjmp calls to be skipped if max errors was 1, even if there were
assumptions in the model. The reasoning here was that assumptions were now using
regular control flow via returns, so didn't require a jmp_buf. The problem with
this is that assumption *statements* are still using siglongjmp.

The effect of these combined changes was that models that failed assume
statements would attempt to siglongjmp with an invalid jmp_buf causing a
segfault. On a debug verifier, this would become an assertion failure.

We repair this by now treating jmp_bufs as required if there are any assume
statements in the model. Note that this partially reverts
603f1809.

Github: closes #141 "segfault with misc/pending-queue-4k.m"
parent ad796007
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment