| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-08 | wreg effects and tags now proper for LEXP_field, LEXP_vector ↵ | Kathy Gray | |
| LEXP_vector_range for sub register writes. Closes issue #23 | |||
| 2015-12-07 | Interpreter working again with updated tag, effects, and types behaviour | Kathy Gray | |
| 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 | Turn back off new analysis style until it works | Kathy Gray | |
| 2015-07-24 | Begin doing better analysis on case splits over unknowns | Kathy Gray | |
| 2015-07-20 | minor fixes | Kathy Gray | |
| 2015-07-02 | fix match_pattern reverse bug | Kathy Gray | |
| 2015-07-01 | fix equality comparison | Kathy Gray | |
| 2015-07-01 | Use set instead of list for tainted values | Kathy Gray | |
| 2015-06-30 | Fix updating dec vector start bugs | 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-21 | Taint printing changes: make it for debugging only, except when showing all ↵ | Kathy Gray | |
| events in exhaustive mode | |||
| 2015-06-18 | Consistent handling of constructors with no parameters | Kathy Gray | |
| 2015-06-17 | fix missed pattern case | Kathy Gray | |
| 2015-06-08 | keeping tainted values in functionally updating records | Kathy Gray | |
| 2015-06-06 | append vectors with proper length for dec case | Kathy Gray | |
| 2015-06-05 | Fix issue #5 | Kathy Gray | |
| 2015-06-05 | small variable renaming for Isabelle | cp526 | |
| 2015-06-05 | slight change of binary_taint for Isabelle | cp526 | |
| 2015-06-03 | make string functions used to UI and debugging output empty strings for ↵ | cp526 | |
| theorem provers, use structural (in)equality for Isabelle and HOL for literals and values | |||
| 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-28 | fix pattern matching bug on concatenated vectors | Kathy Gray | |
| 2015-05-18 | expand unsigned comparisons | Kathy Gray | |
| 2015-05-18 | Add equality check for addresses | Kathy Gray | |
| And fix match failure problem (hopefully) | |||
| 2015-05-17 | extend a missing case | Kathy Gray | |
| 2015-05-16 | Fix bug where undef was blown up to fill the full register on a field assignment | Kathy Gray | |
| 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 | Fix pattern match bug with enumerated values | Kathy Gray | |
| 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-04-07 | Move interpreter to zarith | 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. | |||
| 2015-01-20 | Fix sparse vector fupdate slicing, assigning values in the right order and ↵ | Kathy Gray | |
| with the correct bit number | |||
| 2015-01-16 | more for loop corrections, as well as pattern match error | Kathy Gray | |
| 2015-01-15 | Fix for loop error causing premature stopping | Kathy Gray | |
| 2014-12-18 | Bring interpreter upto date with current Lem | Kathy Gray | |
| 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-12-09 | Abstract tainting to almost always use taint, detaint, retaint, and ↵ | Kathy Gray | |
| binary_taint functions instead of V_track directly. Annoyingly, Lem won't let one section of code use these functions, complaining of too much polymorphism. Also, might fix arithmetic | |||
| 2014-11-24 | improve value to string for debugging | Kathy Gray | |
| 2014-11-24 | wib | Kathy Gray | |
| 2014-11-24 | Missing patterns in pattern matches | Kathy Gray | |
| 2014-11-24 | coerce single element bit vector to bit for conditionals | Kathy Gray | |
| 2014-11-23 | slice Only when I should and not to erase an register write | Kathy Gray | |
| 2014-11-23 | Slice generated vectors when appropriate | Kathy Gray | |
| 2014-11-23 | Treat undef like unknown when needing a vector assignment of them | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |