A scheme of image specification.
An attribute is some statement about a program that is true, thus each attribute is a proposition in a logical database of inferred facts.
Note, in comments we use actual field names in the synopsis section of a function, e.g., section addr size
means that the section
statement has two fields Scheme.addr
and Scheme.size
.
See the OGRE library for more information.
type 'a region = {
addr : addr ;
size : size ;
info : 'a ;
}
a contiguous piece of memory.
val size : size Ogre .field
val addr : addr Ogre .field
val name : string Ogre .field
val root : addr Ogre .field
val readable : bool Ogre .field
val writable : bool Ogre .field
val executable : bool Ogre .field
val fixup : addr Ogre .field
is_executable
an address of a fixup
val arch : (string, (string -> 'a ) -> 'a ) Ogre .attribute
arch name
a file contains code for the name
architecture.
val segment :
((bool * bool * bool) region ,
(addr -> size -> bool -> bool -> bool -> 'a ) ->
'a )
Ogre .attribute
segment addr size readable writable executable
a memory region (addr,size) has the specified permissions.
val section : (unit region , (addr -> size -> 'a ) -> 'a ) Ogre .attribute
section addr size
a memory region is a section
val code_start : (addr , (addr -> 'a ) -> 'a ) Ogre .attribute
code_start addr
an address starts a code sequence
val entry_point : (addr , (addr -> 'a ) -> 'a ) Ogre .attribute
entry_point addr
an address is a program entry point
symbol_chunk addr size root
a contiguous piece of a program symbol, that can be a function or some data.
val named_region :
(string region , (addr -> size -> string -> 'a ) -> 'a ) Ogre .attribute
named_region addr size name
a region of memory has a name
val named_symbol : (addr * string, (addr -> string -> 'a ) -> 'a ) Ogre .attribute
named_symbol addr name
a symbol that starts at this addr
has this name
.
mapped addr size off
sequence of bytes in a file starting at offset off
and has the given size
is mapped into memory at the given address addr
val relocation : (int64 * addr , (addr -> addr -> 'a ) -> 'a ) Ogre .attribute
relocation fixup addr
a value referenced at the code that has the fixup
address is relocated to the specified address addr
.
val external_reference :
(addr * string, (addr -> string -> 'a ) -> 'a ) Ogre .attribute
extrenal_reference addr name
a piece of code at the specified address addr
references an external symbol with the given name
.
val base_address : (addr , (addr -> 'a ) -> 'a ) Ogre .attribute
base_address addr
this is the base address of an image, i.e., an address of a first byte of the image.