| Age | Commit message (Collapse) | Author |
|---|
|
|
|
exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints
|
|
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
|
|
to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem.
|
|
|
|
|
|
trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.
|
|
|
|
|
|
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
|
|
|
|
|
|
it is only ever used for translating the PC.
|
|
|
|
|
|
|
|
|
|
fix sail_values bug.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
has non-zero E (latest spec.)
|
|
|
|
match ASL; add missing functions/cases to library
|
|
|
|
|
|
interpreter
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
instruction state, factor out interpreter/shallow embedding value conversion
|
|
change to printing
|
|
|
|
|
|
|
|
|
|
|
|
tests all memory is equal
|
