summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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.
2016-07-28Banish exit from the mips/cheri sail except at end of SignalException ↵Robert Norton
function. There is a plan to replace this syntax with something more understandable. Should make no functional difference using sequential interpretor but will need to do some work on exception functions when integrating with ppcmem so that it know register writes are exceptional etc.
2016-07-28Complete another if statement with an empty else.Robert Norton
2016-07-28Use recently introduced 'not' function instead of ~ for boolean negation. ↵Robert Norton
More readable when extracted to manual.
2016-07-27Fix misspelt marker comment.Robert Norton
2016-07-27Add final 'else' to CCheckPerms because Peter pointed out that it is better ↵Robert Norton
this way.
2016-07-27CCall comment out of extracted psuedocode region.Robert Norton
2016-07-27Normalise whitespace in cheri_insts.sail for cleaner extraction of ↵Robert Norton
instructions into manual. Whitespace only.
2016-07-27Add a function 'not' to the library with type bit -> bitKathy Gray
2016-07-26Fix incomplete match warning in run_with*Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:49:46 +0000