You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It seems to insert the goto %0000000f in the block 00000008 even though 0000000f is not reachable from this block.
Perhaps a fix would be to just run a pass on the generated blocks and remove all jump terms that occur after an unconditional jump within a given block.
Consider the following BIL program:
We would expect that the final value of
#56
will be conditional, summarized by the postcondition:However, this is not how WP treats it in BIR:
And indeed, it seems to treat the
goto #56
at tid0000000c
as a no-op, which results in our goal above being refuted.A solution would be to tighten assumptions about the behavior of indirect jumps (perhaps here?)
The text was updated successfully, but these errors were encountered: