Searched refs:mk_num (Results 1 - 6 of 6) sorted by path
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 643 val mk_num = numSyntax.mk_numeral o Arbnum.fromInt value 645 subst [mk_var("n",``:num``) |-> mk_num i] ``p + (n2w n):word32`` 647 val xs = zip (map mk_num (foo entry 0)) (map mk_pos entry) 1813 val mk_num = numSyntax.mk_numeral o Arbnum.fromInt value 1814 val th = SIMP_RULE std_ss [] (INST [mk_var("pos",``:num``) |-> mk_num k] th)
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Prim_rec.sml | 1648 mk_num generates the function corresponding to number n. The abstraction 1651 fun mk_num numbits n = let function 1737 (mk_comb(f, x) == mk_num nb n):: recurse (n + 1) xs
|
/seL4-l4v-master/graph-refine/ |
H A D | logic.py | 9 from syntax import true_term, false_term, mk_num namespace 126 return mk_eq (mk_bwand (w, mask), mk_num (0, w.typ)) 436 return mk_bwand (expr, mk_num (((1 << n) - 1), expr.typ)) 1113 arg_offs.append (syntax.mk_num (0, expr2.typ)) 1202 return mk_num (0, expr.typ)
|
H A D | search.py | 17 mk_num, mk_minus, mk_plus, mk_less) 496 result = mk_num (val, x.typ.num + n_extend) 504 result = mk_num ((x.val >> n_bot) & ((1 << length) - 1), length) 896 eq = mk_eq (mk_times (offs_smt, mk_num (4, offs_smt.typ)), 897 mk_num (0, offs_smt.typ)) 1470 zero = mk_num (0, lhs.typ) 1582 const_less = lambda n: mk_less (const, mk_num (n, const.typ)) 1585 const_ge = lambda n: mk_less (mk_num (n, const.typ), const)
|
H A D | solver.py | 1807 syntax.mk_num (n, token_smt_typ), {}) 2003 return syntax.mk_num (n, ln) 2007 return syntax.mk_num (int (s[2:], 2), len (s) - 2) 2009 return syntax.mk_num (int (s[2:], 16), (len (s) - 2) * 4)
|
H A D | syntax.py | 1411 def mk_num (x, typ): function 1420 return mk_num (x, word32T) 1423 return mk_num (x, word8T)
|
Completed in 103 milliseconds