# # ChangeLog for src/Clight/SimplifyCasts.ma # # Generated by Trac 1.2 # Feb 25, 2021, 9:04:08 PM Thu, 19 Jul 2012 16:45:52 GMT campbell [2219] * src/Clight/SimplifyCasts.ma (modified) Speed up cast simplification proof checking a bit. Fri, 13 Jul 2012 17:59:41 GMT campbell [2184] * src/Clight/SimplifyCasts.ma (modified) * src/RTLabs/Traces.ma (modified) Minor fix ups. Thu, 12 Jul 2012 11:28:28 GMT campbell [2176] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/ClassifyOp.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/clightPrintMatita.ml (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/test/duff.c.ma (modified) * src/Clight/test/insertsort.c.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Clight/test/null-op.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/RTL/semantics.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/ByteValues.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Pointers.ma (modified) * src/common/Values.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) Remove memory spaces other than XData and Code; simplify pointers as ... 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 ... Thu, 14 Jun 2012 08:23:08 GMT garnier [2074] * src/Clight/SimplifyCasts.ma (modified) Prophylactic renaming of a relation Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ASM/WellLabeled.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/casts.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) !! BEWARE: major commit !! 1) [affects everybody] split for ... Fri, 08 Jun 2012 11:44:31 GMT garnier [2030] * src/Clight/SimplifyCasts.ma (modified) Cast simplification was too conservative, now reasonably aggressive. Wed, 06 Jun 2012 16:24:43 GMT campbell [2019] * src/Clight/Cexec.ma (modified) * src/Clight/CexecInd.ma (added) * src/Clight/CexecSound.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/compiler.ma (modified) Split out special induction principle for Clight from soundness file. ... Thu, 31 May 2012 14:41:33 GMT garnier [2011] * src/Clight/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) Minor cleanup. Wed, 30 May 2012 19:34:19 GMT garnier [2009] * src/Clight/SimplifyCasts.ma (modified) Proof of simulation completed for singe-step executions. Mon, 21 May 2012 15:03:20 GMT garnier [1974] * src/Clight/SimplifyCasts.ma (modified) Progress on the cast simplification proof. Fri, 18 May 2012 19:18:07 GMT garnier [1970] * src/Clight/SimplifyCasts.ma (modified) Work-in-progress: correction proof for the cast removal on expressions. Wed, 04 Apr 2012 16:48:24 GMT campbell [1873] * src/Clight/SimplifyCasts.ma (modified) * src/common/AST.ma (modified) * src/common/FrontEndVal.ma (modified) Fix up earlier front-end value conversion work. Wed, 04 Apr 2012 16:48:23 GMT campbell [1872] * src/Clight/ClassifyOp.ma (added) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.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/FrontEndOps.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/common/Values.ma (modified) Make binary operations in Cminor/RTLabs properly typed. A few extra ... 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, ... Thu, 08 Sep 2011 14:04:07 GMT campbell [1198] * src/CHANGES (modified) * src/Clight/SimplifyCasts.ma (added) * src/Clight/TypeComparison.ma (modified) * src/Clight/test/castremoval.c (added) * src/Clight/test/castremoval.c.ma (added) * src/Clight/test/sum.c.ma (modified) Clight cast removal (NB: quite different from the prototype).