| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | logic.py | 10 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node namespace
30 return Expr ('Op', boolT, name = 'ROData', vals = [m])
118 return Expr ('Num', init.typ, val = offs * n)
127 mask = Expr ('Num', w.typ, val = ((1 << n) - 1))
335 return Expr ('Num', typ, val = 0)
453 typ/typ2 is ('Type', syntax.Type) or ('Array', Type, Expr) for
990 return (s, Expr ('Op', expr.typ,
1546 return syntax.Expr ('Op', boolT, name = 'StackEquals',
1598 return syntax.Expr ('Op', boolT,
1601 return syntax.Expr ('O
[all...] |
| H A D | loop_bounds.py | 6 from syntax import mk_not, true_term, false_term, mk_implies, Expr, Type, unspecified_precond_term,mk_and namespace
|
| H A D | problem.py | 9 from syntax import (Expr, mk_var, Node, true_term, false_term, namespace
|
| H A D | pseudo_compile.py | 12 from syntax import structs, get_vars, get_expr_typ, get_node_vars, Expr, Node namespace
|
| H A D | search.py | 18 mk_word32, mk_word8, mk_times, Expr, Type, mk_or, mk_eq, mk_memacc,
544 result = Expr ('Num', xs[0].typ, val = result)
|
| H A D | solver.py | 177 from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, namespace
292 return Expr ('SMTExpr', typ, val = smt_expr)
|
| H A D | stats.py | 3 from syntax import Expr, Type namespace
|
| H A D | syntax.py | 374 class Expr: class in inherits:
421 return 'Expr (%s)' % ', '.join(bits)
491 self = Expr ('Op', self.typ, name = self.name,
1026 return (n, Expr (kind, typ, name = name))
1032 return (n, Expr ('Array', typ, vals = xs))
1039 return (n, Expr ('Field', typ2, struct = struct,
1047 return (n, Expr ('FieldUpd', typ, struct = struct,
1052 return (n, Expr ('StructCons', typ, vals = dict(xs)))
1056 return (n, Expr ('Num', typ, val = v))
1064 return (n, Expr ('O
[all...] |