epfl-lara / leon

The Leon system for verification, synthesis, repair
Other
161 stars 49 forks source link

Refactored to enable compiling the library with strict compilation flags #305

Open NicolasRouquette opened 7 years ago

NicolasRouquette commented 7 years ago

Fixes #304

I use the leon library in another project where I compile it with these settings:

scalacOptions ++= Seq(
  "-deprecation",
  "-encoding", "UTF-8",     // yes, this is 2 args
  "-feature",
  "-language:existentials",
  "-language:higherKinds",
  "-language:implicitConversions",
  "-unchecked",
  "-Xfatal-warnings",
  "-Xlint",
  "-Yno-adapted-args",
  "-Ywarn-dead-code",       // N.B. doesn't work well with the ??? hole
  "-Ywarn-numeric-widen",
  "-Ywarn-value-discard",
  "-Xfuture",
  "-Ywarn-unused-import",   // 2.11 only
  "-Yno-imports"            // no automatic imports at all; all symbols must be imported explicitly
)

Most of the refactoring is to due to moving classes and objects that were defined in a package object file to a separate compilation unit.

I was surprised that -Yno-imports helps readability of the library where an unqualified type name could be misunderstood to refer to a type in leon's library instead of the scala library. For example, in leon.lang.Bag, the unqualified List type needs to refer to scala.collection.immutable.List instead of leon.collection.List.

NicolasRouquette commented 7 years ago

The leon library was compiled with Artima's Supersafe with the following settings:

version 1
# See http://www.artima.com/supersafe_user_guide.html

# http://www.artima.com/supersafe_user_guide.html#array-comparison
# prevent nested array

# http://www.artima.com/supersafe_user_guide.html#preventing-a-type-from-being-used-in-comparison
prevent comparison Any nested

# http://www.artima.com/supersafe_user_guide.html#prevent-suspicious-inferred-type
prevent suspicious inferred type