Convert throw into assert(false)

[vkuncak]

Convert throw into assert(false)

[vkuncak]

Sounds good. Yes, I guess users need to declare the exceptions. Having our own synonyms, including a constructor for Exception("...") might be useful.

[vkuncak]

Perhaps a clean way to do it would be to define in stainless.lang:

@extern
def throwReached[A](s: String): A
  require(false)
  ???

and then replace throw E with a call to throwReached("E")

[vkuncak]

One advantage of using such exception instead of assert is that, if ghost code is eliminated but Stainless function is used from unverified Scala code that does not meet the require clauses that Stainless assumed, then errors thrown will be easier to react to and classify than assertions.

[vkuncak]

If we address this with a PR, we should simultaneously add the Try type
https://github.com/scala/scala/blob/v2.13.3/src/library/scala/util/Try.scala#L64

To handle exception handling outside code (such as I/O) the users should write

@extern
def myMethods(x:A): Try[B] = {
   Try(BufferedMuffeledReaderWriter(...))
}

where Try is defined in stainless.lang

[samuelchassot]

We can hopefully also accept Exception as a super class (e.g. define it in stainless.lang) and permit its subclasses.

Here users would have to redefine their own exception classes to use subclasses, right?
For example, to use IllegalArgumentException, one would have to define her own IllegalArgumentException that extends stainless.lang.Exception. Or am I missing something?

[samuelchassot]

stainless/frontends/library/stainless/lang/package.scala

Line 41 in 54399d0

@library

there was a tentative apparently.

[samuelchassot]

This compiles, once I removed the check in FragmentChecker:

import stainless.lang.Exception

class IllegalArgumentException(msg: String) extends Exception

object ThrowTest {
  def f(): Unit = 
    throw new IllegalArgumentException("This is an exception")
}

Now I'll be working on the extraction of throw