| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-28 | added rewriter rewrite_defs_remove_vector_concat that should get rid of ↵ | Christopher Pulte | |
| vector-concat patterns. Not tested. | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | building version of last change, removing stray ) | Kathy Gray | |
| 2015-09-25 | Rewrite expressions for ocaml, lifting assignment introductions into a ↵ | Kathy Gray | |
| special let form to set the scope | |||
| 2015-09-24 | Beginning of expression rewriter for ocaml | Kathy Gray | |
| 2015-09-24 | basic pattern rewriter | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-09-24 | added 'remove_vector_string_patterns and .._expressions functions | Christopher Pulte | |
| 2015-09-17 | Type checker checking on case splits properly, and dependency ↵ | Kathy Gray | |
| transformations restored :) | |||
| 2015-09-06 | Improved type system, so that it catches int where there should be nat | Kathy Gray | |
| Note: the resulting Lem file generated may or may not actually work properly with the interpreter (i.e. it might have too many unknowns); still in the process of debugging some changes there. | |||
| 2015-06-30 | Change rewriter to better reset dec vectors to count from (length - 1) ↵ | Kathy Gray | |
| instead of whatever random spot they might be in, where functions expect length-n to 0 | |||
| 2015-06-30 | Fix updating dec vector start bugs | Kathy Gray | |
| 2015-06-24 | Support new memory write events in the sail front end and pretty printer | Kathy Gray | |
| Events are eamem to signal the memory address to write to and wmv to pass the value to write | |||
| 2015-06-10 | Put missing cases into nexp_eq_check | Kathy Gray | |
| 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-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-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-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-25 | Fix rewriting tag bug | Kathy Gray | |
| 2015-02-18 | Fix dependency generation when type variable appears in a vector length position | Kathy Gray | |
| 2015-02-13 | Fix error of not keeping register reads when they're accessed via a field | Kathy Gray | |
| 2015-02-13 | Actually use new dependency information in generation of lem/etc. | Kathy Gray | |
| Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |