gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

If/Loop branch conditions using wrong position information #26

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

The branch information being sent to the brancher.branch function in Executor for if statements and loop branching contains not quite the correct positional information. ce.condition is being used for the position information; however, ce.condition is potentially the negated version of the condition and so it is not directly an AST element that can be tracked. Removing the negation, even if the condition itself has negation should be okay in this case as either way an AST element for the correct location should be available if an outer negation is removed.

jennalwise commented 2 years ago

Fixed in these commits: https://github.com/gradual-verification/silicon-gv/commit/7505b755655f221111219593efeadcc0ae577104 and https://github.com/gradual-verification/silicon-gv/commit/1bf97ba6ff353d72c605d07abef5faec7606527e