l4ka/pistachio — Issue #2: L4_BootInfo_t on AMD64
Author: mandrookin
Created: 2011-12-06 12:21:16+00:00
State: open

unsigned int	i;
L4_MemoryDesc_t	*	mbi_desc = 0;

do {

printf( "L4_NumMemoryDescriptors = %ld\n", L4_NumMemoryDescriptors(kip));
for(i=0; i < L4_NumMemoryDescriptors(kip); i++)
{
L4_MemoryDesc_t * mdesc = L4_MemoryDesc( kip, i );
if( L4_MemoryDescType (mdesc) == (L4_BootLoaderSpecificMemoryType | 0x10) )
{
printf("Found BootLoaderSpecificMemoryType at %p\n", (void*) L4_MemoryDescLow(mdesc));
mbi_desc = mdesc;
break;
}
}

This code works perfect on x86-32bit, but does not work on AMD64.