summaryrefslogtreecommitdiff
path: root/test/coq/skip
blob: 7a233ddc1ccb8eb6da714b651950d6da6230d645 (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
XXXXX tests with deliberate redundant pattern match clause
option_tuple.sail
pat_completeness.sail
XXXXX tests which need inline extern definitions adjusted
patternrefinement.sail
vector_subrange_gen.sail
XXXXX unsupported existential quantification of a vector length
bind_typ_var.sail
XXXXX needs some smart existential instantiation
complex_exist_sat.sail
XXXXX needs name collision avoidance due to type/constructor punning
constraint_ctor.sail
XXXXX Complex existential type - probably going to need this for ARM instruction ASTs
execute_decode_hard.sail
existential_ast.sail
existential_ast3.sail
XXXXX Needs an existential witness
exist1.sail
exist2.sail
XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere
exist_synonym.sail
XXXXX Examples where int(...) should be expanded internally, but not yet supported
exit1.sail
exit2.sail
inline_typ.sail
XXXXX Examples with exponentials that the solver can't handle
pow_32_64.sail
XXXXX Register constructor doesn't use expanded type from type checker - need environment for type definition to fix this easily
reg_mod.sail
reg_ref.sail
XXXXX Dodgy division/modulo stuff
Replicate.sail
XXXXX Non-terminating loops - I've written terminating versions of these
while_MM.sail
while_MP.sail
while_PM.sail
while_PP.sail
XXXXX Non-terminating loop that's only really useful for the type checking tests
repeat_constraint.sail
XXXXX Not yet - haven't decided whether to support register reads in measures
while_MM_terminating.sail
XXXXX TODO, add termination measure
floor_pow2.sail