From b9b1de59aa2a6bcf362fab192f9f362c4c169039 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 26 May 2015 15:33:55 +0200
Subject: [PATCH] unit testing default evaluator for division semantics
---
.../evaluators/DefaultEvaluatorTests.scala | 57 +++++++++++++++++++
1 file changed, 57 insertions(+)
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index a94833107..b4b4540cd 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -77,9 +77,66 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
expectSuccessful(
defaultEvaluator.eval(Times(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(6))
+ }
+
+ test("Eval of division and modulo semantics for BigInt") {
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(3))
expectSuccessful(
defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(Division(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(1))
+ }
+
+ test("Eval of division and modulo semantics for bit vectors") {
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(10), IntLiteral(3))),
+ IntLiteral(3))
+ expectSuccessful(
+ defaultEvaluator.eval(BVModulo(IntLiteral(10), IntLiteral(3))),
+ IntLiteral(1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVModulo(IntLiteral(-1), IntLiteral(3))),
+ IntLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(-3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVModulo(IntLiteral(-1), IntLiteral(-3))),
+ IntLiteral(-1))
+
+ expectSuccessful(
+ defaultEvaluator.eval(BVDivision(IntLiteral(1), IntLiteral(-3))),
+ IntLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(BVModulo(IntLiteral(1), IntLiteral(-3))),
+ IntLiteral(1))
}
test("Eval of simple boolean operations") {
--
GitLab