summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-10-06move type definitions that both interpreter and shallow embedding use to ↵Christopher Pulte
sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
2016-09-30add Robert's DIA typeclass instancesChristopher Pulte
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-28Possible fix for equality and inequalityKathy Gray
2016-09-28Fix type checking bug that was missing unifications for natsKathy Gray
2016-09-26minor changesChristopher Pulte
2016-09-26nicer lem output: fewer unnecessary letbinds, monad binds and returnsChristopher Pulte
2016-09-25Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵Christopher Pulte
for-loops or case-expressions also return updated variables
2016-09-25Catch formal type system up to reality, in progressKathy Gray
2016-09-24nicer lem output: fewer unecessary 'return'sChristopher Pulte
2016-09-23Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-09-23sail-to-lem progressChristopher Pulte
2016-09-23Add register footprint function needed by ppcmem (mips only for now)Robert Norton
2016-09-21fixesChristopher Pulte
2016-09-19Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-19Fix type check bugKathy Gray
2016-09-19remove conflict messageChristopher Pulte
2016-09-16fixChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of ↵Christopher Pulte
unknown length (in the last item)
2016-09-14Switch mips/cheri over to using memory ea/val for writes. Tag is now first ↵Robert Norton
byte of value for capability writes. Still need TAGw for now but should kill eventually.
2016-09-14Use cap_size to check for address alignment in csc/clc instead of hardcoded ↵Robert Norton
32-byte alignment test.
2016-09-14Add memory kind for concurrent tag reads and writesKathy Gray
2016-09-14Change reading and writing of tag memory to report the tag/look for the tag ↵Kathy Gray
as the first byte of the byte list on tagged memory operations
2016-09-14Fix mistyped identifier in emacs modeKathy Gray
2016-09-13Support memea and memv in sequential interpreterKathy Gray
2016-09-13Add optional address to memv eventsKathy Gray
2016-09-13add show functions, fixChristopher Pulte
2016-09-13extern slice for instruction analysisKathy Gray
2016-09-12add list append functionKathy Gray
2016-09-09Fix bug in type checking cons that put the list first instead of the new elementKathy Gray
2016-09-09minor fixesKathy Gray
2016-09-09update instruction_analysis to support nias and instruction kindChristopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2016-09-02Extend type checking so that patterns with vector concatenation don't permit ↵Kathy Gray
under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis
2016-08-24pull files from idlarmShaked Flur
2016-08-18move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵Christopher
to interp_interface, fix reg_name comparison and equality
2016-08-17tuple assignment now implemented so (a,b) := foo() will now workKathy Gray
2016-08-17Fix pattern match bug in interp where vector accesses were using the wrong ↵Kathy Gray
start index
2016-08-14Add missing case to replicateKathy Gray
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
Not working yet
2016-08-10Missing case in libKathy Gray
2016-08-10Fix sizeof code generation to look at parameter boundsKathy Gray
2016-08-09More fixes to resolving nat variables across casesKathy Gray
2016-08-08Fix bug in type checker that ignored some pattern's constraints; fix second ↵Kathy Gray
bug that didn't cope properly with flow sensitive analysis across more than two case branches.
2016-08-06Add duplicate_bits to libKathy Gray
Pull Peter's changes to interp_interface back into the primary repo
2016-08-05Fix list parsing and empty vector parsingKathy Gray
Add div to library functions
2016-08-01Remove raise_c2_exception_v function which is not needed after permissions ↵Robert Norton
merge and no longer appears in spec.
2016-08-01Complete transition to merged perms. We need to take care to keep around the ↵Robert Norton
unused reserved permissions for when copying data, and stragely for candperms too.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 03:44:06 +0000