Searched refs:builtinTs (Results 1 - 8 of 8) sorted by last modified time

/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py881 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 Dstack_logic.py22 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 Dsolver.py177 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 Dsearch.py17 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 Drep_graph.py11 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 Dproblem.py10 fresh_name, word32T, word8T, mk_eq, mk_word32, builtinTs)
H A Dlogic.py10 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 Dinst_logic.py51 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