I am trying to model memory using Z3, however I stil have a very basic question . Given .elf file for arm with segments and sections as shown below
Segments
r-x 0x00000000-0x0000a88c
rw- 0x0001a88c-0x0001b2dc
Sections:
0x00008000-0x0000800c .init (PROGBITS) {Code}
0x0000800c-0x0000a780 .text (PROGBITS) {Code}
0x0000a780-0x0000a78c .fini (PROGBITS) {Code}
0x0000a78c-0x0000a794 .rodata (PROGBITS) {Read-only data}
0x0000a794-0x0000a7b8 .ARM.extab (PROGBITS) {Read-only data}
0x0000a7b8-0x0000a888 .ARM.exidx {Read-only data}
0x0000a888-0x0000a88c .eh_frame (PROGBITS) {Read-only data}
0x0001a88c-0x0001a894 .init_array {Writable data}
0x0001a894-0x0001a898 .fini_array {Writable data}
0x0001a898-0x0001a89c .jcr (PROGBITS) {Writable data}
0x0001a8a0-0x0001b0e0 .data (PROGBITS) {Writable data}
0x0001b0e0-0x0001b2dc .bss (NOBITS) {Writable data}
If I have instrution like Load R3, [R0] with R0 = 0 Where can I found the zero memory location to load its initial value in the elf file i.e M[0] ? How can I model the memory values before execution ? For example, I would like to have address range like from 0xaaaa to 0xcccc in elf files are M[0] to M[final] initial values.
User contributions licensed under CC BY-SA 3.0