summaryrefslogtreecommitdiff
path: root/Test/dafny1/AnswerNoRuntimeChecking
blob: 5472ec14144a6428bbd35727c8c74cd01ead360e (plain)
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

-------------------- 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)