viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 43 forks source link

Fixing crash in proof obligation expression computation #783

Closed marcoeilers closed 6 months ago

marcoeilers commented 6 months ago

This code could crash because the list of subconditions for And, Or and Implies actually returns three lists of subnodes instead of two, which the code expected. This is because it return one list per subnode, and the subnodes include the type of the node, which is why there are three subnodes for binary operations.