diff --git a/frontends/benchmarks/dotty-specific/invalid/i1479.scala b/frontends/benchmarks/dotty-specific/invalid/i1479.scala new file mode 100644 index 0000000000..58a776e2d1 --- /dev/null +++ b/frontends/benchmarks/dotty-specific/invalid/i1479.scala @@ -0,0 +1,15 @@ +object i1479 { + case class MyClass(var x: BigInt, var y: BigInt, var isValid: Boolean = true) { + require(!isValid || x <= y) + } + + inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit = + m.isValid = false // Note that we may not have mc.x <= mc.y so this is invalid + body + m.isValid = true + + def inc(m: MyClass): Unit = + changeMyClass(m): + m.x += 1 + m.y += 1 +} \ No newline at end of file diff --git a/frontends/benchmarks/dotty-specific/valid/i1479.scala b/frontends/benchmarks/dotty-specific/valid/i1479.scala new file mode 100644 index 0000000000..5cab60ae49 --- /dev/null +++ b/frontends/benchmarks/dotty-specific/valid/i1479.scala @@ -0,0 +1,17 @@ +object i1479 { + case class MyClass(var x: BigInt, var y: BigInt, var isValid: Boolean = true) { + require(!isValid || x <= y) + } + + inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit = + require(m.isValid) + m.isValid = false + body + m.isValid = true + + def inc(m: MyClass): Unit = + require(m.isValid) + changeMyClass(m): + m.x += 1 + m.y += 1 +} \ No newline at end of file diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala index a82e857391..e7068314ef 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala @@ -62,7 +62,7 @@ trait ASTExtractors { if (sym eq NoSymbol) return Seq.empty - val erased = if (sym.isEffectivelyErased) Seq(("ghost", Seq.empty[tpd.Tree])) else Seq() + val erased = if (sym.isEffectivelyErased && !(sym is Inline)) Seq(("ghost", Seq.empty[tpd.Tree])) else Seq() val selfs = sym.annotations val owners = if (ignoreOwner) List.empty[Annotation]