Mutable fields in traits cannot have a default value when using var inside @extern class

[vkuncak]

trafficstars

This code:

@extern
case class Foo() {
  var counter: Int = 0
}

shows message:

[ Error  ] extern.scala:5:5: Mutable fields in traits cannot have a default value
               var counter: Int = 0

what is the intention here? Without @extern, we get error that vars are not allowed.

[saraswat]

Indeed, this is the case with trait as well.

To be perfectly clear, it would be highly desirable if @extern marked classes were left alone by Stainless -- only scalac processing was done on them, e.g. type-checking. In this way, we could support some form of incrementality -- proving some properties hold for some code paths inside large code bases, without forcing the entire code base to be converted to Pure Scala.

[romac]

You can use @ignore to leave out a definition (class, object, method, function) entirely.