| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-08 | augment annot of interpreter | Kathy Gray | |
| 2015-08-06 | Update analysis to merge states and values after branches taken due to ↵ | Kathy Gray | |
| unknown conditions. Does not merge if one path has resulted in an exit | |||
| 2015-07-24 | Begin doing better analysis on case splits over unknowns | Kathy Gray | |
| 2015-07-01 | fix equality comparison | Kathy Gray | |
| 2015-07-01 | Use set instead of list for tainted values | Kathy Gray | |
| 2015-07-01 | Go on despite the presence of an exit in exhaustive mode | Kathy Gray | |
| 2015-06-28 | Tag enumeration variables properly when introducing them | Kathy Gray | |
| 2015-06-26 | Better handling of literal true and false (turn them into the expected bit0 ↵ | Kathy Gray | |
| and bit1); also fix some handling of wmv and eamem. | |||
| 2015-06-24 | Support new write memory events | Kathy Gray | |
| 2015-06-24 | Add new outcomes/events separating effective address and value for memory writes | Kathy Gray | |
| 2015-06-22 | Fixes issue #12 | Kathy Gray | |
| 2015-06-18 | Consistent handling of constructors with no parameters | Kathy Gray | |
| 2015-06-17 | Extend mode and external memory functions with endian flag | Kathy Gray | |
| 2015-06-09 | Too hasty removal; still used by trans_sail.gen | Kathy Gray | |
| 2015-06-09 | remove superfluous num_to_bits; replaced by bit_list_of_integer | Kathy Gray | |
| 2015-06-09 | support exit/escape out of the interface | Kathy Gray | |
| 2015-06-07 | Fix instruction extractor | Kathy Gray | |
| 2015-06-02 | Fix errors around ARM not being able to decode due to instruction_extractor ↵ | Kathy Gray | |
| being very power-specific. Note: slight interface change to instruction_extractor | |||
| 2015-05-13 | Add dynamic footprint dependency check event/outcome | Kathy Gray | |
| Also fix type checker bug in not reporting modifications to parameter values | |||
| 2015-05-01 | Change interpreter interface to support ppcmem2's view of vectors as always ↵ | Kathy Gray | |
| increasing while supporting inc and dec views to the interpreter and in printing Fix bugs exposed by running idlarm several instructions (after fixing above) | |||
| 2015-04-22 | Fix some interpreter bugs preventing ARM instructions from making progress | Kathy Gray | |
| 2015-03-18 | Use boolean on write where applicable | Kathy Gray | |
| 2015-03-17 | Correct directionality in interpreter. Now the interpreter shouldn't use inc ↵ | Kathy Gray | |
| unless that's the current default or there's no default set in the spec | |||
| 2015-03-15 | Many changes: | Kathy Gray | |
| Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction | |||
| 2015-02-27 | Fix a series of errors leading to the first ARM instruction not running. | Kathy Gray | |
| Including: Correct loss of constraints between declared constraints, pattern constraints and expression body constraints Handle insertion of dependent parameters in the case of unit parameters Add a case to how ifields are translated to permit numbers as well as bits and bitvectors Expand interpreter to actually handle user-defined functions on the left had side of the assignment expression. | |||
| 2014-12-11 | Many fixes, primarily dealing with undefined | Kathy Gray | |
| Including: turn an undefined literal into a vector of undefined values of the correct length handle sparse vector unspecified default values as undefined literals allow global lets to call library functions | |||
| 2014-12-10 | Fix mismatch errors in interpreter, mostly relating to taint/detaint behaviour | Kathy Gray | |
| Also fixed for loop evaluation | |||
| 2014-11-23 | make interpreter work better with unknowns, make interp_inter_imp do better ↵ | Kathy Gray | |
| on coercions | |||
| 2014-11-23 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Peter Sewell | |
| 2014-11-23 | the properly named "git" | Peter Sewell | |
| 2014-11-23 | extern single bit and single bool to instruction_fields | Kathy Gray | |
| 2014-11-23 | Fill in some of the basic coercions | Kathy Gray | |
| 2014-11-23 | clean up interp inter | Kathy Gray | |
| 2014-11-23 | more coercions | Peter Sewell | |
| 2014-11-23 | OCaml stubs for coercions and _to_istate OCaml | Peter Sewell | |
| 2014-11-23 | wib (comment out to typecheck the rest...) | Peter Sewell | |
| 2014-11-23 | fight with interface/impl mismatch. lose. | Peter Sewell | |
| 2014-11-23 | update instruction/istate decoding. | Kathy Gray | |
| Use register size. Printing again doesn't compile | |||
| 2014-11-22 | interp_interface happy again. printing functions now doesn't compile | Kathy Gray | |
| 2014-11-22 | Add size of register to register for making appropriate unknown register_values | Kathy Gray | |
| 2014-11-22 | Changing interface in step with Peter and ppcmem changes | Kathy Gray | |
| 2014-11-21 | Support signed and unsigned arithmetic | Kathy Gray | |
| 2014-11-21 | Fix bugs now documented in ppcmem notes | Kathy Gray | |
| 2014-11-20 | look for sub matches of registers on exhaustive mode | Kathy Gray | |
| 2014-11-19 | add byte_list_of_integer | Kathy Gray | |
| 2014-11-19 | Correct off-by-one bug in type checking vector slices | Kathy Gray | |
| Convert sparse vectors into full-fledged vectors more frequently and on export to memory system | |||
| 2014-11-18 | Actually expect barriers to happen | Kathy Gray | |
| 2014-11-18 | Fix countLeadingZeroes typo (diff in number of es present) | Kathy Gray | |
| 2014-11-16 | Add some missing functions | Kathy Gray | |
| 2014-11-16 | Add overflow checking arithmetic operations. Fix various bugs that this exposed | Kathy Gray | |
| Of note: Interp_lib.to_num now takes an Unsigned or a Signed constructor, rather than a boolean | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |