Context Navigation

abstractStatus.mli @ 3106

Last change on this file since 3106 was 3106, checked in by sacerdot, 7 years ago
New extraction.
File size: 1.3 KB

Line
1	open Preamble
2
3	open Hide
4
5	open Integers
6
7	open AST
8
9	open Division
10
11	open Exp
12
13	open Arithmetic
14
15	open Extranat
16
17	open Vector
18
19	open FoldStuff
20
21	open BitVector
22
23	open Z
24
25	open BitVectorZ
26
27	open Pointers
28
29	open Coqlib
30
31	open Values
32
33	open Events
34
35	open IOMonad
36
37	open IO
38
39	open Sets
40
41	open Listb
42
43	open Proper
44
45	open PositiveMap
46
47	open Deqsets
48
49	open ErrorMessages
50
51	open PreIdentifiers
52
53	open Errors
54
55	open Extralib
56
57	open Setoids
58
59	open Monad
60
61	open Option
62
63	open Div_and_mod
64
65	open Russell
66
67	open Util
68
69	open List
70
71	open Lists
72
73	open Nat
74
75	open Positive
76
77	open Types
78
79	open Identifiers
80
81	open CostLabel
82
83	open Jmeq
84
85	open Hints_declaration
86
87	open Core_notation
88
89	open Pts
90
91	open Logic
92
93	open Relations
94
95	open Bool
96
97	open StructuredTraces
98
99	open BitVectorTrie
100
101	open String
102
103	open LabelledObjects
104
105	open ASM
106
107	open Status
108
109	open Fetch
110
111	val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class
112
113	val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
114
115	val current_instruction :
116	BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
117	ASM.instruction
118
119	val current_instruction_label :
120	BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
121	Status.status -> CostLabel.costlabel Types.option
122
123	val word_deqset : Deqsets.deqSet
124
125	val oC_classify :
126	BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
127	StructuredTraces.status_class
128

Note: See TracBrowser for help on using the repository browser.