-
Notifications
You must be signed in to change notification settings - Fork 1
/
FanPeriodic_p_tcproc_fan_GumboX_UnitTests.scala
93 lines (75 loc) · 2.63 KB
/
FanPeriodic_p_tcproc_fan_GumboX_UnitTests.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
package tc.CoolingFan
import org.sireum._
import tc.GumboXUtil.GumboXResult
import tc.util.{Container, UnitTestConfigurationBatch}
import tc.CoolingFan.FanPeriodic_p_tcproc_fan_UnitTestConfiguration_Util._
// This file will not be overwritten so is safe to edit
class FanPeriodic_p_tcproc_fan_GumboX_UnitTests extends FanPeriodic_p_tcproc_fan_GumboX_TestHarness_ScalaTest {
// set verbose to T to see pre/post state values and generated unit tests
// that can be copied/pasted to replay a test
val verbose: B = F
// set failOnUnsatPreconditions to T if the unit tests should fail when either
// SlangCheck is never able to satisfy a datatype's filter or the generated
// test vectors are never able to satisfy an entry point's assume pre-condition
val failOnUnsatPreconditions: B = F
def configs: MSZ[UnitTestConfigurationBatch] = {
return MSZ(
defaultComputeConfig(verbose = verbose, failOnUnsatPreconditions = failOnUnsatPreconditions)
)
}
for (c <- configs) {
def next: Option[Container] = {
try {
return Some(c.profile.next)
} catch {
case e: AssertionError => // SlangCheck was unable to satisfy a datatype's filter
return None()
}
}
for (i <- 0 until c.numTests) {
val testName = s"${c.name}_$i"
this.registerTest(testName) {
var retry: B = T
var j: Z = 0
while (j < c.numTestVectorGenRetries && retry) {
next match {
case Some(o) =>
if (verbose && j > 1) {
println(s"Retry $j:")
}
val results = c.test(o)
if (verbose) {
c.genReplay(o, testName, results) match {
case Some(s) => println(s)
case _ =>
}
}
results match {
case GumboXResult.Pre_Condition_Unsat =>
case GumboXResult.Post_Condition_Fail =>
fail("Post condition did not hold")
retry = F
case GumboXResult.Post_Condition_Pass =>
if (verbose) {
println("Success!")
}
retry = F
}
case _ =>
}
j = j + 1
}
if (retry) {
if (c.failOnUnsatPreconditions) {
fail("Unable to satisfy precondition")
} else if (verbose) {
cprintln(T, "Unable to satisfy precondition")
}
}
}
}
}
def configsToJson: String = {
return st"[ ${(for (c <- configs) yield s"\"${c.name}|${c.description}\"", ", ")} ]".render
}
}