From aa5eb2bbe9b0d9794b70ea8839cc4177975bff48 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 17 Feb 2015 17:57:04 +0100
Subject: [PATCH] parsing bit vector constants from cvc4
---
project/Build.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 2 ++
src/main/scala/leon/utils/TypingPhase.scala | 1 +
.../regression/verification/purescala/invalid/Array3.scala | 1 +
4 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/project/Build.scala b/project/Build.scala
index 70c01e8e7..6d2daf152 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -80,6 +80,6 @@ object Leon extends Build {
def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
- lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e721cf606f73c6ba41f7622c141a1eefef2c712d")
+ lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "8b37b5e95cd87093734ee342b484b1786c8c0bfe")
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 0c69b047b..98a129ce2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -515,6 +515,7 @@ trait SMTLIBTarget {
case (Core.True(), BooleanType) => BooleanLiteral(true)
case (Core.False(), BooleanType) => BooleanLiteral(false)
+ case (FixedSizeBitVectors.BitVectorConstant(n, 32), Int32Type) => IntLiteral(n.toInt)
case (SHexadecimal(hexa), Int32Type) => IntLiteral(hexa.toInt)
case (SimpleSymbol(s), _: ClassType) if constructors.containsB(s) =>
@@ -553,6 +554,7 @@ trait SMTLIBTarget {
FiniteArray(definedElements, Some(default), IntLiteral(size)).setType(at)
} else {
+ println("size is: " + size)
val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
FiniteArray(entries).setType(at)
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 57f5c314e..61eb37b36 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -35,6 +35,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
fd.precondition = {
val argTypesPreconditions = fd.params.flatMap(arg => arg.tpe match {
case cct : CaseClassType if cct.parent.isDefined => Seq(CaseClassInstanceOf(cct, arg.id.toVariable))
+ case (at : ArrayType) => Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
case _ => Seq()
})
argTypesPreconditions match {
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array3.scala b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
index 3145fb07f..b7be061e3 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array3.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
@@ -5,6 +5,7 @@ import leon.lang._
object Test {
def find(c: Array[Int], i: Int): Int = {
+ require(i >= 0)
if(c(i) == i)
42
else
--
GitLab