# # ChangeLog for src/Clight/label.ma # # Generated by Trac 1.2 # Jan 23, 2021, 1:02:06 PM Wed, 17 Oct 2012 16:45:20 GMT campbell [2399] * src/Clight/label.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Fill in some details about the statement of correctness. Wed, 10 Oct 2012 15:18:15 GMT campbell [2392] * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) Labelling translations of && and || need a lot of cost labelling to ... Tue, 09 Oct 2012 13:10:07 GMT campbell [2391] * 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/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/test/controlflow.c.ma (modified) * src/Clight/toCminor.ma (modified) Revert "Put the post-loop cost label into the Clight while statement ... Wed, 26 Sep 2012 16:14:38 GMT campbell [2353] * 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/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/toCminor.ma (modified) Put the post-loop cost label into the Clight while statement to get ... Mon, 03 Sep 2012 11:16:29 GMT campbell [2319] * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/labelSpecification.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/compiler.ma (modified) Generate per-program cost labels rather than per-function ones, and ... Thu, 21 Jun 2012 15:21:02 GMT campbell [2103] * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/AST.ma (modified) * src/joint/Erasure.ma (modified) Make transform_*program take a more general transformation to make ... Fri, 13 Apr 2012 16:36:16 GMT campbell [1888] * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (added) Show that labelling of expressions works ... after fixing it to ... 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, 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, ... 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. 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 ... Thu, 28 Apr 2011 14:43:50 GMT campbell [781] * src/Clight/label.ma (added) * src/Clight/test/insertsort.ma (modified) * src/common/Events.ma (modified) Implement labelling pass for Clight.