the problem is that there's a call to g() that returns some poison. I was hoping that --disable-poison-input and/or --tgt-is-asm would prevent poison values from being introduced, but this doesn't seem to happen.
is this something that needs to be fixed on the Alive side?
one thing that I tried is to mark g()'s return value as noundef. after doing this, the refinement check succeeds, but I have do make the change both in the source and target, and that's something we're trying to avoid here.
the target code is from @katrinafyi's tool, extracted from the ARM semantics!
regehr
commented
4 months ago
attached is src/tgt pair that doesn't verify when we invoke like this:
the problem is that there's a call to g() that returns some poison. I was hoping that
--disable-poison-inputand/or--tgt-is-asmwould prevent poison values from being introduced, but this doesn't seem to happen.is this something that needs to be fixed on the Alive side?
one thing that I tried is to mark g()'s return value as noundef. after doing this, the refinement check succeeds, but I have do make the change both in the source and target, and that's something we're trying to avoid here.
the target code is from @katrinafyi's tool, extracted from the ARM semantics!
src.ll.txt tgt.ll.txt