epfl-lara/stainless

Issues

• Unpredictable reporting on circular type classes

  #1535 opened 5 days ago by vkuncak
  0

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

  #1522 opened 25 days ago by vkuncak
  0

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

  #1483 opened 7 months ago by vkuncak
  4

• Incorrect usage of `old` when it is not

  #1530 opened 14 days ago by mario-bucev
  0

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

  #1529 opened 14 days ago by mario-bucev
  0

• Convert throw into assert(false)

  #1512 opened 20 days ago by vkuncak
  7

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

  #1519 opened a month ago by drganam
  0

• Error reporting from alias analysis

  #1513 opened a month ago by vkuncak
  0

• MethodLifting reporting when subclasses have preconditions

  #1511 opened a month ago by vkuncak
  0

• Fatal error: Well-formedness check failed after extraction

  #1416 opened a year ago by drganam
  5

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

  #1493 opened a month ago by acruise
  1

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

  #1497 opened 4 months ago by samuelchassot
  9

• Incorrect transformation of inner functions mutating a local variable

  #1510 opened a month ago by mario-bucev
  0

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

  #1506 opened 2 months ago by mario-bucev
  0

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

  #1504 opened 3 months ago by samuelchassot
  1

• Call by name arguments unsound

  #1395 opened a year ago by andreagilot-da
  12

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

  #1487 opened 6 months ago by mario-bucev
  2

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

  #1459 opened 7 months ago by vkuncak
  1

• Inconsistent positions for postcondition

  #1480 opened 7 months ago by mario-bucev
  1

• Inline functions that do mutation rejected as ghost

  #1479 opened 7 months ago by vkuncak
  3

• Crash in Inox type checker when using freshCopy

  #1474 opened 7 months ago by vkuncak
  1

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

  #1470 opened 7 months ago by vkuncak
  0

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

  #1465 opened 7 months ago by samuelchassot
  4

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

  #1463 opened 7 months ago by mario-bucev
  0

• Reconcile full-imperative using a ShareCell abstraction

  #1458 opened 7 months ago by vkuncak
  3

• Collection types in Stainless should be inductive

  #1457 opened 7 months ago by vkuncak
  0

• IArray support

  #1448 opened 7 months ago by vkuncak
  1

• Incorrect ADT member type approximation

  #1452 opened 7 months ago by mbovel
  2

• Size of type parameters

  #1451 opened 7 months ago by mbovel
  0

• Support for CVC5

  #1423 opened 8 months ago by samuelchassot
  1

• Slowness of `ValueClasses`

  #1426 opened 8 months ago by mario-bucev
  1

• Invalid conterexample in ScanLeft

  #1438 opened 8 months 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

• Does not verify syntactic equality

  #1399 opened a year ago by andreagilot-da
  10

• How can I define an AVL tree in Stainless?

  #1414 opened a year 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 a year ago by samuelchassot
  1

• Crash when using --watch

  #1412 opened a year ago by andreagilot-da
  0

• Better error reporting for expressions before decreases

  #1417 opened a year ago by andreagilot-da
  0

• Function not equal to its body when using extern annotations

  #1411 opened a year ago by andreagilot-da
  1

• `FragmentChecker` does not go trough `ensuring`

  #1408 opened a year ago by mario-bucev
  1

• Better reporting during extraction, esp. for new users

  #1403 opened a year ago by vkuncak
  7

• Immutable scala sets don't work with extern annotation in Scala 2

  #1401 opened a year ago by andreagilot-da
  0

• Type error: couldn't find function `IntAbsToBigInt`

  #1405 opened a year ago by mario-bucev
  0

• Fatal error: Variable tmp is not defined in context

  #1407 opened a year ago by andreagilot-da
  1

• Using andThen leads to a fatal type error

  #1398 opened a year ago by andreagilot-da
  1

• Crashes when changing type parameters during instantiation with laws

  #1397 opened a year ago by vkuncak
  12

• Type error in presence of type aliases in `Map` keys

  #1390 opened a year ago by mario-bucev
  0

• Inox fatal error when doing imports of inner objects

  #1389 opened a year ago by andreagilot-da
  0