Timeline
Feb 15, 2012:
- 6:02 PM Changeset [1697] by
- important bug found
- 4:09 PM Changeset [1696] by
- finished adding russell types to the traverse_cost_* functions
- 2:10 PM Changeset [1695] by
- Progress on CostsProof?.ma file.
- 9:30 AM Changeset [1694] by
- indexed labels branch
Feb 14, 2012:
- 4:38 PM Changeset [1693] by
- Changes to ASMCosts and CostsProofs? files to get everything working again.
- 1:18 PM Changeset [1692] by
- resolved conflict in asm costs this morning
- 1:43 AM Changeset [1691] by
- Some progress in the proof: less daemons, less hypotheses in lemmas.
Feb 13, 2012:
- 3:58 PM Changeset [1690] by
- nested loops are not supported yet, the only test had one
- 3:54 PM Changeset [1689] by
- kept out the wrapper (which I did not touch, so not sure it works)
- 9:08 AM Changeset [1688] by
- up d5.1-5.3
Feb 10, 2012:
- 2:12 PM Changeset [1687] by
- corrected title
Feb 9, 2012:
- 6:16 PM Changeset [1686] by
- corrected abstract
- 6:08 PM Changeset [1685] by
- adjusted comparison with aiT
- 5:42 PM Changeset [1684] by
- changes from the past week
- 5:41 PM Changeset [1683] by
- abstract and running example
- 1:22 PM Changeset [1682] by
- Complete proof for as_after_return for RTLabs.
- 1:22 PM Changeset [1681] by
- Checkpoint of stack preservation work in RTLabs.
- 1:22 PM Changeset [1680] by
- Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
Feb 7, 2012:
- 6:01 PM Changeset [1679] by
- Frama-C plug-in (sources+documentation)
- 4:36 PM Changeset [1678] by
- finished editing the english in the report
- 12:23 PM Changeset [1677] by
- changes to paolo's english in the report, about a 1/4 of the way through
Feb 6, 2012:
- 6:50 PM Changeset [1676] by
- corrected some faults still TODO: running example, language corrections
- 3:33 PM Changeset [1675] by
- Some work on sound labelled for RTLabs.
- 12:32 PM Changeset [1674] by
- corrected some faults still TODO: running example, language corrections
Feb 4, 2012:
- 11:58 AM Changeset [1673] by
- report on indexed labels TODO: corrections, examples, etc
Feb 1, 2012:
- 4:16 PM Changeset [1672] by
- Matita now generates a couple of inversion lemmas that were manually …
- 4:16 PM Changeset [1671] by
- A little more on RTLabs infinite traces.
- 4:16 PM Changeset [1670] by
- Snapshot of non-terminating RTLabs structured traces work.
- 3:36 PM Changeset [1669] by
- Commit for claudio
Jan 30, 2012:
- 11:41 AM Changeset [1668] by
- - split build_maps into build_maps and build_maps_ok - work with CSC …
Jan 29, 2012:
- 10:25 PM Changeset [1667] by
- Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
Jan 28, 2012:
- 1:42 PM Changeset [1666] by
- PreStatus? datatype change: the code_memory field is not a left …
Jan 27, 2012:
- 5:05 PM Changeset [1665] by
- progress on closing holes in block_cost' proof
- 12:11 AM Changeset [1664] by
- corrected a bug in loop peeling where continue and breaks were not …
Jan 26, 2012:
- 5:40 PM Changeset [1663] by
- old cases working again, work on new ones
- 10:06 AM Changeset [1662] by
- rev
- 10:04 AM Changeset [1661] by
- rev
- 8:58 AM Changeset [1660] by
- Deliverable: Frama-C plug-in (D5.1-5.3)
- 8:43 AM Changeset [1659] by
Jan 25, 2012:
- 6:18 PM Changeset [1658] by
- asm costs changes from today
- 5:40 PM Changeset [1657] by
- preliminary version of D5
Jan 23, 2012:
- 7:01 PM Changeset [1656] by
- Minor fixups to RTLabs/Traces due to syntax changes.
- 6:31 PM Changeset [1655] by
- Update Cminor and RTLabs semantics to use new monad definitions.
- 5:37 PM Changeset [1654] by
- Corrections to structured trace definitions (see the mailing list). …
- 5:37 PM Changeset [1653] by
- Start on building finite sections of non-terminating structured traces.
- 5:37 PM Changeset [1652] by
- Forgot to apply 1583 to non-terminating case.
- 5:37 PM Changeset [1651] by
- Start looking at non-terminating structured traces by defining …
Jan 19, 2012:
- 4:56 PM Changeset [1650] by
- changes over the last couple of days: stuck due to matita producing …
Jan 18, 2012:
- 6:17 PM Changeset [1649] by
- - changes to Assembly for integration with Policy and easier use of …
- 11:01 AM Changeset [1648] by
- new version of utilities/monad.ma with typecheck command comented out
Jan 17, 2012:
- 1:13 PM Changeset [1647] by
- * corrected some notation problems * adapted Cligth with slight …
Jan 16, 2012:
- 3:04 PM Changeset [1646] by
- finished the block_costs computation, and propagated the changes …
Note: See TracTimeline
for information about the timeline view.
