Type Members

1.  class erasable extends Annotation

   Annotations

   @ignore()

2.  class extern extends Annotation

   Only extract the contracts and replace the annotated function's body with a choose.

   Only extract the contracts and replace the annotated function's body with a choose.

   Annotations

   @ignore() @field() @getter() @setter() @param()

3.  class ghost extends Annotation with StaticAnnotation

   Code annotated with @ghost is removed after stainless extraction.

   Code annotated with @ghost is removed after stainless extraction.

   Code that can be annotated with @ghost: classes, method and value definitions, method parameters.

   See the Stainless specification for details.

   Annotations

   @ignore() @field() @getter() @setter() @param()

4.  class ignore extends Annotation

   The annotated symbols is not extracted at all.

   The annotated symbols is not extracted at all. For internal usage only.

5.  class indexedAt extends Annotation

   Annotations

   @ignore()

6.  class induct extends Annotation

   Apply the "induct" tactic during verification of the annotated function.

   Apply the "induct" tactic during verification of the annotated function.

   Annotations

   @ignore()

7.  class inlineOnce extends Annotation

   Inline this function, but only once.

   Inline this function, but only once. This might be useful if one wants to eg. inline a recursive function. Note: A recursive function will not be inlined within itself.

   Annotations

   @ignore()

8.  class invariant extends Annotation

   Denotes the annotated method as an invariant of its class

   Denotes the annotated method as an invariant of its class

   Annotations

   @ignore()

9.  class keep extends Annotation

   Can be used to mark a library function/class/object so that it is not filtered out by the keep objects.

   Can be used to mark a library function/class/object so that it is not filtered out by the keep objects. Use the command-line option --keep=g to keep all objects marked by @keep(g)

   Annotations

   @ignore()

10.  class law extends Annotation

    Mark this function as expressing a law that must be satisfied by instances or subclasses of the enclosing class.

    Mark this function as expressing a law that must be satisfied by instances or subclasses of the enclosing class.

    Annotations

    @ignore()

11.  class library extends Annotation

    The annotated function or class' methods are not verified by default (use --functions=...

    The annotated function or class' methods are not verified by default (use --functions=... to override this).

    Annotations

    @ignore()

12.  class mutable extends Annotation

    Used to mark non-sealed classes that must be considered mutable.

    Used to mark non-sealed classes that must be considered mutable. Can also be used to mark a type parameter T to announce that it can be instantiated with mutable types

    Annotations

    @ignore()

13.  class opaque extends Annotation

    Don't unfold the function's body during verification.

    Don't unfold the function's body during verification.

    Annotations

    @ignore()

14.  class partialEval extends Annotation

    Instruct Stainless to partially evaluate calls to the annotated function.

    Instruct Stainless to partially evaluate calls to the annotated function.

    Annotations

    @ignore()

15.  class pure extends Annotation

    Specify that the annotated function is pure, which will be checked.

    Specify that the annotated function is pure, which will be checked.

    Annotations

    @ignore() @field() @getter() @setter() @param()

16.  class wrapping extends Annotation

    Disable overflow checks for sized integer arithmetic operations within the annotated function.

    Disable overflow checks for sized integer arithmetic operations within the annotated function.

    Annotations

    @ignore()