133 open Hints_declaration
154 (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
158 PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
159 (ByteValues.beval Identifiers.identifier_map,
160 SemanticsUtils.hw_register_env) Types.prod Errors.res
162 val ps_reg_retrieve :
163 ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res
166 I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
167 Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
170 val hw_reg_retrieve :
171 ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res
173 val ps_arg_retrieve :
174 ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
177 val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res
179 val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env
181 val eRTL_state : Joint_semantics.sem_state_params
184 ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod ->
187 val ertl_allocate_local :
188 PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
189 Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod
191 val ertl_save_frame :
192 Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
193 Joint_semantics.state Errors.res
196 Joint_semantics.state -> (Joint_semantics.state,
197 ByteValues.program_counter) Types.prod Errors.res
199 val ertl_fetch_external_args :
200 AST.external_function -> Joint_semantics.state -> __ -> Values.val0
203 val ertl_set_result :
204 Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
205 Joint_semantics.state Errors.res
207 val ps_reg_store_status :
208 Registers.register -> ByteValues.beval -> Joint_semantics.state ->
209 Joint_semantics.state Errors.res
212 AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
213 AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res
215 val eRTL_sem_uns : __ Joint_semantics.sem_unserialized_params
217 val eRTL_semantics : SemanticsUtils.sem_graph_params