# # ChangeLog for src/common/Identifiers.ma # # Generated by Trac 1.2 # Feb 28, 2021, 11:45:47 PM 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. Thu, 28 Jul 2011 10:14:37 GMT campbell [1092] * src/common/Identifiers.ma (modified) * src/utilities/lists.ma (modified) Some minor definitions for identifiers and lists. Tue, 19 Jul 2011 10:23:32 GMT mulligan [1077] * src/ERTL/ERTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) ack, dependent types are scary Fri, 15 Jul 2011 14:56:04 GMT campbell [1072] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Identifiers.ma (modified) Use not equals form of showing entry/exit labels. Fri, 15 Jul 2011 10:56:48 GMT campbell [1070] * src/ASM/BitVectorTrie.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Identifiers.ma (modified) Show that entry and exit labels are in the RTLabs graph. Thu, 14 Jul 2011 12:27:41 GMT mulligan [1068] * src/RTL/RTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/Identifiers.ma (modified) rtlabs translation complete subject to axioms Wed, 06 Jul 2011 11:29:58 GMT campbell [1058] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Maps.ma (deleted) Evict CompCert Maps interface in favour of BitVectorTries. Tue, 05 Jul 2011 15:53:11 GMT mulligan [1057] * src/ASM/Util.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/AST.ma (modified) * src/common/Identifiers.ma (modified) * src/common/IntValue.ma (added) changes from today Tue, 05 Jul 2011 14:25:41 GMT campbell [1056] * src/Clight/label.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Identifiers.ma (modified) Switch to delayed identifier error scheme. Tue, 05 Jul 2011 10:15:12 GMT mulligan [1055] * src/common/Identifiers.ma (modified) changes to how identifiers are generated Mon, 04 Jul 2011 16:20:23 GMT mulligan [1053] * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/Identifiers.ma (modified) changes 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 ... Thu, 28 Apr 2011 15:36:33 GMT mulligan [782] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/RegisterSet.ma (modified) More work on rtl-ertl pass from today, plus resolved conflict. Thu, 28 Apr 2011 08:55:47 GMT campbell [779] * src/ASM/BitVectorTrie.ma (modified) * src/common/Identifiers.ma (modified) Add merging of tries and identifier sets (based on Dominic's earlier ... 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:30:53 GMT mulligan [757] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Lots more fixing to get both front and backends using same ... Thu, 14 Apr 2011 15:54:37 GMT mulligan [753] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LTL/Branch.ma (deleted) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) Work from today. Mon, 04 Apr 2011 15:13:10 GMT campbell [738] * src/Clight/AST.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/RTLabs/import.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Use lower case names for identifiers for consistency with CompCert ... Mon, 04 Apr 2011 15:13:09 GMT campbell [737] * src/Clight/AST.ma (modified) * src/RTLabs/RTLabsMatitaPrinter.ml (modified) * src/RTLabs/test/search.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) Use more abstract identifiers in Clight / RTLabs. Mon, 04 Apr 2011 15:13:08 GMT campbell [736] * src/RTLabs/RTLabs-sem.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (added) * src/common/Registers.ma (modified) Extra type safety for identifiers.