| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-03 | Fix bug exposed/introduced by properly handling vector starts in the type ↵ | Kathy Gray | |
| checker | |||
| 2016-04-12 | Reduce warnings for interpreter. Removed all pattern match warnings for ↵ | Kathy Gray | |
| interp_lib, interp_inter_imp, and printing_functions. | |||
| 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-19 | abbreviate printing of memory values <=9 | Peter Sewell | |
| 2015-06-24 | Support new write memory events | Kathy Gray | |
| 2015-06-22 | Fixes issue #12 | 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 | Put reverse in the correct place | Kathy Gray | |
| 2015-06-18 | add endian flag to memory printing | 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-18 | Match cases better in bit vector printing (i.e. allow undef, and taint) | 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-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-01-15 | Add support for overflow detecting subtraction | Kathy Gray | |
| 2014-11-30 | clean up ghastly pre-submission pp hackery | Peter Sewell | |
| 2014-11-24 | Give a better answer on overflow with two vectors of unknowns (i.e. unknown ↵ | Kathy Gray | |
| instead of 0) | |||
| 2014-11-23 | fix logfile printing | Peter Sewell | |
| 2014-11-23 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Peter Sewell | |
| Conflicts: src/lem_interp/printing_functions.ml | |||
| 2014-11-23 | wib | Peter Sewell | |
| 2014-11-23 | instruction printing | Kathy Gray | |
| 2014-11-23 | better... still not right | Peter Sewell | |
| 2014-11-23 | new printing code | Peter Sewell | |
| 2014-11-23 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Peter Sewell | |
| 2014-11-23 | wib | Peter Sewell | |
| 2014-11-23 | make interpreter now builds | Kathy Gray | |
| and I *think* that I'm making vectors of unknowns in all the necessary places now. | |||
| 2014-11-23 | wib | Peter Sewell | |
| 2014-11-23 | Fill in some of the basic coercions | Kathy Gray | |
| 2014-11-22 | Printing functions compiles again | Kathy Gray | |
| 2014-11-22 | Add size of register to register for making appropriate unknown register_values | Kathy Gray | |
| 2014-11-22 | make interpreter now compiles | Kathy Gray | |
| Printing functions are not complete and may cause exceptions still on unknown or undef bits. run_interp_model doesn't work and thus make power doesn't work. | |||
| 2014-11-22 | Changing interface in step with Peter and ppcmem changes | Kathy Gray | |
| 2014-11-21 | Print out default values for underspecified vectors instead of leaving them ↵ | Kathy Gray | |
| and letting them turn into undefineds | |||
| 2014-11-19 | print sparse vectors | Kathy Gray | |
| 2014-11-18 | wib | Kathy Gray | |
| 2014-11-18 | Add missing cases to printing_functions printing of interp_values | Kathy Gray | |
| 2014-11-17 | Use red printing for the value in the hole from Printing_functions instead ↵ | Kathy Gray | |
| of mangling the ascii manually | |||
| 2014-11-17 | wib | Peter Sewell | |
| 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 | |||
| 2014-11-12 | ; -> , | Peter Sewell | |
| 2014-11-12 | Add a function to print local variables and values, local_variables_to_string | Kathy Gray | |
| will format them as one long ; separated line | |||
| 2014-11-11 | remove [ and ] from values in the hole | Kathy Gray | |
| 2014-11-08 | make pp of Bitvector values of widths 1,2,4, or 8 bytes be in hex (but ↵ | Peter Sewell | |
| including start bit-index) | |||
| 2014-11-06 | Refactor printing to display the contents the [_] and to better format bit ↵ | Kathy Gray | |
| vectors | |||
| 2014-11-04 | K,P better instruction pp | Peter Sewell | |
| 2014-11-03 | pp of initial index of bitvector | Peter Sewell | |
| 2014-10-30 | more compact pp of binary values (following verilog literal syntax) | Peter Sewell | |
| (though we still get some long lists of bitzero,bitzero,... in the instruction state printing...) | |||
| 2014-10-29 | tweak value pp (remove byte count) | Peter Sewell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |