From bae8c9aaad29eb554310474568a9ed3226021ab1 Mon Sep 17 00:00:00 2001 From: Marco Antognini Date: Mon, 30 Jan 2017 18:35:48 +0100 Subject: [PATCH] Fix typos --- .../scala/leon/genc/ir/Referentiator.scala | 2 +- .../genc/unverified/IntegralColor.scala | 49 +++++++++---------- 2 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/main/scala/leon/genc/ir/Referentiator.scala b/src/main/scala/leon/genc/ir/Referentiator.scala index 34e13ad25..80b3f813c 100644 --- a/src/main/scala/leon/genc/ir/Referentiator.scala +++ b/src/main/scala/leon/genc/ir/Referentiator.scala @@ -281,7 +281,7 @@ final class Referentiator(val ctx: LeonContext) extends Transformer(LIR, RIR) wi val isRef = typeInfos.head if (typeInfos exists { _ != isRef }) { fatalError(s"Cannot apply reference because of normalisation inconsistency on types. " + - s"Inciminated variable: ${vd.id}; Use `--debug=trees` option to learn why it failed.") + s"Incriminated variable: ${vd.id}; Use `--debug=trees` option to learn why it failed.") } lookingAhead = false diff --git a/src/test/resources/regression/genc/unverified/IntegralColor.scala b/src/test/resources/regression/genc/unverified/IntegralColor.scala index 28e7a23d3..0e859266d 100644 --- a/src/test/resources/regression/genc/unverified/IntegralColor.scala +++ b/src/test/resources/regression/genc/unverified/IntegralColor.scala @@ -19,7 +19,7 @@ object IntegralColor { rgb & 0x000000FF } ensuring isValidComponent _ - def getGray(rgb: Int): Int = { + def getGrey(rgb: Int): Int = { (getRed(rgb) + getGreen(rgb) + getBlue(rgb)) / 3 } ensuring isValidComponent _ @@ -27,7 +27,7 @@ object IntegralColor { val color = 0x20C0FF 32 == getRed(color) && 192 == getGreen(color) && - 255 == getBlue(color) && 159 == getGray(color) + 255 == getBlue(color) && 159 == getGrey(color) }.holds case class Color(r: Int, g: Int, b: Int) @@ -35,10 +35,9 @@ object IntegralColor { def getColor(rgb: Int) = Color(getRed(rgb), getGreen(rgb), getBlue(rgb)) /* - *case class Image(width: Int, height: Int, buffer: Array[Int]) { - * // currently not enforced: - * require(width <= 1000 && height <= 1000 && buffer.length == width * height) - *} + * case class Image(width: Int, height: Int, buffer: Array[Int]) { + * require(width <= 1024 && height <= 1024 && buffer.length == width * height) + * } */ def matches(value: Array[Int], expected: Array[Int]): Boolean = { @@ -60,38 +59,38 @@ object IntegralColor { /* *val source = Image(WIDTH, HEIGHT, Array(0x20c0ff, 0x123456, 0xffffff, 0x000000)) - *val expected = Image(WIDTH, HEIGHT, Array(159, 52, 255, 0)) // gray convertion - *val gray = Image(WIDTH, HEIGHT, Array.fill(4)(0)) + *val expected = Image(WIDTH, HEIGHT, Array(159, 52, 255, 0)) // grey convertion + *val grey = Image(WIDTH, HEIGHT, Array.fill(4)(0)) */ val source = Array(0x20c0ff, 0x123456, 0xffffff, 0x000000) - val expected = Array(159, 52, 255, 0) // gray convertion - val gray = Array.fill(4)(0) + val expected = Array(159, 52, 255, 0) // grey convertion + val grey = Array.fill(4)(0) - // NOTE: Cannot define a toGray function as XLang doesn't allow mutating + // NOTE: Cannot define a toGrey function as XLang doesn't allow mutating // arguments and GenC doesn't allow returning arrays var idx = 0 (while (idx < WIDTH * HEIGHT) { - gray(idx) = getGray(source(idx)) + grey(idx) = getGrey(source(idx)) idx = idx + 1 - }) invariant { idx >= 0 && idx <= WIDTH * HEIGHT && gray.length == WIDTH * HEIGHT } + }) invariant { idx >= 0 && idx <= WIDTH * HEIGHT && grey.length == WIDTH * HEIGHT } // NB: the last invariant is very important -- without it the verification times out - matches(gray, expected) + matches(grey, expected) }.holds // Only for square kernels case class Kernel(size: Int, buffer: Array[Int]) def isKernelValid(kernel: Kernel): Boolean = - kernel.size > 0 && kernel.size < 1000 && kernel.size % 2 == 1 && + kernel.size > 0 && kernel.size < 1024 && kernel.size % 2 == 1 && kernel.buffer.length == kernel.size * kernel.size - def applyFilter(gray: Array[Int], size: Int, idx: Int, kernel: Kernel): Int = { - require(size > 0 && size < 1000 && - gray.length == size * size && - idx >= 0 && idx < gray.length && + def applyFilter(grey: Array[Int], size: Int, idx: Int, kernel: Kernel): Int = { + require(size > 0 && size < 1024 && + grey.length == size * size && + idx >= 0 && idx < grey.length && isKernelValid(kernel)) def up(x: Int): Int = { @@ -110,7 +109,7 @@ object IntegralColor { val r = fix(row) val c = fix(col) - gray(r * size + c) + grey(r * size + c) } val mid = kernel.size / 2 @@ -144,7 +143,7 @@ object IntegralColor { } def testFilterConvolutionSmooth: Boolean = { - val gray = Array(127, 255, 51, 0) + val grey = Array(127, 255, 51, 0) val expected = Array(124, 158, 76, 73) val size = 2 // grey is size x size @@ -155,16 +154,16 @@ object IntegralColor { 1, 2, 1, 1, 1, 1)) - // val smoothed = Array.fill(gray.length)(0) // This is a VLA - assert(gray.length == 4) + // val smoothed = Array.fill(grey.length)(0) // This is a VLA + assert(grey.length == 4) val smoothed = Array.fill(4)(0) assert(smoothed.length == expected.length) var idx = 0; (while (idx < smoothed.length) { - smoothed(idx) = applyFilter(gray, size, idx, kernel) / 10 + smoothed(idx) = applyFilter(grey, size, idx, kernel) / 10 idx = idx + 1 - }) invariant { idx >= 0 && idx <= smoothed.length && smoothed.length == gray.length } + }) invariant { idx >= 0 && idx <= smoothed.length && smoothed.length == grey.length } matches(smoothed, expected) }.holds