| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-09 | Fix error in building register values | Kathy Gray | |
| (make one function to do it instead of almost the same function multiple times) Fix lost nexp variable in constraints, removing another undefined | |||
| 2015-06-08 | keeping tainted values in functionally updating records | Kathy Gray | |
| 2015-06-07 | Fix instruction extractor | Kathy Gray | |
| 2015-06-06 | append vectors with proper length for dec case | Kathy Gray | |
| 2015-06-05 | Manually turn negative nat values to 0 instead of letting Lem use an abs ↵ | Kathy Gray | |
| call to turn them positive, in to_vec* | |||
| 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 | changes to compare and equality instances to make lem generate isabelle output | cp526 | |
| 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-26 | small bug fixes | Kathy Gray | |
| 2015-05-19 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Shaked Flur | |
| 2015-05-19 | avoid the use of Str.regexp as it breaks js_of_ocaml | Shaked Flur | |
| 2015-05-19 | Add signed and unsigned functions, converting bit vectors to appropriate ↵ | Kathy Gray | |
| numbers (explicit instead of implicit in operations) | |||
| 2015-05-18 | Match cases better in bit vector printing (i.e. allow undef, and taint) | 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-18 | Add comparison for address | Kathy Gray | |
| 2015-05-17 | extend a missing case | Kathy Gray | |
| 2015-05-16 | 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-15 | actually match depend effect in has_effect function | 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-05 | allow undefined in mask for size | Kathy Gray | |
| 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-14 | Fix bug showing up in power.sail's compilation to Lem causing unknown values ↵ | Kathy Gray | |
| where they shouldn't be | |||
| 2015-04-07 | Move interpreter to zarith | Kathy Gray | |
| 2015-03-26 | Add subtraction to nexp grammar (removing the need to do a + (-1 * b)) | Kathy Gray | |
| Fix up parsing on 2** precedence Fix errors on type variables in function definition | |||
| 2015-03-19 | added constructors for aarch64 read_kind and write_kind | Shaked Flur | |
| 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. | |||
| 2015-01-28 | take sign into account on whether a number fits into the number of available ↵ | Kathy Gray | |
| bits or not | |||
| 2015-01-20 | Fix sparse vector fupdate slicing, assigning values in the right order and ↵ | Kathy Gray | |
| with the correct bit number | |||
| 2015-01-17 | update division | Kathy Gray | |
| 2015-01-16 | more for loop corrections, as well as pattern match error | Kathy Gray | |
| 2015-01-15 | signed subtraction | Kathy Gray | |
| 2015-01-15 | Fix for loop error causing premature stopping | Kathy Gray | |
| 2015-01-15 | Add support for overflow detecting subtraction | Kathy Gray | |
| 2015-01-14 | correct where overflow checking should happen on multiplication arithmetic | Kathy Gray | |
| 2015-01-14 | correct wrongly used variable in arith operations | Kathy Gray | |
| 2015-01-14 | more carry out | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |