source: extracted/joint_fullexec.mli @ 2960

Last change on this file since 2960 was 2960, checked in by sacerdot, 7 years ago

New extraction, it diverges in RTL execution now.

File size: 1.5 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open ExtraMonads
6
7open Deqsets_extra
8
9open State
10
11open Bind_new
12
13open BindLists
14
15open Blocks
16
17open TranslateUtils
18
19open ExtraGlobalenvs
20
21open I8051bis
22
23open String
24
25open Sets
26
27open Listb
28
29open LabelledObjects
30
31open BitVectorTrie
32
33open Graphs
34
35open I8051
36
37open Order
38
39open Registers
40
41open BackEndOps
42
43open Joint
44
45open BEMem
46
47open CostLabel
48
49open Events
50
51open IOMonad
52
53open IO
54
55open Extra_bool
56
57open Coqlib
58
59open Values
60
61open FrontEndVal
62
63open Hide
64
65open ByteValues
66
67open Division
68
69open Z
70
71open BitVectorZ
72
73open Pointers
74
75open GenMem
76
77open FrontEndMem
78
79open Proper
80
81open PositiveMap
82
83open Deqsets
84
85open Extralib
86
87open Lists
88
89open Identifiers
90
91open Exp
92
93open Arithmetic
94
95open Vector
96
97open Div_and_mod
98
99open Util
100
101open FoldStuff
102
103open BitVector
104
105open Extranat
106
107open Integers
108
109open AST
110
111open ErrorMessages
112
113open Option
114
115open Setoids
116
117open Monad
118
119open Jmeq
120
121open Russell
122
123open Positive
124
125open PreIdentifiers
126
127open Bool
128
129open Relations
130
131open Nat
132
133open List
134
135open Hints_declaration
136
137open Core_notation
138
139open Pts
140
141open Logic
142
143open Types
144
145open Errors
146
147open Globalenvs
148
149open Joint_semantics
150
151open SemanticsUtils
152
153open Traces
154
155open Stacksize
156
157open SmallstepExec
158
159open Executions
160
161open Measurable
162
163val joint_exec :
164  Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
165  SmallstepExec.trans_system
166
167val joint_fullexec :
168  Joint_semantics.sem_params -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
169
170val joint_preclassified_system :
171  Joint_semantics.sem_params -> Measurable.preclassified_system
172
Note: See TracBrowser for help on using the repository browser.