From b01a86823bc86a7c70571ec6baf8f3956ce0e05f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 25 Apr 2012 23:51:32 +0200
Subject: [PATCH] Evaluator case when postcondition of undefined funciton was
violated
---
src/main/scala/leon/Evaluator.scala | 7 +++++++
src/main/scala/leon/FairZ3Solver.scala | 4 ++++
2 files changed, 11 insertions(+)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 0f3204e70..6bb9ef1b3 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -24,11 +24,16 @@ object Evaluator {
case class InfiniteComputation() extends EvaluationResult {
val finalResult = None
}
+ case class PostconditionViolationFunctionFromModel() extends EvaluationResult {
+ val finalResult = None
+ }
+
def eval(context: EvaluationContext, expression: Expr, evaluator: Option[(EvaluationContext)=>Boolean], maxSteps: Int=500000) : EvaluationResult = {
case class RuntimeErrorEx(msg: String) extends Exception
case class InfiniteComputationEx() extends Exception
case class TypeErrorEx(typeError: TypeError) extends Exception
+ case class PostconditionViolationFunctionFromModelEx() extends Exception
var left: Int = maxSteps
@@ -96,6 +101,7 @@ object Evaluator {
val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
rec(frame + ((freshResID -> callResult)), postBody) match {
case BooleanLiteral(true) => ;
+ case BooleanLiteral(false) if !fd.hasImplementation => throw PostconditionViolationFunctionFromModelEx()
case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
case other => throw TypeErrorEx(TypeError(other, BooleanType))
}
@@ -307,6 +313,7 @@ object Evaluator {
case RuntimeErrorEx(msg) => RuntimeError(msg)
case InfiniteComputationEx() => InfiniteComputation()
case TypeErrorEx(te) => te
+ case PostconditionViolationFunctionFromModelEx() => PostconditionViolationFunctionFromModel()
}
}
}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index c29e06bac..ebca10ab2 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -827,6 +827,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info("- Invalid model.")
(false, asMap)
}
+ case PostconditionViolationFunctionFromModel() => {
+ reporter.info("- Invalid Model: postcondition violation of a function that whose implementation was specified by the model")
+ (false, asMap)
+ }
case other => {
reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
(false, asMap)
--
GitLab