99 open Hints_declaration
154 I8051.register -> ByteValues.beval -> SemanticsUtils.hw_register_env ->
155 SemanticsUtils.hw_register_env Errors.res
157 val hw_reg_retrieve :
158 SemanticsUtils.hw_register_env -> I8051.register -> ByteValues.beval
161 val hw_arg_retrieve :
162 SemanticsUtils.hw_register_env -> I8051.register Joint.argument ->
163 ByteValues.beval Errors.res
165 val eval_registers_move :
166 SemanticsUtils.hw_register_env -> Joint_LTL_LIN.registers_move ->
167 SemanticsUtils.hw_register_env Errors.res
169 val lTL_LIN_state : Joint_semantics.sem_state_params
171 val ltl_lin_fetch_external_args :
172 AST.external_function -> Joint_semantics.state -> Nat.nat -> Values.val0
175 val ltl_lin_set_result :
176 Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
177 Joint_semantics.state Errors.res
179 val lTL_LIN_save_frame :
180 Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
181 Joint_semantics.state Errors.res
183 val eval_LTL_LIN_ext_seq :
184 AST.ident List.list -> 'a1 Joint_semantics.genv_gen ->
185 Joint_LTL_LIN.ltl_lin_seq -> AST.ident -> Joint_semantics.state ->
186 Joint_semantics.state Errors.res
188 val lTL_LIN_semantics : __ Joint_semantics.sem_unserialized_params