viperproject / silver

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

No non-pure check for predicate access arguments #720

Closed vfukala closed 1 year ago

vfukala commented 1 year ago

Consider

predicate p(flag: Bool)

method client() {
    inhale p(p(false))
}

Silver doesn't produce any consistency errors for this program. Silicon and Carbon then both crash on such an input.

I think there should be a consistency check that predicate access arguments are pure. Similarly to when we check that function arguments are pure.