# # ChangeLog for src/Cminor/test # # Generated by Trac 1.2 # Apr 17, 2021, 9:57:57 AM Wed, 04 Jan 2012 18:19:09 GMT campbell [1633] * src/Clight/clightPrintMatita.ml (modified) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/factorial.Cminor.ma (added) * src/Cminor/test/factorial.ma (deleted) * src/Cminor/test/factorial.test.ma (added) * src/Cminor/test/null-op.Cminor.ma (modified) * src/Cminor/test/null-op.test.ma (added) * src/Cminor/test/search.Cminor.ma (modified) * src/Cminor/test/search.test.ma (modified) * src/Cminor/test/sum-bad.ma (deleted) * src/Cminor/test/switcher.ma (deleted) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/import.ma (modified) * src/acc-matita-printers.patch (modified) Update Cminor pretty printer and examples. Fri, 16 Sep 2011 17:16:44 GMT campbell [1226] * src/Clight/clightPrintMatita.ml (modified) * src/Clight/test/sum.c.ma (modified) * src/Clight/test/sum.test.ma (added) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/search.Cminor.ma (modified) * src/Cminor/test/search.test.ma (added) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/test/search.RTLabs.ma (modified) * src/RTLabs/test/search.test.ma (added) Adjust pretty printers for change in program records, try a test of each. Wed, 31 Aug 2011 10:15:39 GMT campbell [1157] * src/Clight/clightPrintMatita.ml (modified) * src/Clight/test/duff.c.ma (modified) * src/Clight/test/factorial.c.ma (modified) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/search.Cminor.ma (modified) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/test/search.RTLabs.ma (modified) Update pretty printers and examples. Wed, 15 Jun 2011 14:15:57 GMT campbell [966] * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/null-op.Cminor.ma (modified) * src/Cminor/test/search.Cminor.ma (modified) Update Cminor pretty printer and some examples. Wed, 08 Jun 2011 11:14:55 GMT campbell [898] * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/null-op.Cminor.ma (added) * src/Cminor/test/null-op.ma (deleted) * src/Cminor/test/search.Cminor.ma (added) * src/Cminor/test/search.ma (deleted) * src/Cminor/test/sum.ma (deleted) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/test/search.RTLabs.ma (added) * src/RTLabs/test/sum.RTLabs.ma (added) Update pretty printers and examples. Fri, 03 Jun 2011 15:35:30 GMT campbell [879] * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/test/factorial.ma (modified) * src/Cminor/test/null-op.ma (modified) * src/Cminor/test/search.ma (modified) * src/Cminor/test/sum-bad.ma (modified) * src/Cminor/test/sum.ma (modified) * src/Cminor/test/switcher.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/test/search.ma (modified) * src/RTLabs/test/sum.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/Events.ma (modified) * src/common/IO.ma (modified) Refine "AST" types to include size/signedness information. Thu, 19 May 2011 13:06:42 GMT campbell [816] * src/CHANGES (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/test/search.ma (modified) * src/Clight/toCminor.ma (added) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/test/factorial.ma (modified) * src/Cminor/test/search.ma (modified) * src/Cminor/test/switcher.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) * src/RTLabs/test/search.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/lists.ma (modified) Clight to Cminor compilation, modulo switch statements, temporary ... Fri, 13 May 2011 11:10:23 GMT campbell [797] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/test/insertsort.ma (modified) * src/Clight/test/io.ma (modified) * src/Clight/test/io2.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/test/sum-bad.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/debug.ma (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/Animation.ma (modified) * src/common/Errors.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PreIdentifiers.ma (added) * src/common/SmallstepExec.ma (modified) * src/common/Values.ma (modified) Add error messages wherever the error monad is used. Sticks to ... Wed, 27 Apr 2011 09:47:40 GMT campbell [776] * src/Clight/Csem.ma (modified) * src/Clight/test/null-op.c (added) * src/Clight/test/null-op.ma (added) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/test/null-op.ma (added) Fix up some minor null pointer issues in Clight. Add corresponding ... Fri, 22 Apr 2011 13:21:28 GMT campbell [771] * src/Cminor/test/switcher.ma (modified) * src/Cminor/toRTLabs.ma (modified) Implement switch statements in Cminor -> RTLabs phase Fri, 22 Apr 2011 11:49:13 GMT campbell [770] * src/Clight/test/switcher.c (added) * src/Clight/test/switcher.ma (added) * src/Cminor/test/switcher.ma (added) Clight and Cminor examples for switch statement. Fri, 22 Apr 2011 11:49:12 GMT campbell [768] * src/Cminor/test/factorial.ma (modified) * src/Cminor/test/search.ma (modified) * src/Cminor/test/sum.ma (modified) Make Cminor tests test translation to RTLabs. Tue, 19 Apr 2011 10:22:32 GMT campbell [761] * src/ASM/BitVectorTrie.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/test/sum-bad.ma (added) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/option.ma (added) Enforce the use of declared identifiers/registers in Cminor/RTLabs. Mon, 18 Apr 2011 10:33:35 GMT campbell [758] * src/Clight/test/sum.c (added) * src/Clight/test/sum.ma (added) * src/Cminor/cminorMatitaPrinter.ml (modified) * src/Cminor/initialisation.ma (added) * src/Cminor/test/sum.c (added) * src/Cminor/test/sum.ma (added) * src/common/Globalenvs.ma (modified) Implement replacement of global var initialisation data by code in ... Wed, 13 Apr 2011 16:52:10 GMT campbell [751] * src/Cminor (added) * src/Cminor/cminorMatitaPrinter.ml (added) * src/Cminor/semantics.ma (added) * src/Cminor/syntax.ma (added) * src/Cminor/test (added) * src/Cminor/test/factorial.ma (added) * src/Cminor/test/search.ma (added) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/SmallstepExec.ma (modified) * src/common/Values.ma (modified) Initial version of the Cminor syntax and semantics.