"ycchang" <ycchang@cirx.org> writes:

>  this inline funtion returns PTE_BASE + i386_btop(va) , where
>  PTE_BASE = 0xbfc00000 and i386_btop(va) is defined as
>  ((unsigned)(x) >> PGSHIFT). That is to say it gets the VA of PTE
>  corresponding to a VA.

...

> So , should vtopte() return PTE_BASE + i386_btop(va)*4? 

It does. The definition of PTE_BASE is the value 0xbfbc0000 cast to a
pointer, a pt_entry_t *. The pointer type causes the addition to
follow the usual C rules for pointer arithmetic, which means that the
value returned from i386_btop() is interpreted as a number of
pt_entry_t's. Since a pt_entry_t is 4 bytes (see pte.h), the scaling
is implicit in the pointer math.

        - Nathan