| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | syntax.py | 883 word32T = Type ('Word', '32') variable
893 return word32T
938 return (n, word32T)
1200 assert p.typ == word32T, expr
1418 return mk_num (x, word32T)
1428 assert x.typ == word32T
1441 assert p.typ == word32T
1446 assert p.typ == word32T
|
| H A D | stack_logic.py | 22 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq namespace
116 cache = None, typ = syntax.word32T):
266 sp = mk_var ('r13', syntax.word32T)
291 sp = syntax.rename_expr (mk_var ('r13', syntax.word32T), r)
365 elif expr.typ == syntax.word32T:
368 assert expr.typ == syntax.word32T, expr
381 v = mk_var (('Fake', k, offs), syntax.word32T)
407 syntax.word32T), v2))
420 assert expr.typ == syntax.word32T, expr
424 r = (('Fake', k, offs), syntax.word32T)
1004 from syntax import mk_var, word32T, builtinTs namespace
[all...] |
| H A D | solver.py | 178 foldr1, mk_or, boolT, word32T, word8T, mk_implies, Type, get_global_wrapper)
392 elif expr.is_op ('Equals') and expr.vals[0].typ == word32T:
450 p = solv.cache_large_expr (p, 'memacc_pointer', syntax.word32T)
459 solv.note_model_expr (p, syntax.word32T)
465 p = solv.cache_large_expr (p, 'memupd_pointer', syntax.word32T)
477 p = solv.cache_large_expr (p, 'memupd_pointer', syntax.word32T)
479 solv.note_model_expr (p_align, syntax.word32T)
481 syntax.word32T)
486 solv.note_model_expr (p, syntax.word32T)
921 split = add ('split', syntax.word32T, spli
[all...] |
| H A D | search.py | 17 foldr1, boolT, word32T, word8T, builtinTs, true_term, false_term,
1349 loop = mk_var ('%i', word32T)
|
| H A D | rep_graph.py | 11 builtinTs, word32T, word8T, foldr1, mk_eq, mk_plus, mk_word32, mk_var)
1060 word32T)
1065 return mk_smt_expr (vname, word32T)
1156 substs = {('%n', word32T): induct_var}
|
| H A D | pseudo_compile.py | 21 from syntax import word32T, word8T namespace
61 assert i.typ == word32T
|
| H A D | problem.py | 10 fresh_name, word32T, word8T, mk_eq, mk_word32, builtinTs)
|
| H A D | loop_bounds.py | 255 loop = syntax.mk_var ('%i', syntax.word32T)
|
| H A D | logic.py | 10 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node namespace
132 arg_regs = mk_var_list (['r0', 'r1', 'r2', 'r3'], word32T)
134 sp = mk_var ('r13', word32T)
136 r0_input = mk_var ('r0_input', word32T)
137 sregs = mk_stack_sequence (sp, 4, st, word32T, len (var_c_args) + 1)
139 ret = mk_var ('ret', word32T)
140 preconds = [mk_aligned (sp, 2), mk_eq (ret, mk_var ('r14', word32T)),
144 'r9', 'r10', 'r11', 'r13'], word32T)]
152 save_seq = mk_stack_sequence (r0_input, 4, st, word32T,
158 init_save_seq = mk_stack_sequence (r0, 4, st, word32T,
[all...] |
| H A D | inst_logic.py | 57 [(nm, syntax.word32T) for nm in word_args] + ex_args + globs,
58 [(nm, syntax.word32T) for nm in word_rets] + ex_rets + globs)
140 [syntax.mk_var (reg, syntax.word32T) for reg in inp_regs]
143 [(reg, syntax.word32T) for reg in out_regs] + bin_globs))
|
| H A D | check.py | 24 mk_plus, mk_minus, word32T, word8T, mk_and, mk_eq, mk_implies, mk_not,
252 word32T.serialise (ss)
263 assert typ == word32T, typ
398 return lambda exp: logic.var_subst (exp, {('%i', word32T) : v},
406 lsub = mksub (mk_plus (mk_var ('%n', word32T),
575 return lambda exp: logic.var_subst (exp, {('%i', word32T) : v},
581 isub = mksub (mk_plus (mk_var ('%n', word32T),
630 return eq_hyp ((mk_var ('%n', word32T), visit),
810 v = syntax.mk_var ('#seq-visits', word32T)
811 t = logic.var_subst (t, {('%i', word32T)
[all...] |