summaryrefslogtreecommitdiff
path: root/Test/dafny1/AnswerNoRuntimeChecking
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1/AnswerNoRuntimeChecking')
-rw-r--r--Test/dafny1/AnswerNoRuntimeChecking76
1 files changed, 76 insertions, 0 deletions
diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking
new file mode 100644
index 00000000..5472ec14
--- /dev/null
+++ b/Test/dafny1/AnswerNoRuntimeChecking
@@ -0,0 +1,76 @@
+
+-------------------- Queue --------------------
+Compiled assembly into Queue.dll
+
+-------------------- PriorityQueue --------------------
+Compiled assembly into PriorityQueue.dll
+
+-------------------- ExtensibleArray --------------------
+Compiled assembly into ExtensibleArray.exe
+
+-------------------- ExtensibleArrayAuto --------------------
+Compiled assembly into ExtensibleArrayAuto.exe
+
+-------------------- BinaryTree --------------------
+Compiled assembly into BinaryTree.dll
+
+-------------------- UnboundedStack --------------------
+Compiled assembly into UnboundedStack.dll
+
+-------------------- ListCopy --------------------
+Compilation error: an assume statement cannot be compiled (line 14)
+Compilation error: an assume statement cannot be compiled (line 15)
+
+-------------------- ListReverse --------------------
+Compiled assembly into ListReverse.dll
+
+-------------------- ListContents --------------------
+Compiled assembly into ListContents.dll
+
+-------------------- MatrixFun --------------------
+Compiled assembly into MatrixFun.exe
+
+-------------------- pow2 --------------------
+Compiled assembly into pow2.dll
+
+-------------------- SchorrWaite --------------------
+Compiled assembly into SchorrWaite.dll
+
+-------------------- Cubes --------------------
+Compiled assembly into Cubes.dll
+
+-------------------- SumOfCubes --------------------
+Compiled assembly into SumOfCubes.dll
+
+-------------------- FindZero --------------------
+Compiled assembly into FindZero.dll
+
+-------------------- TerminationDemos --------------------
+Compiled assembly into TerminationDemos.dll
+
+-------------------- Substitution --------------------
+Compiled assembly into Substitution.dll
+
+-------------------- KatzManna --------------------
+Compilation error: an assume statement cannot be compiled (line 66)
+
+-------------------- Induction --------------------
+Compiled assembly into Induction.dll
+
+-------------------- Rippling --------------------
+Compilation error: Arbitrary type ('FunctionValue') cannot be compiled
+
+-------------------- Celebrity --------------------
+Compilation error: Function _default._default.Knows has no body
+Compilation error: an assume statement cannot be compiled (line 16)
+
+-------------------- BDD --------------------
+Compiled assembly into BDD.dll
+
+-------------------- UltraFilter --------------------
+Compilation error: Method _default.UltraFilter.H has no body
+Compilation error: an assume statement cannot be compiled (line 42)
+Compilation error: an assume statement cannot be compiled (line 45)
+Compilation error: an assume statement cannot be compiled (line 76)
+Compilation error: an assume statement cannot be compiled (line 97)
+Compilation error: an assume statement cannot be compiled (line 98)