user must guarantee that the UB is never ever triggered by their program.
-
I've been requesting comments on the RISC-V formal spec mailing list. We'll see what happens.. But it's clear that I can't implement this
in riscv-formal. Even a very small bounded and causal version of this would drastically complicate the SMT problems I'm constructing..
-
-
Definitely beyond me to impl at this point, but I am curious how a casual version would be done. Check insns side effects, if they are >>
-
"abornal", check a bounded number of insns ahead and behind to see if UB was encountered?
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.