This PR adds some elegant rules that propagate assume nodes down from a top-level function. It also adds a couple of tests.
Not included is rules for Switch, which are a little harder.
This PR changes Assumption to have three new variants: InIf and InFunction, and InSwitch.
I realized that our previous plan of using a strait up boolean condition isn't quite right due to effects. For example, if an If statement reads from memory, the value it reads is whatever was in memory at the execution time of the predicate.
This PR adds some elegant rules that propagate assume nodes down from a top-level function. It also adds a couple of tests.
Not included is rules for
Switch, which are a little harder.This PR changes
Assumptionto have three new variants:InIfandInFunction, andInSwitch. I realized that our previous plan of using a strait up boolean condition isn't quite right due to effects. For example, if anIfstatement reads from memory, the value it reads is whatever was in memory at the execution time of the predicate.