Lines Matching defs:ebp
149 val ebp = mk_var("ebp",``:word32``)
150 fun access_ebp tm = (tm = ebp) orelse
151 (can (match_term ``(v:word32) - n2w n``) tm andalso (ebp = (cdr o car) tm))
158 val th = DISCH ``ALIGNED ebp`` th
308 val th = x86_spec "89EE"; (* mov esi,ebp *)
311 val th = x86_spec "89EA"; (* mov edx,ebp *)
313 val th = x86_spec "89CD"; (* mov ebp,ecx *)
314 val th = x86_spec "45"; (* inc ebp *)
317 val th = x86_spec "8B2A"; (* mov ebp,[edx] *)
319 val th = x86_spec "8929"; (* mov [ecx],ebp *)
321 val th = x86_spec "892A"; (* mov [edx],ebp *)
341 val th = x86_spec (x86_encode "add [ebp-20],eax")