Report use of choose, @extern and ??? in the verification summary

[mario-bucev]

Closes #1366
For example, the following snippet:

import stainless.lang._
import stainless.collection._
import stainless.annotation._

object ExtractionSummary {

  case class OuterClass(okField: Int, @extern externField: Int) {
    def methodWithChoose: BigInt = choose((x: BigInt) => x >= 42)
    def methodWithExternInner: BigInt = {
      def inner: BigInt = {
        @extern
        def innerInnerInMethod: BigInt = 42
        innerInnerInMethod
      }
      inner
    }
  }

  def someFn(x: BigInt): BigInt = {
    @extern
    def innerExtern(x: BigInt) = x

    def usingChoose: BigInt = choose((x: BigInt) => x >= 42)

    x
  }

  def someFn2(x: BigInt, m: Map[BigInt, BigInt]): BigInt = {
    @extern
    def innerExtern2(x: BigInt) = x

    def usingChoose2: BigInt = choose((x: BigInt) => x >= 42)

    val z: BigInt = choose((x: BigInt) => x >= 42)
    val useKeys = m.keys
    x
  }

  def someFn3(x: BigInt): Unit = {
    case class InnerClass(f1: BigInt, @extern f2: BigInt) {
      @extern def methodOfInnerClass: BigInt = 42
    }
  }
}

will have the following short summary:

Verification pipeline summary:
  explicit choose, @extern, cache, 
  choose injection, nativez3, non-batched

and the extended summary:

Verification pipeline summary:
  -The following definitions contain explicit choose:
    -User:
      -Free functions:
        someFn2, usingChoose (defined in someFn), 
        usingChoose2 (defined in someFn2)
      -Class OuterClass:
        -Methods:
          methodWithChoose
  -The following definitions are @extern:
    -User:
      -Free functions:
        innerExtern (defined in someFn), innerExtern2 (defined in someFn2)
      -Class InnerClass:
        -Methods:
          methodOfInnerClass
        -Fields:
          f2
      -Class OuterClass:
        -Methods:
          _$innerInnerInMethod (defined in methodWithExternInner)
        -Fields:
          externField
    -Library:
      -Class MapOps:
        -Methods:
          keys
  Cache used
  -Anti-aliasing phase transformed the following functions:
    methodOfInnerClass
  -Choose injected in the following functions:
    -User:
      _$innerInnerInMethod, innerExtern, innerExtern2, methodOfInnerClass
    -Library:
      keys
  Solvers used: nativez3
  Processing mode: partial

[vkuncak]

We probably should not report the uses of choose in a library, but maybe we should somehow report unjustified uses of the library annotation. Can we check that the source files are not in a given directory, or can we use packages for this purpose?

[mario-bucev]

All definitions in the library are conveniently annotated with @library, it is trivial to filter them out. In this PR, library definitions and user definitions are split when reported, but I can modify it to only display user definitions.

[vkuncak]

I will merge this, but note that my point was that using library annotation in user code is itself a loophole.