Skip to content

Commit

Permalink
change dummy comment in synthesized
Browse files Browse the repository at this point in the history
  • Loading branch information
Dspil committed Sep 14, 2023
1 parent 4d73949 commit 0ab9faa
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -287,7 +287,7 @@ class SlicesImpl(val arrays : Arrays) extends Slices {
val rDecl = vpr.LocalVarDecl("right", vpr.Int)()
val body : vpr.Exp = vpr.Add(lDecl.localVar, rDecl.localVar)()
val post : vpr.Exp = vpr.EqCmp(vpr.Result(vpr.Int)(), body)()
val pre : vpr.Exp = synthesized(termination.DecreasesTuple(Seq.empty, None))("This function is assumed to terminate")
val pre : vpr.Exp = synthesized(termination.DecreasesTuple(Seq.empty, None))("Termination measure")
vpr.Function("sadd", Seq(lDecl, rDecl), vpr.Int, Seq(pre), Seq(post), Some(body))()
}

Expand Down

0 comments on commit 0ab9faa

Please sign in to comment.