epfl-lara/stainless

Issues

• Use local directory in CI

  #1581 opened 2 months ago by vkuncak
  0

• Cache refactor to improve performance and footprint

  #1576 opened 3 months ago by samuelchassot
  1

• `--functions` does not account for trait methods dependencies

  #1571 opened 3 months ago by mario-bucev
  1

• `unfolding` should return the return value of the function so that it is a hint for verification, and has the behaviour of the unfolded function at runtime

  #1550 opened 4 months ago by samuelchassot
  4

• Finite sets printed in debug using curly braces instead of Set(...)

  #1544 opened 3 months ago by vkuncak
  2

• Internal type error in extraction when passing anonymous trait instance to method expecting trait

  #1553 opened 4 months ago by vkuncak
  2

• Missformed SMT source, Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication

  #1549 opened 4 months ago by vkuncak
  8

• introduce `old` outside of post condition

  #1551 opened 4 months ago by samuelchassot
  1

• "publicly opaque" concept would be useful when working with laws

  #1504 opened 9 months ago by samuelchassot
  2

• Missing dependencies when using bigSubstring

  #1542 opened 4 months ago by LioTree
  1

• Egg invariant: unsatisfiable invariant of locally declared classes that depend on mutable local state

  #1545 opened 4 months ago by vkuncak
  1

• ADT must appear only in strictly positive positions when using Map

  #1547 opened 4 months ago by LioTree
  0

• Type error when @extern method's result widens ADT value

  #1537 opened 5 months ago by vkuncak
  2

• StackOverflowError during Measure Inference

  #1536 opened 6 months ago by drganam
  0

• Unpredictable reporting on circular type classes

  #1535 opened 6 months ago by vkuncak
  0

• Treat the `erased` soft keyword as Stainless `@ghost`

  #1522 opened 7 months ago by vkuncak
  0

• Equalities to be rejected: Double, functions, allocatable non-case classes, type vars

  #1483 opened a year ago by vkuncak
  4

• Incorrect usage of `old` when it is not

  #1530 opened 6 months ago by mario-bucev
  0

• Well-formedness check failure when operating on an `Array` type alias

  #1529 opened 6 months ago by mario-bucev
  0

• Convert throw into assert(false)

  #1512 opened 6 months ago by vkuncak
  7

• PrimitiveSize functions should not be generated when termination checking is off?

  #1519 opened 7 months ago by drganam
  0

• Error reporting from alias analysis

  #1513 opened 7 months ago by vkuncak
  0

• MethodLifting reporting when subclasses have preconditions

  #1511 opened 7 months ago by vkuncak
  0

• Fatal error: Well-formedness check failed after extraction

  #1416 opened 2 years ago by drganam
  5

• Why is `ConcTree.Empty` not a `case object`?

  #1493 opened 7 months ago by acruise
  1

• Unsoundness when using `swap` due to AntiAliasing not flagging

  #1497 opened 10 months ago by samuelchassot
  9

• Incorrect transformation of inner functions mutating a local variable

  #1510 opened 7 months ago by mario-bucev
  0

• `AntiAliasing` does not update local aliasing information after replacement

  #1506 opened 8 months ago by mario-bucev
  0

• `AntiAliasing` not updating targets for `val` fields

  #1487 opened a year ago by mario-bucev
  2

• error: Lookup failed for adt with symbol `Conc$27` in phase FunctionSpecialization

  #1459 opened a year ago by vkuncak
  1

• Inconsistent positions for postcondition

  #1480 opened a year ago by mario-bucev
  1

• Inline functions that do mutation rejected as ghost

  #1479 opened a year ago by vkuncak
  3

• Crash in Inox type checker when using freshCopy

  #1474 opened a year ago by vkuncak
  1

• Failure of postcondition shown as failure of the assertion in the branch

  #1470 opened a year ago by vkuncak
  0

• Deep structure updates in non-aliased imperative (was: `computes` to use condition as a more efficient implementation)

  #1465 opened a year ago by samuelchassot
  4

• Incorrect "refinements checks for subtyping" generated in some cases

  #1463 opened a year ago by mario-bucev
  0

• Reconcile full-imperative using a ShareCell abstraction

  #1458 opened a year ago by vkuncak
  3

• Collection types in Stainless should be inductive

  #1457 opened a year ago by vkuncak
  0

• IArray support

  #1448 opened a year ago by vkuncak
  1

• Incorrect ADT member type approximation

  #1452 opened a year ago by mbovel
  2

• Size of type parameters

  #1451 opened a year ago by mbovel
  0

• Support for CVC5

  #1423 opened a year ago by samuelchassot
  1

• Slowness of `ValueClasses`

  #1426 opened a year ago by mario-bucev
  1

• Invalid conterexample in ScanLeft

  #1438 opened a year ago by fengwz17
  2

• Unsoundness of `no-inc:z3` involving class invariants

  #1432 opened a year ago by mario-bucev
  0

• Refinement type not properly freshened

  #1430 opened a year ago by mario-bucev
  0

• How can I define an AVL tree in Stainless?

  #1414 opened 2 years ago by mingyang91
  8

• Supporting more Either methods

  #1415 opened a year ago by andreagilot-da
  0

• CVC4 built from source with the attached modification (to build on arm64) makes Stainless freeze

  #1419 opened 2 years ago by samuelchassot
  1

• Better error reporting for expressions before decreases

  #1417 opened 2 years ago by andreagilot-da
  0