| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-06-05 | small variable renaming for Isabelle | cp526 | |
| 2015-06-05 | slight change of binary_taint for Isabelle | cp526 | |
| 2015-06-04 | reduce number of unknown identifiers and get one step closer to actually ↵ | Kathy Gray | |
| decoding an ARM instruction. (Note: may fix issue #2, haven't checked yet) | |||
| 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-16 | Fix vector field type annotation error | 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-05 | continue moving closer to better Gt Lt constraint checks | 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-17 | remove old elf sources | 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-14 | Get power.sail compiling to Lem again | Kathy Gray | |
| 2015-04-08 | Fixes to make arm spec build again | Kathy Gray | |
| 2015-04-08 | Fixes for power compilation reworking | Kathy Gray | |
| 2015-04-08 | makefile changes to keep up with lem ocaml-lib changes | Kathy Gray | |
| 2015-04-07 | Move interpreter to zarith | Kathy Gray | |
| 2015-03-31 | Fix int -> nat bug. Now something with type int cannot be used as something ↵ | Kathy Gray | |
| of type nat (at least not without a >= 0 check) | |||
| 2015-03-26 | Turn off all the debugging printfs | 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 | Begin adding new information to constraints to get tightness of bounds properly | Kathy Gray | |
| 2015-03-19 | added constructors for aarch64 read_kind and write_kind | Shaked Flur | |
| 2015-03-18 | Handle type/kind variables in val spec vs function declaration as equal, ↵ | Kathy Gray | |
| although the function ones are optional | |||
| 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 | oops, last one broke power's build. this fixes it | Kathy Gray | |
| 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-03-04 | Fix off-by-one constraint error on vector to number coercions | Kathy Gray | |
| 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-02-25 | Fix rewriting tag bug | Kathy Gray | |
| 2015-02-25 | and catch a printf | Kathy Gray | |
| 2015-02-25 | Stop losing constraints due to incorrectly calculating their size | Kathy Gray | |
| 2015-02-24 | Fix lem printing | Kathy Gray | |
| 2015-02-24 | Turn off the printfs left in from previous debugging | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |