Timeline
Apr 18, 2012:
- 2:52 PM Changeset [1891] by
- Nightmarish proofs on bitvectors. Trying to find some way of making …
- 2:01 PM Changeset [1890] by
- - added comment about bitvector translation
Apr 17, 2012:
- 6:05 PM Changeset [1889] by
- - some pages of article
Apr 13, 2012:
- 6:36 PM Changeset [1888] by
- Show that labelling of expressions works ... after fixing it to match …
Apr 12, 2012:
- 1:53 PM Changeset [1887] by
- - added SEFM2012 directory - some progress in assembly
Apr 11, 2012:
- 2:36 PM Changeset [1886] by
- - improvements for disambiguation and quick(er) typing
- 10:06 AM Changeset [1885] by
- - updated assembler with new definition of occurs_exactly_once
Apr 9, 2012:
- 3:07 PM Changeset [1884] by
- Syntax changes to fit Paolo's commit.
- 11:53 AM Changeset [1883] by
- Ilias' switch removal code, plus a test.
Apr 6, 2012:
- 8:02 PM Changeset [1882] by
- big update, alas incomplete: joint changed a bit, and all BE languages …
- 6:39 PM Changeset [1881] by
- Resurrect version of exec_up_to which shows the final state.
- 4:57 PM Changeset [1880] by
- Show that RTLabs flat traces are determined by their starting state, …
Apr 5, 2012:
- 6:13 PM Changeset [1879] by
- - Policy compiles until the end, still some (fairly trivial) cases …
Apr 4, 2012:
- 6:48 PM Changeset [1878] by
- Enforce typing of constants in front-end, plus binops for RTLabs.
- 6:48 PM Changeset [1877] by
- Update RTLabs structured traces for typed binops and new memory model.
- 6:48 PM Changeset [1876] by
- Update Cexec soundness proof. Change finishes_with predicate to …
- 6:48 PM Changeset [1875] by
- Update brief memory model test.
- 6:48 PM Changeset [1874] by
- First cut at using back-end memory model throughout. Note the …
- 6:48 PM Changeset [1873] by
- Fix up earlier front-end value conversion work.
- 6:48 PM Changeset [1872] by
- Make binary operations in Cminor/RTLabs properly typed. A few extra …
- 1:40 PM Changeset [1871] by
- Change Clight to Cminor compilation to use gotos rather than loops, …
Apr 3, 2012:
- 2:52 PM Changeset [1870] by
- - changed sigma00 in Assembly to use foldl_strong + proved invariants …
Mar 28, 2012:
- 11:44 AM Changeset [1869] by
- a load of axioms closed in ASMCosts file
Note: See TracTimeline
for information about the timeline view.
