search

rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
61 stars 10 forks source link

isla-litmus-dump WIP #72

Closed tperami closed 4 months ago

tperami commented 1 year ago

There is currently no register dump: TODO

Currently, all is the executable file, the Coq pretty printing needs to move in a separate isla library.

Test with isla-lang/isla-litmus-dump for the coq output

Alasdair commented 1 year ago

It might be better if the main Coq printing parts were in a subfolder in isla-axiomatic, like isla-axiomatic/src/coq, or isla-axiomatic/src/litmus-dump.

I also added a register state function in isla-lib/src/trace.