Support for Array - Githubissues

mantognini / leon

The Leon system for verification, synthesis, and more.

leon.epfl.ch

Other

0 stars 0 forks source link

Support for Array #2

Closed mantognini closed 8 years ago

mantognini commented 8 years ago

Subtasks of #1.

:red_circle: indicate limitations in Leon itself.

[x] Create array using VLA (array on the stack)
[x] Accept array as parameter
[x] Read array (length + values)
[x] Prevent returning arrays
[ ] Allow editing array passed as function parameter :red_circle:
[ ] Add support for 2 dimensional array :red_circle:
[ ] Add support for N-dimensional arrays :red_circle: :question:

mantognini commented 8 years ago

:red_circle: Current limitation of Leon with 2D arrays:

  def main = {
    // This is not supported by Leon:
    val m = Array.fill(2, 3)(0)
    // Error:
    // Could not extract as PureScala (Scala tree of type class scala.reflect.internal.Trees$ApplyToImplicitArgs)
    0
  }