Searched refs:builtinTs (Results 1 - 8 of 8) sorted by last modified time
/seL4-l4v-10.1.1/graph-refine/ |
H A D | syntax.py | 881 builtinTs = mk_builtinTs () variable 882 boolT = builtinTs['Bool'] 888 phantom_types = set ([builtinTs[t] for t 926 elif bits[n] in builtinTs: 927 return (n + 1, builtinTs[bits[n]]) 1067 return (n, Expr ('Type', builtinTs['Type'], val = typ)) 1302 rm = builtinTs['RoundingMode'] 1316 return Expr ('Token', builtinTs['Token'], name = nm) 1440 assert m.typ == builtinTs['Mem'] 1445 assert m.typ == builtinTs['Me [all...] |
H A D | stack_logic.py | 22 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq namespace 293 syntax.builtinTs['Mem']), r) 1004 from syntax import mk_var, word32T, builtinTs namespace 1009 st = mk_var ('stack', builtinTs['Mem']) 1012 mem = mk_var ('mem', builtinTs['Mem']) 1013 dom = mk_var ('dom', builtinTs['Dom']) 1014 dom_stack = mk_var ('dom_stack', builtinTs['Dom']) 1265 if not (nm.startswith ('stack') and typ == syntax.builtinTs['Mem']): 1284 if typ in [builtinTs['Mem'], builtinTs['Do [all...] |
H A D | solver.py | 177 from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, namespace 262 smt_typs_omitted = set ([builtinTs['HTD'], builtinTs['PMS']]) 384 elif expr.is_op ('Equals') and expr.vals[0].typ == builtinTs['Mem']: 468 memT = syntax.builtinTs['Mem'] 512 if expr.typ == builtinTs['RelWrapper']: 519 return (typ.kind == 'Word' or typ == builtinTs['Bool'] 520 or typ == builtinTs['Token']) 895 if typ == builtinTs['Mem'] and mem_name != None: 973 smt_typ (builtinTs['Me [all...] |
H A D | search.py | 17 foldr1, boolT, word32T, word8T, builtinTs, true_term, false_term, 621 if group[0][0][0].typ == syntax.builtinTs['Mem']: 1061 mem_vs = [v for v in knowledge.v_ids if v[0].typ == builtinTs['Mem']] 1357 if with_rodata and var.typ == builtinTs['Mem']: 1379 if v.typ == builtinTs['Mem']
|
H A D | rep_graph.py | 11 builtinTs, word32T, word8T, foldr1, mk_eq, mk_plus, mk_word32, mk_var) 432 [builtinTs['HTD'], builtinTs['Dom']]) 622 if typ == syntax.builtinTs['Mem']: 634 assert typ == builtinTs['Mem'] 700 if typ == builtinTs['Mem']: 901 if typ == syntax.builtinTs['Mem']] 1146 if x.typ == syntax.builtinTs['RelWrapper']: 1197 if typ == syntax.builtinTs['Mem']]: 1257 if x.typ.kind == 'Word' or x.typ == syntax.builtinTs['Me [all...] |
H A D | problem.py | 10 fresh_name, word32T, word8T, mk_eq, mk_word32, builtinTs)
|
H A D | logic.py | 10 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node namespace 29 assert m.typ == builtinTs['Mem'] 48 if v.typ not in [builtinTs['Mem'], builtinTs['Dom'], 49 builtinTs['HTD'], builtinTs['PMS'], 52 memT = builtinTs['Mem'] 135 st = mk_var ('stack', builtinTs['Mem']) 175 mem = mk_var ('mem', builtinTs['Mem']) 1534 assert lhs.typ == syntax.builtinTs['RelWrappe [all...] |
H A D | inst_logic.py | 51 bin_globs = [('mem', syntax.builtinTs['Mem'])] 52 asm_globs = [('Mem', syntax.builtinTs['Mem'])] 88 ident_v = ("inst_ident", syntax.builtinTs['Token'])
|
Completed in 53 milliseconds