vars need to be treated as functions within a common block

dijkstracula / irving

there's no checking like bounded model checking

GNU Affero General Public License v3.0

1 stars 0 forks source link

Open dijkstracula opened 10 months ago

dijkstracula commented 10 months ago

protocol p(self) {
  var foo: nat

  common {
    after init(self) {
      foo(self) := 0;
    }
  }
}

dijkstracula commented 10 months ago

Really, trying to handle common blocks at all was a dumb idea.