summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp_ast.lem
AgeCommit message (Collapse)Author
2017-07-24move value type definitions to ott, and introduce new E_internal_value ast ↵Jon French
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
# 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
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵Robert Norton
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.
2017-02-03fix headersPeter Sewell
2013-10-10Rename Ast to Interp_ast for the interpreterGabriel Kerneis