99 open Hints_declaration
121 type registers_move =
122 | From_acc of I8051.register * Types.unit0
123 | To_acc of Types.unit0 * I8051.register
124 | Int_to_reg of I8051.register * BitVector.byte
125 | Int_to_acc of Types.unit0 * BitVector.byte
127 val registers_move_rect_Type4 :
128 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
129 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
130 BitVector.byte -> 'a1) -> registers_move -> 'a1
132 val registers_move_rect_Type5 :
133 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
134 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
135 BitVector.byte -> 'a1) -> registers_move -> 'a1
137 val registers_move_rect_Type3 :
138 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
139 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
140 BitVector.byte -> 'a1) -> registers_move -> 'a1
142 val registers_move_rect_Type2 :
143 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
144 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
145 BitVector.byte -> 'a1) -> registers_move -> 'a1
147 val registers_move_rect_Type1 :
148 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
149 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
150 BitVector.byte -> 'a1) -> registers_move -> 'a1
152 val registers_move_rect_Type0 :
153 (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
154 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
155 BitVector.byte -> 'a1) -> registers_move -> 'a1
157 val registers_move_inv_rect_Type4 :
158 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
159 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
160 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
163 val registers_move_inv_rect_Type3 :
164 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
165 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
166 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
169 val registers_move_inv_rect_Type2 :
170 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
171 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
172 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
175 val registers_move_inv_rect_Type1 :
176 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
177 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
178 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
181 val registers_move_inv_rect_Type0 :
182 registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
183 (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
184 BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
187 val registers_move_discr : registers_move -> registers_move -> __
189 val registers_move_jmdiscr : registers_move -> registers_move -> __
194 | LOW_ADDRESS of Graphs.label
195 | HIGH_ADDRESS of Graphs.label
197 val ltl_lin_seq_rect_Type4 :
198 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
201 val ltl_lin_seq_rect_Type5 :
202 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
205 val ltl_lin_seq_rect_Type3 :
206 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
209 val ltl_lin_seq_rect_Type2 :
210 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
213 val ltl_lin_seq_rect_Type1 :
214 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
217 val ltl_lin_seq_rect_Type0 :
218 'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
221 val ltl_lin_seq_inv_rect_Type4 :
222 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
223 (Graphs.label -> __ -> 'a1) -> 'a1
225 val ltl_lin_seq_inv_rect_Type3 :
226 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
227 (Graphs.label -> __ -> 'a1) -> 'a1
229 val ltl_lin_seq_inv_rect_Type2 :
230 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
231 (Graphs.label -> __ -> 'a1) -> 'a1
233 val ltl_lin_seq_inv_rect_Type1 :
234 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
235 (Graphs.label -> __ -> 'a1) -> 'a1
237 val ltl_lin_seq_inv_rect_Type0 :
238 ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
239 (Graphs.label -> __ -> 'a1) -> 'a1
241 val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __
243 val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __
245 val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list
247 val lTL_LIN_uns : Joint.unserialized_params
249 val lTL_LIN_functs : Joint.get_pseudo_reg_functs
251 val lTL_LIN : Joint.uns_params