Searched refs:mk_less_eq (Results 1 - 5 of 5) sorted by relevance

/seL4-l4v-10.1.1/graph-refine/
H A Dlogic.py15 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
142 mk_less_eq (min_stack_size, sp)]
151 preconds += [mk_aligned (r0, 2), mk_less_eq (sp, r0)]
161 preconds += [mk_less_eq (sp, addr)
183 preconds += [mk_less_eq (sp, addr)]
533 mk_less_eq (mk_plus (isize, offs), osize))
591 return mk_less_eq (num, mk_word32 (size_lim))
613 mk_less_eq (p, mk_uminus (size)))])
H A Dloop_bounds.py265 x_init_cmp1 = syntax.mk_less_eq (x, rew (x, minus_loop_step))
266 x_init_cmp2 = syntax.mk_less_eq (rew (x, minus_loop_step), x)
H A Dsyntax.py1351 def mk_less_eq (x, y, signed = False): function
1486 mk_eq, mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32,
H A Dpseudo_compile.py17 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
H A Dstack_logic.py22 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq namespace

Completed in 50 milliseconds