-
- Downloads
Fix issue in freshenLocals where a ValDef would sometimes be freshened twice
The issue is due to `scala.collection.mutable.HashMap#getOrElseUpdate` being broken[1, 2] in Scala v2.11.9 - v2.12.7. This sometimes resulted in ill-formed code, such as in the following example surfaced in https://github.com/epfl-lara/stainless/pull/433: BEFORE FRESHENING: val A$103: (Object$0) => Boolean = (x$186: Object$0) => x$186 is Integer$0 val thiss$7: { x$245: Object$0 | @unchecked isMonoid$0(x$245, A$103) } = thiss$12 val x$178: { x$247: Object$0 | @unchecked A$103(x$247) } = Integer$0(x$180) val y$17: { x$248: Object$0 | @unchecked A$103(x$248) } = Integer$0(y$19) val z$10: { x$249: Object$0 | @unchecked A$103(x$249) } = Integer$0(z$12) @unchecked (append$2(A$103, thiss$7, x$178, append$2(A$103, thiss$7, y$17, z$10)) == append$2(A$103, thiss$7, append$2(A$103, thiss$7, x$178, y$17), z$10)) AFTER FRESHENING: val A$108: (Object$0) => Boolean = (x$345: Object$0) => x$345 is Integer$0 val thiss$13: { x$346: Object$0 | @unchecked isMonoid$0(x$346, A$108) } = thiss$12 val x$348: { x$347: Object$0 | @unchecked A$108(x$347) } = Integer$0(x$180) val y$22: { x$349: Object$0 | @unchecked A$108(x$349) } = Integer$0(y$19) val z$14: { x$350: Object$0 | @unchecked A$108(x$350) } = Integer$0(z$12) @unchecked (append$2(A$108, thiss$13, x$348, append$2(A$108, thiss$13, y$22, z$15)) == append$2(A$108, thiss$13, append$2(A$108, thiss$13, x$348, y$22), z$15)) Note that `z$10` has been freshened twice above: once to `z$14`, and then again to `z$15`. - [1] https://github.com/scala/bug/issues/10703 - [2] https://github.com/retronym/scala/commit/5af85b5ce690d62bab90f8738c3fe1d0d2e0e41f
parent
ac07339d
No related branches found
No related tags found
Loading
Please register or sign in to comment