Skip to content

Commit

Permalink
Fix typos
Browse files Browse the repository at this point in the history
  • Loading branch information
mantognini committed Feb 13, 2017
1 parent 5e84253 commit bae8c9a
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 26 deletions.
2 changes: 1 addition & 1 deletion src/main/scala/leon/genc/ir/Referentiator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
49 changes: 24 additions & 25 deletions src/test/resources/regression/genc/unverified/IntegralColor.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,26 +19,25 @@ 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 _

def testColorSinglePixel: Boolean = {
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)

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 = {
Expand All @@ -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 = {
Expand All @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down

0 comments on commit bae8c9a

Please sign in to comment.