# # ChangeLog for src/Clight/toCminor.ma # # Generated by Trac 1.2 # Apr 19, 2021, 8:25:24 PM Mon, 19 Dec 2011 13:48:37 GMT campbell [1631] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/lists.ma (modified) Use fact that type environments in Cminor have distinct variables to ... Mon, 19 Dec 2011 13:48:36 GMT campbell [1630] * src/Clight/toCminor.ma (modified) * src/utilities/lists.ma (modified) Remainder of freshness in Clight to Cminor pass. Mon, 19 Dec 2011 13:48:35 GMT campbell [1629] * src/Clight/fresh.ma (modified) * src/Clight/toCminor.ma (modified) Sort out most of the fresh names stuff in Clight to Cminor. Mon, 19 Dec 2011 13:48:34 GMT campbell [1627] * src/Clight/toCminor.ma (modified) * src/common/Identifiers.ma (modified) Add some notions of freshness, and start using them for temporary ... Mon, 19 Dec 2011 13:48:33 GMT campbell [1626] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Errors.ma (modified) * src/utilities/lists.ma (added) Add extra type safety in front end. NB: critical freshness parts ... Wed, 14 Dec 2011 14:58:39 GMT sacerdot [1612] * src/Clight/toCminor.ma (modified) * src/RTLabs/import.ma (modified) All library ported to new Matita lib (finally). Wed, 14 Dec 2011 13:30:39 GMT sacerdot [1608] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/common/Errors.ma (modified) Porting to new library still in progress. Wed, 14 Dec 2011 12:18:30 GMT sacerdot [1605] * src/Clight/CexecEquiv.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) Porting to last standard library of Matita. Fri, 18 Nov 2011 23:38:20 GMT sacerdot [1516] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/BitVectorZ.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/common/AST.ma (modified) * src/common/Events.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/GenMem.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Integers.ma (modified) * src/common/Mem.ma (modified) * src/common/Pointers.ma (modified) * src/common/PositiveMap.ma (modified) * src/joint/BEValues.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) * src/utilities/lists.ma (modified) Ported to syntax of Matita 0.99.1. Fri, 18 Nov 2011 12:03:14 GMT campbell [1515] * src/ASM/ASM.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/fresh.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/insertsort.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (added) * src/common/PreIdentifiers.ma (modified) * src/joint/Erasure.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) Add type of maps on positive binary numbers, and use them for ... Fri, 14 Oct 2011 08:56:45 GMT campbell [1369] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/Values.ma (modified) Put type information into front-end unary ops. Slight change to ... Tue, 11 Oct 2011 10:24:33 GMT campbell [1351] * src/Clight/toCminor.ma (modified) * src/Cminor/semantics.ma (modified) * src/common/Errors.ma (modified) * src/utilities/deppair.ma (modified) * src/utilities/lists.ma (modified) Tidy up some loose ends from the invariants branch merge. Fri, 07 Oct 2011 10:26:39 GMT campbell [1316] * src (modified) * src/ASM (modified) * src/ASM/BitVectorTrie.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Errors.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/deppair.ma (copied) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/option.ma (modified) * src/utilities/pair.ma (copied) Merge in id-lookup-branch to trunk. Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224] * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IntValue.ma (deleted) Type of programs in common/AST made more dependent. In particular, ... Mon, 12 Sep 2011 14:20:57 GMT campbell [1207] * src/ASM/Arithmetic.ma (modified) * src/Clight/fresh.ma (added) * src/Clight/toCminor.ma (modified) Second part of fixing temporaries in Clight to Cminor stage. Mon, 12 Sep 2011 14:20:57 GMT campbell [1206] * src/Clight/toCminor.ma (modified) First stage of fixing temporary generation in Clight/toCminor.ma. Tue, 06 Sep 2011 15:20:19 GMT campbell [1194] * src/Clight/toCminor.ma (modified) Remove old, commented out code. Tue, 30 Aug 2011 10:47:18 GMT campbell [1139] * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/test/insertsort.c.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) Shift init_data out of generic program record so that it only appears ... Tue, 19 Jul 2011 10:39:01 GMT campbell [1078] * src/Clight/toCminor.ma (modified) Implement stack allocation for parameters whose address is taken. Wed, 15 Jun 2011 14:15:54 GMT campbell [962] * src/Clight/toCminor.ma (modified) * src/common/FrontEndOps.ma (modified) Casts should use source type's signedness, not the target's. Wed, 15 Jun 2011 14:15:52 GMT campbell [961] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Clight/test/search.ma (modified) * src/Clight/test/sum.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) * src/utilities/extranat.ma (modified) Use precise bitvector sizes throughout the front end, rather than ... Mon, 06 Jun 2011 11:27:59 GMT campbell [886] * src/Clight/toCminor.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) Put types into parameter and variable lists in Cminor. Temporarily ... Fri, 03 Jun 2011 15:35:32 GMT campbell [882] * src/Clight/CexecSound.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/toCminor.ma (modified) * src/RTLabs/import.ma (modified) * src/common/AST.ma (modified) * src/utilities/extralib.ma (modified) Fix up fragile proofs for current version of matita. Fri, 03 Jun 2011 15:35:31 GMT campbell [881] * src/Clight/test/io.ma (modified) * src/Clight/test/sum.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AST.ma (modified) Sort out regions in Cminor to fix Clight to Cminor translation of Ederef. Fri, 03 Jun 2011 15:35:31 GMT campbell [880] * src/Clight/Cexec.ma (modified) * src/Clight/TypeComparison.ma (added) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AST.ma (modified) Add type information into Cminor. As a result, the Clight to Cminor ... 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 ...