99 open Hints_declaration
123 val lTL : Joint.graph_params
125 type ltl_program = Joint.joint_program
127 val dpi1__o__byte_to_ltl_argument__o__inject :
128 (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0
130 val eject__o__byte_to_ltl_argument__o__inject :
131 BitVector.byte Types.sig0 -> Joint.hdw_argument Types.sig0
133 val byte_to_ltl_argument__o__inject :
134 BitVector.byte -> Joint.hdw_argument Types.sig0
136 val dpi1__o__byte_to_ltl_argument :
137 (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument
139 val eject__o__byte_to_ltl_argument :
140 BitVector.byte Types.sig0 -> Joint.hdw_argument
142 val dpi1__o__reg_to_ltl_argument__o__inject :
143 (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0
145 val eject__o__reg_to_ltl_argument__o__inject :
146 I8051.register Types.sig0 -> Joint.hdw_argument Types.sig0
148 val reg_to_ltl_argument__o__inject :
149 I8051.register -> Joint.hdw_argument Types.sig0
151 val dpi1__o__reg_to_ltl_argument :
152 (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument
154 val eject__o__reg_to_ltl_argument :
155 I8051.register Types.sig0 -> Joint.hdw_argument
157 val lTL_premain : ltl_program -> Joint.joint_closed_internal_function