Lines Matching defs:check
89 fun check (f,m) b = (b () orelse raise ERR f (term_to_string m); I);
91 fun check_is_15 s tm = check (s,tm) (fn _ => is_PC tm);
157 check ("encode_mode3", tm) (fn _ => width_okay 8 imm12)
160 check ("encode_mode3", tm) (fn _ => is_0 imm2)
233 check ("encode_branch", tm) (fn _ => is_T toarm orelse is_PC cond)
252 check ("encode_data_processing", tm) (fn _ => check_dp (opc,d,n))
383 check ("encode_load_store", tm) (fn _ => is_0 imm8)
387 check ("encode_load_store", tm) (fn _ => is_0 imm8)
422 check ("encode_miscellaneous", pairSyntax.mk_pair (cond,tm))
478 let val checkbr = check ("thumb_encode_branch", tm) in
507 check ("thumb_encode_register", mode1)
520 let val checkdp = check ("thumb_encode_data_processing",tm) in
699 check ("encode_status_access", tm) (fn _ => optionSyntax.is_none mode)
708 let val checkls = check ("thumb_encode_load_store",tm) in
848 let val checkmisc = check ("thumb_encode_miscellaneous",tm) in
869 let val checkb = check ("thumb2_encode_branch", tm)
941 let val checkdp = check ("thumb2_encode_data_processing",tm) in
1093 let val checkls = check ("thumb2_encode_load_store",tm) in
1239 let val checkmisc = check ("thumb2_encode_miscellaneous",tm) in
1299 let val checkbr = check ("thumbee_encode_branch", tm) in
1315 let val checkls = check ("thumbee_encode_load_store",tm) in