xlang does not eliminate side effect in blocks
Function invocation not attached to any value in a statement block should be kept for potential side effects. The committed regression test illustrates the issue. Additionally, become consistent in the name XLang in various files of Leon.
Showing
- src/main/scala/leon/Main.scala 4 additions, 4 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/xlang/ImperativeCodeElimination.scala 12 additions, 0 deletionssrc/main/scala/leon/xlang/ImperativeCodeElimination.scala
- src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala 1 addition, 1 deletionsrc/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
- src/main/scala/leon/xlang/XLangAnalysisPhase.scala 1 addition, 1 deletionsrc/main/scala/leon/xlang/XLangAnalysisPhase.scala
- src/test/resources/regression/verification/xlang/invalid/Asserts.scala 16 additions, 0 deletions...urces/regression/verification/xlang/invalid/Asserts.scala
- src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala 1 addition, 1 deletion...n/test/verification/PureScalaVerificationRegression.scala
- src/test/scala/leon/test/verification/XLangVerificationRegression.scala 2 additions, 2 deletions.../leon/test/verification/XLangVerificationRegression.scala
Loading
Please register or sign in to comment