Lines Matching defs:r15
56 val r15 = mk_var("r15",``:word32``)
72 val mems = filter (fn x => not (tmem x [``r15 + 3w:word32``,
73 ``r15 + 2w:word32``,``r15 + 1w:word32``,r15])) mems
86 ``(r15:word32,(n2w (c:num)):word32)``
87 fun is_pc_relative tm = tmem (mk_var("r15",``:word32``)) (free_vars tm)
120 ``ALIGNED r15``,
121 ``ARM_READ_MEM (r15 + 3w) s = n2w n``,
122 ``ARM_READ_MEM (r15 + 2w) s = n2w n``,
123 ``ARM_READ_MEM (r15 + 1w) s = n2w n``,
124 ``ARM_READ_MEM (r15 + 0w) s = n2w n``,
125 ``ARM_READ_MEM r15 s = n2w n``] tm
126 in subst s r15 !~ r15 end handle HOL_ERR _ => true
129 val pre_conds = filter (fn x => not (is_neg x andalso is_eq (cdr x) andalso tmem r15 (free_vars x))) pre_conds
137 val pc = mk_var("r15",``:word32``)
647 val thms = arm_spec (enc "LDMIA sp!, {r0-r2, r15}");
656 val thms = arm_spec (enc "STMDB sp!, {r0-r2, r15}");