Searched refs:mk_word8 (Results 1 - 10 of 10) sorted by path
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | instructionSyntax.sml | 29 val mk_word8 = mk_word ``:8``; value
95 ``m:word8`` |-> mk_word8 m] ``Dp_immediate n m``
203 subst [``i:word8`` |-> mk_word8 (Arbnum.fromInt n)] ``Dth_immediate i``
298 ``m:word8`` |-> mk_word8 m] ``Msr_immediate n m``
369 ``offset:word8`` |-> mk_word8 (Arbnum.fromInt (#offset y))]
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_parserLib.sml | 416 fun mk_word8 i = wordsSyntax.mk_wordii (i,8); function
2025 of [] => mk_word8 0
2911 mk_Load_Exclusive (rn,rt,mk_word8 (Int.abs (v div 4)))))
2916 return (enc, mk_Load_Exclusive (rn,rt,mk_word8 0)))))));
2940 (rn,rd,rt,mk_word8 (Int.abs (v div 4)))))
2945 return (enc, mk_Store_Exclusive (rn,rd,rt,mk_word8 0))))))));
3947 mk_word8 (Int.abs (v div 4))))
3958 (fn _ => return (T,T,F,mk_word8 0)))
3970 mk_word8 (Int.abs (v div 4))))
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
| H A D | arm_evalLib.sml | 35 val mk_word8 = mk_word 8; value
92 let fun ss i = mk_word8 (String.substring (s,i,2)) in
433 of SOME tm => mk_word8 tm
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/ |
| H A D | MultScript.sml | 118 fun mk_word8 i = wordsSyntax.mk_n2w(numSyntax.term_of_int i, ``:8``); function
126 fn i => let val y = mk_word8 i in eval_mult ``^x ** ^y`` end))
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/AES/word8/ |
| H A D | MultScript.sml | 126 fun mk_word8 i = wordsSyntax.mk_n2w(numSyntax.term_of_int i, ``:8``); function
134 fn i => let val y = mk_word8 i in eval_mult ``^x ** ^y`` end))
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | check.py | 23 from syntax import (true_term, false_term, boolT, mk_var, mk_word32, mk_word8, namespace
|
| H A D | logic.py | 15 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
|
| H A D | pseudo_compile.py | 17 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
|
| H A D | search.py | 18 mk_word32, mk_word8, mk_times, Expr, Type, mk_or, mk_eq, mk_memacc,
538 result = syntax.mk_word8 (v)
|
| H A D | syntax.py | 1420 def mk_word8 (x): function
1487 mk_word8, mk_word32_maybe, mk_cast, mk_memacc, mk_memupd, mk_arr_index,
|
Completed in 119 milliseconds