seL4-l4v-10.1.1/graph-refine/syntax.py

374 class Expr:
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 ('Op', typ, name = op, vals = xs))
1067 		return (n, Expr ('Type', builtinTs['Type'], val = typ))
1099 true_term = Expr ('Op', boolT, name = 'True', vals = [])
1100 false_term = Expr ('Op', boolT, name = 'False', vals = [])
1101 unspecified_precond_term = Expr ('Op', boolT, name = 'UnspecifiedPrecond', vals = [])
1313 	return Expr ('Var', typ, name = nm)
1316 	return Expr ('Token', builtinTs['Token'], name = nm)
1320 	return Expr ('Op', x.typ, name = 'Plus', vals = [x, y])
1323 	zero = Expr ('Num', x.typ, val = 0)
1328 	return Expr ('Op', x.typ, name = 'Minus', vals = [x, y])
1332 	return Expr ('Op', x.typ, name = 'Times', vals = [x, y])
1336 	return Expr ('Op', x.typ, name = 'DividedBy', vals = [x, y])
1340 	return Expr ('Op', x.typ, name = 'Modulus', vals = [x, y])
1345 	return Expr ('Op', x.typ, name = 'BWAnd', vals = [x, y])
1349 	return Expr ('Op', boolT, name = 'Equals', vals = [x, y])
1354 	return Expr ('Op', boolT, name = name, vals = [x, y])
1359 	return Expr ('Op', boolT, name = name, vals = [x, y])
1364 	return Expr ('Op', boolT, name = 'Implies', vals = [x, y])
1375 	return Expr ('Op', boolT, name = 'And', vals = [x, y])
1380 	return Expr ('Op', boolT, name = 'Or', vals = [x, y])
1384 	return Expr ('Op', boolT, name = 'Not', vals = [x])
1389 		n = Expr ('Num', x.typ, val = n)
1390 	return Expr ('Op', x.typ, name = name, vals = [x, n])
1395 	return Expr ('Op', x.typ, name = "CountLeadingZeroes", vals = [x])
1398 	return Expr ('Op', x.typ, name = "WordReverse", vals = [x])
1415 	return Expr ('Num', typ, val = x)
1437 		return Expr ('Op', typ, name = 'WordCast', vals = [x])
1442 	return Expr ('Op', typ, name = 'MemAcc', vals = [m, p])
1447 	return Expr ('Op', m.typ, name = 'MemUpdate', vals = [m, p, v])
1451 	return Expr ('Op', arr.typ.el_typ, name = 'ArrayIndex',
1469 	return Expr ('Op', x.typ, name = 'IfThenElse', vals = [P, x, y])
1472 	return Expr ('Type', builtinTs['Type'], val = typ)
1475 	return Expr ('Op', boolT, name = 'PValid',
1479 	return Expr ('Op', builtinTs['RelWrapper'], name = nm, vals = vals)
1483 	return Expr ('Op', expr.typ, expr.name, vals = vals)