source: extracted/eRTL_semantics.mli @ 2829

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

Semantics files committed.

File size: 3.2 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
149open SemanticsUtils
150
151open ERTL
152
153type ertl_reg_env =
154  (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
155  Types.prod
156
157val ps_reg_store :
158  PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
159  (ByteValues.beval Identifiers.identifier_map,
160  SemanticsUtils.hw_register_env) Types.prod Errors.res
161
162val ps_reg_retrieve :
163  ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res
164
165val hw_reg_store :
166  I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
167  Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
168  Errors.res
169
170val hw_reg_retrieve :
171  ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res
172
173val ps_arg_retrieve :
174  ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
175  Errors.res
176
177val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res
178
179val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env
180
181val eRTL_state : Joint_semantics.sem_state_params
182
183val ertl_eval_move :
184  ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod ->
185  __
186
187val ertl_allocate_local :
188  PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
189  Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod
190
191val ertl_save_frame :
192  Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
193  Joint_semantics.state Errors.res
194
195val ertl_pop_frame :
196  Joint_semantics.state -> (Joint_semantics.state,
197  ByteValues.program_counter) Types.prod Errors.res
198
199val ertl_fetch_external_args :
200  AST.external_function -> Joint_semantics.state -> __ -> Values.val0
201  List.list Errors.res
202
203val ertl_set_result :
204  Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
205  Joint_semantics.state Errors.res
206
207val ps_reg_store_status :
208  Registers.register -> ByteValues.beval -> Joint_semantics.state ->
209  Joint_semantics.state Errors.res
210
211val eval_ertl_seq :
212  AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
213  AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res
214
215val eRTL_sem_uns : __ Joint_semantics.sem_unserialized_params
216
217val eRTL_semantics : SemanticsUtils.sem_graph_params
218
Note: See TracBrowser for help on using the repository browser.