276def x86NativeEncodeJumpToLabel :
277 (pi unrestricted conditionFlag : Nat .
278 (pi unrestricted condition : (family X86NativeCondition) .
279 (pi unrestricted targetName : Bytes .
280 (pi unrestricted labels : (family X86NativeLabelTable) .
281 (pi unrestricted sourceEnd : (family X86NativeUnsigned32) .
282 (pi unrestricted tailResult : (family X86NativeAssemblyResult) .
283 (family X86NativeAssemblyResult))))))) =
284 (lambda unrestricted conditionFlag : Nat .
285 (lambda unrestricted condition : (family X86NativeCondition) .
286 (lambda unrestricted targetName : Bytes .
287 (lambda unrestricted labels : (family X86NativeLabelTable) .
288 (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) .
289 (lambda unrestricted tailResult : (family X86NativeAssemblyResult) .
290 (eliminate
291 X86NativeLabelLookupResult
292 (lambda unrestricted lookup : (family X86NativeLabelLookupResult) .
293 (family X86NativeAssemblyResult))
294 (x86NativeLookupLabel targetName labels)
295 (branch
296 X86NativeLabelFound
297 targetOffset
298 .
299 (eliminate
300 X86NativeRelativeDisplacementResult
301 (lambda unrestricted displacementResult : (family X86NativeRelativeDisplacementResult) .
302 (family X86NativeAssemblyResult))
303 (x86NativeRelativeDisplacement targetOffset sourceEnd)
304 (branch
305 X86NativeRelativeDisplacementSuccess
306 displacement
307 .
308 (nat-eliminate
309 (lambda unrestricted conditional : Nat . (family X86NativeAssemblyResult))
310 (x86NativePrependAssemblyBytes
311 (x86EncodeNativeInstruction
312 (constructor
313 X86NativeInstruction
314 X86NativeJumpRelative32
315 (x86NativeUnsigned32Displacement displacement)))
316 tailResult)
317 (lambda unrestricted predecessor : Nat .
318 (lambda unrestricted induction : (family X86NativeAssemblyResult) .
319 (x86NativePrependAssemblyBytes
320 (x86EncodeNativeInstruction
321 (constructor
322 X86NativeInstruction
323 X86NativeJumpConditionRelative32
324 condition
325 (x86NativeUnsigned32Displacement displacement)))
326 tailResult)))
327 conditionFlag))
328 (branch
329 X86NativeRelativeDisplacementOutOfRange
330 .
331 (constructor
332 X86NativeAssemblyResult
333 X86NativeAssemblyDisplacementOutOfRange
334 targetName))))
335 (branch
336 X86NativeLabelMissing
337 .
338 (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel targetName)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.