Skip to content

Commit

Permalink
termination
Browse files Browse the repository at this point in the history
  • Loading branch information
Dspil committed Sep 13, 2023
1 parent 21bd69f commit fa0a0d4
Showing 1 changed file with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -509,6 +509,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
* ensures slen(result) == j - i
* ensures scap(result) == alen(a) - i
* ensures sarray(result) == a
* decreases _
* {
* sfullSliceFromArray(a, i, j, alen(a))
* }
Expand All @@ -525,6 +526,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
val pre1 = synthesized(vpr.LeCmp(vpr.IntLit(0)(), iDecl.localVar))("The low bound of the slice might be negative")
val pre2 = synthesized(vpr.LeCmp(iDecl.localVar, jDecl.localVar))("The low bound of the slice might exceed the high bound")
val pre3 = synthesized(vpr.LeCmp(jDecl.localVar, ctx.array.len(aDecl.localVar)()))("The high bound of the slice might exceed the array capacity")
val pre4 = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")

// postconditions
val result = vpr.Result(ctx.slice.typ(typ))()
Expand All @@ -545,7 +547,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
s"${Names.sliceFromArray}_${Names.serializeType(typ)}",
Seq(aDecl, iDecl, jDecl),
ctx.slice.typ(typ),
Seq(pre1, pre2, pre3),
Seq(pre1, pre2, pre3, pre4),
Seq(post1, post2, post3, post4),
if (generateFunctionBodies) Some(body) else None
)()
Expand Down

0 comments on commit fa0a0d4

Please sign in to comment.