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