| Age | Commit message (Collapse) | Author |
|
|
|
|
|
behaviour that appeared to ignore ocaml depfiles.
|
|
|
|
Warning: this changes a few of the constructor names in the instruction_extractor.lem interface
|
|
|
|
|
|
|
|
|
|
Bytevectors; add place holder for memory size dependency tracking
|
|
|
|
|
|
|
|
|
|
|
|
this is quite specific to Power's spec)
|
|
|
|
|
|
|
|
gdb on actual binary for hello6
|
|
function-clause
|
|
|
|
properly yet but run_power.native is connected to it
|
|
|
|
effectively use elf model yet
|
|
|
|
instruction
|
|
|
|
|
|
|
|
|
|
|
|
Fix a few other bugs as well
|
|
(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)
|
|
|
|
|
|
|
|
adding executable as a test as well
|
|
|
|
LEM_DIR must contain the *absolute* path the Lem directory.
If not defined, the previous behaviour is retained: a relative path is
used, assuming Lem is in bitbucket/lem.
|
|
|
|
|
|
printing the events.
Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem
|
|
testing register tracking/tainting
|
|
instead of internal actions
|
|
|
|
There are problems that warrant discussion about handling special registers that hold records or data structures previously.
|
|
|
|
then hits an error. So still in progress
Note: moved barrier kind changes to interp_interface, along with other memory kinds
|
|
|