viperproject / silver

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

Incorrect field assignments crash Viper #675

Closed marcoeilers closed 1 year ago

marcoeilers commented 1 year ago

The following program, where the field assignment mixes up the field name and the receiver expression, crashes Silicon and Carbon:

field f: Int

method m(r: Ref)
    requires acc(r.f)
{
   var tmp: Int
   f.r := tmp
}