| /seL4-l4v-master/graph-refine/ |
| H A D | logic.py | 8 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node namespace
28 return Expr ('Op', boolT, name = 'ROData', vals = [m])
116 return Expr ('Num', init.typ, val = offs * n)
125 mask = Expr ('Num', w.typ, val = ((1 << n) - 1))
333 return Expr ('Num', typ, val = 0)
451 typ/typ2 is ('Type', syntax.Type) or ('Array', Type, Expr) for
988 return (s, Expr ('Op', expr.typ,
1544 return syntax.Expr ('Op', boolT, name = 'StackEquals',
1596 return syntax.Expr ('Op', boolT,
1599 return syntax.Expr ('O
[all...] |
| H A D | loop_bounds.py | 12 from syntax import mk_not, true_term, false_term, mk_implies, Expr, Type, unspecified_precond_term,mk_and namespace
|
| H A D | problem.py | 7 from syntax import (Expr, mk_var, Node, true_term, false_term, namespace
|
| H A D | pseudo_compile.py | 10 from syntax import structs, get_vars, get_expr_typ, get_node_vars, Expr, Node namespace
|
| H A D | search.py | 16 mk_word32, mk_word8, mk_times, Expr, Type, mk_or, mk_eq, mk_memacc,
542 result = Expr ('Num', xs[0].typ, val = result)
|
| H A D | solver.py | 175 from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, namespace
290 return Expr ('SMTExpr', typ, val = smt_expr)
|
| H A D | stats.py | 9 from syntax import Expr, Type namespace
|
| H A D | syntax.py | 372 class Expr: class in inherits:
419 return 'Expr (%s)' % ', '.join(bits)
489 self = Expr ('Op', self.typ, name = self.name,
1024 return (n, Expr (kind, typ, name = name))
1030 return (n, Expr ('Array', typ, vals = xs))
1037 return (n, Expr ('Field', typ2, struct = struct,
1045 return (n, Expr ('FieldUpd', typ, struct = struct,
1050 return (n, Expr ('StructCons', typ, vals = dict(xs)))
1054 return (n, Expr ('Num', typ, val = v))
1062 return (n, Expr ('O
[all...] |