From c89d4dbf1c5a1478e4e30fcbd5e2f41200c8e6eb Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Tue, 24 Nov 2015 11:13:56 +0100
Subject: [PATCH] Fix documentation and C conversion of BVAShiftRight and
BVLShiftRight
---
src/main/scala/leon/genc/CConverter.scala | 4 ++--
src/main/scala/leon/purescala/Expressions.scala | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index 9ccad62cd..c4c606f37 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -368,8 +368,8 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
case BVOr(lhs, rhs) => buildBinOp(lhs, "|", rhs)
case BVXOr(lhs, rhs) => buildBinOp(lhs, "^", rhs)
case BVShiftLeft(lhs, rhs) => buildBinOp(lhs, "<<", rhs)
- case BVAShiftRight(lhs, rhs) => buildBinOp(lhs, ">>>", rhs)
- case BVLShiftRight(lhs, rhs) => buildBinOp(lhs, ">>", rhs)
+ case BVAShiftRight(lhs, rhs) => buildBinOp(lhs, ">>", rhs)
+ case BVLShiftRight(lhs, rhs) => fatalError("operator >>> not supported")
// Ignore assertions for now
case Ensuring(body, _) => convert(body)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 13e4efbef..50efdf406 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -725,11 +725,11 @@ object Expressions {
case class BVShiftLeft(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
- /** $encodingof `... >>> ...` $noteBitvector (logical shift) */
+ /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */
case class BVAShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
- /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */
+ /** $encodingof `... >>> ...` $noteBitvector (logical shift) */
case class BVLShiftRight(lhs: Expr, rhs: Expr) extends Expr {
val getType = Int32Type
}
--
GitLab