Searched refs:mk_less_eq (Results 1 - 5 of 5) sorted by relevance
/seL4-l4v-10.1.1/graph-refine/ |
H A D | logic.py | 15 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 D | loop_bounds.py | 265 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 D | syntax.py | 1351 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 D | pseudo_compile.py | 17 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
|
H A D | stack_logic.py | 22 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq namespace
|
Completed in 50 milliseconds