Skip to content
Snippets Groups Projects
Commit 9321437a authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Fix bug in isPurelyFunctional, comments

parent f46962ed
Branches
Tags
No related merge requests found
...@@ -3,10 +3,7 @@ ...@@ -3,10 +3,7 @@
package inox package inox
package ast package ast
import utils._ /** Provides functions to manipulate [[Expressions.Expr]].
import scala.reflect._
/** Provides functions to manipulate [[purescala.Expressions]].
* *
* This object provides a few generic operations on Leon expressions, * This object provides a few generic operations on Leon expressions,
* as well as some common operations. * as well as some common operations.
...@@ -114,9 +111,9 @@ trait ExprOps extends GenTreeOps { ...@@ -114,9 +111,9 @@ trait ExprOps extends GenTreeOps {
/** Returns if this expression behaves as a purely functional construct, /** Returns if this expression behaves as a purely functional construct,
* i.e. always returns the same value (for the same environment) and has no side-effects * i.e. always returns the same value (for the same environment) and has no side-effects
*/ */
def isPurelyFunctional(e: Expr): Boolean = exists { def isPurelyFunctional(e: Expr): Boolean = !exists {
case _ : Error => false case _ : Error => true
case _ => true case _ => false
}(e) }(e)
/** Extracts the body without its specification /** Extracts the body without its specification
......
...@@ -80,7 +80,6 @@ trait Trees extends Expressions with Extractors with Types with Definitions with ...@@ -80,7 +80,6 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
/** Builds a fresh identifier /** Builds a fresh identifier
* *
* @param name The name of the identifier * @param name The name of the identifier
* @param tpe The type of the identifier
* @param alwaysShowUniqueID If the unique ID should always be shown * @param alwaysShowUniqueID If the unique ID should always be shown
*/ */
def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = { def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = {
...@@ -92,7 +91,7 @@ trait Trees extends Expressions with Extractors with Types with Definitions with ...@@ -92,7 +91,7 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
* *
* @param name The name of the identifier * @param name The name of the identifier
* @param forceId The forced ID of the identifier * @param forceId The forced ID of the identifier
* @param tpe The type of the identifier * @param alwaysShowUniqueID If the unique ID should always be shown
*/ */
def forceId(name: String, forceId: Int, alwaysShowUniqueID: Boolean = false): Identifier = def forceId(name: String, forceId: Int, alwaysShowUniqueID: Boolean = false): Identifier =
new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, alwaysShowUniqueID) new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, alwaysShowUniqueID)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment