summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Collapse)Author
2015-09-06Improved type system, so that it catches int where there should be natKathy 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-30Change 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-30Fix updating dec vector start bugsKathy Gray
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
Events are eamem to signal the memory address to write to and wmv to pass the value to write
2015-06-10Put missing cases into nexp_eq_checkKathy Gray
2015-06-04reduce 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-01Fix pattern match bug with enumerated valuesKathy Gray
2015-05-01Change 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-26Add 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-15Many 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-25Fix rewriting tag bugKathy Gray
2015-02-18Fix dependency generation when type variable appears in a vector length positionKathy Gray
2015-02-13Fix error of not keeping register reads when they're accessed via a fieldKathy Gray
2015-02-13Actually 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