# # ChangeLog for src/Cminor # # Generated by Trac 1.2 # Dec 9, 2019, 6:51:54 PM Wed, 03 Apr 2013 15:54:34 GMT campbell [3081] * src/Clight/SimplifyCastsMeasurable.ma (modified) * src/Clight/SwitchAndLabel.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/common/FEMeasurable.ma (modified) * src/common/SmallstepExec.ma (modified) * src/utilities/extranat.ma (modified) * src/utilities/lists.ma (modified) Tidy up recent work a little. Tue, 02 Apr 2013 10:16:41 GMT campbell [3063] * src/Clight/SimplifyCastsMeasurable.ma (modified) * src/Clight/toCminorMeasurable.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/common/FEMeasurable.ma (modified) Remove measure function from FEMeasurable because we're not using it ... Thu, 28 Mar 2013 13:59:43 GMT campbell [3007] * src/Cminor/Cminor_abstract.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/common/FEMeasurable.ma (modified) Sketch out how Cminor to RTLabs correctness would fit into the ... Wed, 27 Mar 2013 23:07:56 GMT campbell [2992] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabs_syntax.ma (modified) Add "only one return" invariant to RTLabs functions. Wed, 27 Mar 2013 10:41:51 GMT campbell [2971] * src/Cminor/toRTLabs.ma (modified) Single RTLabs return statement. Thu, 21 Mar 2013 20:45:49 GMT campbell [2936] * src/Cminor/Cminor_semantics.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/RTLabs_syntax.ma (modified) * src/compiler.ma (modified) Disable initialisation code generation in Cminor, propogate init data ... Thu, 21 Mar 2013 07:39:00 GMT campbell [2924] * src/Cminor/toRTLabs.ma (modified) Make calls to a known identifier actually use a direct call. Thu, 07 Mar 2013 17:33:42 GMT sacerdot [2809] * src/Cminor/Cminor_classified_system.ma (added) ... Wed, 06 Mar 2013 18:23:42 GMT campbell [2793] * src/Cminor/initialisation.ma (modified) Oops, gave fields wrong order during initialisation. Tue, 26 Feb 2013 18:37:41 GMT garnier [2737] * src/Clight/Clight_abstract.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Cminor/Cminor_abstract.ma (modified) Commit of current proof state for Clight to Cminor translation. Sat, 23 Feb 2013 16:05:03 GMT campbell [2722] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Measurable.ma (modified) * src/correctness.ma (modified) It's easier to keep the real function identifier in front-end ... Tue, 19 Feb 2013 11:23:50 GMT campbell [2677] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Clight_abstract.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Cminor/Cminor_abstract.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/RTLabs/RTLabs_abstract.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/RTLabs_traces.ma (modified) * src/correctness.ma (modified) Retain the pointer for the function called in front-end call states ... Thu, 07 Feb 2013 20:22:22 GMT sacerdot [2645] * src/ASM/ASM.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Char.ma (deleted) * src/ASM/I8051.ma (modified) * src/BACKEND_BROKEN_FILES (added) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/test/addptrcharboth.test.ma (modified) * src/Clight/test/badconditional.test.ma (modified) * src/Clight/test/controlflow.test.ma (modified) * src/Clight/test/endptr.test.ma (modified) * src/Clight/test/endptr2.test.ma (modified) * src/Clight/test/forcont.test.ma (modified) * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/implicit.test.ma (modified) * src/Clight/test/implicitcond.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/test/trivial.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/Cminor/Cminor_syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTLptr/ERTLptr.ma (modified) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/RTL/RTL_semantics.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/import.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/BackEndOps.ma (modified) * src/common/ByteValues.ma (modified) * src/common/CostLabel.ma (modified) * src/common/ErrorMessages.ma (added) * src/common/Errors.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Graphs.ma (modified) * src/common/IO.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PreIdentifiers.ma (modified) * src/common/Registers.ma (modified) * src/common/Values.ma (modified) * src/compiler.ma (modified) * src/joint/Joint.ma (modified) * src/joint/String.ma (moved) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) 1. some broken back-end files repaires, several still to go 2. the ... Wed, 06 Feb 2013 17:39:21 GMT campbell [2624] * src/Cminor/initialisation.ma (modified) * src/common/AST.ma (modified) * src/common/Floats.ma (deleted) * src/common/Globalenvs.ma (modified) Properly evict unused and axiomatised Floats. Wed, 06 Feb 2013 12:01:34 GMT garnier [2608] * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/MemProperties.ma (modified) * src/Clight/frontend_misc.ma (modified) * src/Clight/memoryInjections.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/toCminorCorrectnessExpr.ma (modified) * src/Clight/toCminorOps.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/RTLabs_traces.ma (modified) * src/common/ByteValues.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Pointers.ma (modified) * src/common/extraGlobalenvs.ma (modified) Regions are no more stored in blocks. block_region now tests the id, ... Tue, 05 Feb 2013 12:36:31 GMT sacerdot [2601] * extracted (added) * extracted/PROBLEMS (added) * extracted/aSM.ml (added) * extracted/aSM.mli (added) * extracted/aSMCosts.ml (added) * extracted/aSMCosts.mli (added) * extracted/aSMCostsSplit.ml (added) * extracted/aSMCostsSplit.mli (added) * extracted/aST.ml (added) * extracted/aST.mli (added) * extracted/abstractStatus.ml (added) * extracted/abstractStatus.mli (added) * extracted/arithmetic.ml (added) * extracted/arithmetic.mli (added) * extracted/bitVector.ml (added) * extracted/bitVector.mli (added) * extracted/bitVectorTrie.ml (added) * extracted/bitVectorTrie.mli (added) * extracted/bitVectorZ.ml (added) * extracted/bitVectorZ.mli (added) * extracted/bool.ml (added) * extracted/bool.mli (added) * extracted/byteValues.ml (added) * extracted/byteValues.mli (added) * extracted/casts.ml (added) * extracted/casts.mli (added) * extracted/cexec.ml (added) * extracted/cexec.mli (added) * extracted/cexecInd.ml (added) * extracted/cexecInd.mli (added) * extracted/cexecSound.ml (added) * extracted/cexecSound.mli (added) * extracted/char.ml (added) * extracted/char.mli (added) * extracted/classifyOp.ml (added) * extracted/classifyOp.mli (added) * extracted/cminor_syntax.ml (added) * extracted/cminor_syntax.mli (added) * extracted/compiler.ml (added) * extracted/compiler.mli (added) * extracted/coqlib.ml (added) * extracted/coqlib.mli (added) * extracted/core_notation.ml (added) * extracted/core_notation.mli (added) * extracted/costLabel.ml (added) * extracted/costLabel.mli (added) * extracted/csem.ml (added) * extracted/csem.mli (added) * extracted/csyntax.ml (added) * extracted/csyntax.mli (added) * extracted/deqsets.ml (added) * extracted/deqsets.mli (added) * extracted/div_and_mod.ml (added) * extracted/div_and_mod.mli (added) * extracted/division.ml (added) * extracted/division.mli (added) * extracted/errors.ml (added) * extracted/errors.mli (added) * extracted/events.ml (added) * extracted/events.mli (added) * extracted/extra_bool.ml (added) * extracted/extra_bool.mli (added) * extracted/extralib.ml (added) * extracted/extralib.mli (added) * extracted/extranat.ml (added) * extracted/extranat.mli (added) * extracted/fetch.ml (added) * extracted/fetch.mli (added) * extracted/floats.ml (added) * extracted/floats.mli (added) * extracted/foldStuff.ml (added) * extracted/foldStuff.mli (added) * extracted/fresh.ml (added) * extracted/fresh.mli (added) * extracted/frontEndMem.ml (added) * extracted/frontEndMem.mli (added) * extracted/frontEndOps.ml (added) * extracted/frontEndOps.mli (added) * extracted/frontEndVal.ml (added) * extracted/frontEndVal.mli (added) * extracted/frontend_misc.ml (added) * extracted/frontend_misc.mli (added) * extracted/genMem.ml (added) * extracted/genMem.mli (added) * extracted/globalenvs.ml (added) * extracted/globalenvs.mli (added) * extracted/graphs.ml (added) * extracted/graphs.mli (added) * extracted/hide.ml (added) * extracted/hide.mli (added) * extracted/hints_declaration.ml (added) * extracted/hints_declaration.mli (added) * extracted/iO.ml (added) * extracted/iO.mli (added) * extracted/iOMonad.ml (added) * extracted/iOMonad.mli (added) * extracted/identifiers.ml (added) * extracted/identifiers.mli (added) * extracted/initialisation.ml (added) * extracted/initialisation.mli (added) * extracted/integers.ml (added) * extracted/integers.mli (added) * extracted/interpret.ml (added) * extracted/interpret.mli (added) * extracted/jmeq.ml (added) * extracted/jmeq.mli (added) * extracted/label.ml (added) * extracted/label.mli (added) * extracted/labelledObjects.ml (added) * extracted/labelledObjects.mli (added) * extracted/list.ml (added) * extracted/list.mli (added) * extracted/listb.ml (added) * extracted/listb.mli (added) * extracted/lists.ml (added) * extracted/lists.mli (added) * extracted/logic.ml (added) * extracted/logic.mli (added) * extracted/memProperties.ml (added) * extracted/memProperties.mli (added) * extracted/memoryInjections.ml (added) * extracted/memoryInjections.mli (added) * extracted/monad.ml (added) * extracted/monad.mli (added) * extracted/nat.ml (added) * extracted/nat.mli (added) * extracted/option.ml (added) * extracted/option.mli (added) * extracted/order.ml (added) * extracted/order.mli (added) * extracted/pointers.ml (added) * extracted/pointers.mli (added) * extracted/positive.ml (added) * extracted/positive.mli (added) * extracted/positiveMap.ml (added) * extracted/positiveMap.mli (added) * extracted/preIdentifiers.ml (added) * extracted/preIdentifiers.mli (added) * extracted/preamble.ml (added) * extracted/proper.ml (added) * extracted/proper.mli (added) * extracted/pts.ml (added) * extracted/pts.mli (added) * extracted/rTLabs_syntax.ml (added) * extracted/rTLabs_syntax.mli (added) * extracted/registers.ml (added) * extracted/registers.mli (added) * extracted/relations.ml (added) * extracted/relations.mli (added) * extracted/russell.ml (added) * extracted/russell.mli (added) * extracted/setoids.ml (added) * extracted/setoids.mli (added) * extracted/sets.ml (added) * extracted/sets.mli (added) * extracted/simplifyCasts.ml (added) * extracted/simplifyCasts.mli (added) * extracted/smallstep.ml (added) * extracted/smallstep.mli (added) * extracted/smallstepExec.ml (added) * extracted/smallstepExec.mli (added) * extracted/star.ml (added) * extracted/star.mli (added) * extracted/status.ml (added) * extracted/status.mli (added) * extracted/statusProofs.ml (added) * extracted/statusProofs.mli (added) * extracted/string.ml (added) * extracted/string.mli (added) * extracted/structuredTraces.ml (added) * extracted/structuredTraces.mli (added) * extracted/switchRemoval.ml (added) * extracted/switchRemoval.mli (added) * extracted/toCminor.ml (added) * extracted/toCminor.mli (added) * extracted/toRTLabs.ml (added) * extracted/toRTLabs.mli (added) * extracted/typeComparison.ml (added) * extracted/typeComparison.mli (added) * extracted/types.ml (added) * extracted/types.mli (added) * extracted/util.ml (added) * extracted/util.mli (added) * extracted/utilBranch.ml (added) * extracted/utilBranch.mli (added) * extracted/values.ml (added) * extracted/values.mli (added) * extracted/vector.ml (added) * extracted/vector.mli (added) * extracted/z.ml (added) * extracted/z.mli (added) * src/ASM/BitVector.ma (modified) * src/Clight/Clight_abstract.ma (moved) * src/Clight/toCminor.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Clight/toCminorCorrectnessExpr.ma (modified) * src/Clight/toCminorOps.ma (modified) * src/Cminor/Cminor_abstract.ma (moved) * src/Cminor/Cminor_semantics.ma (moved) * src/Cminor/Cminor_syntax.ma (moved) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/ERTL/ERTL_semantics.ma (moved) * src/ERTLptr/ERTLptr_semantics.ma (moved) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/LIN_semantics.ma (moved) * src/LTL/LTL_semantics.ma (moved) * src/RTL/RTL_semantics.ma (moved) * src/RTLabs/CostCheck.ma (modified) * src/RTLabs/CostInj.ma (modified) * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/MeasurableTraces.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabs_abstract.ma (moved) * src/RTLabs/RTLabs_semantics.ma (moved) * src/RTLabs/RTLabs_syntax.ma (moved) * src/RTLabs/RTLabs_traces.ma (moved) * src/RTLabs/debug.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Globalenvs.ma (modified) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (moved) * src/joint/semanticsUtils.ma (modified) * src/joint/stacksize.ma (modified) * src/utilities/extra_bool.ma (moved) Extraction to ocaml is now working, with a couple of bugs left. One ... Thu, 31 Jan 2013 11:56:03 GMT garnier [2598] * src/Clight/abstract.ma (modified) * src/Clight/memoryInjections.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Cminor/abstract.ma (modified) Tentative, partial draft for the definition of Clight-Cminor ... Thu, 31 Jan 2013 11:07:02 GMT campbell [2597] * src/Clight/toCminorCorrectness.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/common/FEMeasurable.ma (added) Some work in progress on measurable subtrace preservation. Fri, 30 Nov 2012 17:31:29 GMT campbell [2511] * src/Cminor/toRTLabsCorrectness.ma (added) * src/RTLabs/MeasurableTraces.ma (modified) * src/RTLabs/abstract.ma (modified) * src/common/Measurable.ma (modified) Conjecture main Cminor/RTLabs simulation results. Add a few notes ... Tue, 27 Nov 2012 16:50:51 GMT garnier [2496] * src/Clight/abstract.ma (modified) * src/Clight/frontend_misc.ma (modified) * src/Clight/toCminor.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Cminor/abstract.ma (modified) * src/common/Errors.ma (modified) Some tentative work on the simulation proof for expressions, in order ... Fri, 23 Nov 2012 16:28:25 GMT campbell [2489] * src/Clight/toCminorCorrectness.ma (modified) * src/Cminor/abstract.ma (added) Conjecture some Clight/Cminor simulation results. Thu, 15 Nov 2012 17:12:57 GMT garnier [2468] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecInd.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/ClassifyOp.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/MemProperties.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/frontend_misc.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/memoryInjections.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/common/AST.ma (modified) * src/common/Events.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Values.ma (modified) Floats are gone from the front-end. Some trace amount might remain in ... Fri, 12 Oct 2012 13:33:53 GMT campbell [2395] * src/Clight/Csem.ma (modified) * src/Clight/test/endptr.test.ma (modified) * src/Clight/test/endptr2.c (added) * src/Clight/test/endptr2.c.ma (added) * src/Clight/test/endptr2.test.ma (copied) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/FrontEndMem.ma (modified) * src/common/FrontEndOps.ma (modified) Proper handling of comparison of pointers off-the-end of an object. ... Fri, 05 Oct 2012 10:57:20 GMT campbell [2390] * src/Cminor/toRTLabs.ma (modified) Tidy up a corner case when generating RTLabs so that we generate ... Mon, 01 Oct 2012 16:21:59 GMT campbell [2384] * Deliverables/D2.2/8051-matita-out/src/RTLabs/RTLabsMatitaPrinter.ml (moved) * Deliverables/D2.2/8051-matita-out/src/clight/clightPrintMatita.ml (moved) * Deliverables/D2.2/8051-matita-out/src/cminor/cminorMatitaPrinter.ml (moved) Move Matita pretty printers into place. Thu, 20 Sep 2012 16:57:34 GMT campbell [2335] * src/Cminor/toRTLabs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (modified) Deal with goto labels in RTLabs to Cminor by fixing up goto ... 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, 02 Aug 2012 16:40:15 GMT campbell [2292] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/utilities/lists.ma (modified) More RTLabs invariants. Thu, 02 Aug 2012 15:04:37 GMT campbell [2289] * src/Cminor/toRTLabs.ma (modified) Update alias Thu, 02 Aug 2012 15:04:35 GMT campbell [2287] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) RTLabs typing for loads and stores. Tue, 24 Jul 2012 17:40:23 GMT campbell [2254] * src/Cminor/semantics.ma (modified) Fix up invariants in Cminor semantics. Tue, 24 Jul 2012 17:40:22 GMT campbell [2253] * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/compiler.ma (modified) Cminor to RTLabs is now a total function. Tue, 24 Jul 2012 17:40:21 GMT campbell [2252] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) Use the return statement invariant. Restructure the invariants for ... Tue, 24 Jul 2012 17:40:21 GMT campbell [2251] * 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) Add new invariant to Cminor that return typs should be respected. Tue, 24 Jul 2012 17:40:13 GMT campbell [2249] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) Tweak Cminor invariant to be slightly more readable/extendable. Mon, 23 Jul 2012 12:05:10 GMT campbell [2232] * 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) Remove unused block structure in Cminor. Thu, 12 Jul 2012 12:56:50 GMT campbell [2178] * src/Cminor/toRTLabs.ma (modified) * src/utilities/extralib.ma (modified) Shift some notation into utilities. 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 ... Fri, 08 Jun 2012 14:57:14 GMT sacerdot [2033] * src/Cminor/toRTLabs.ma (modified) Daemon reverted. 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 ... Thu, 24 May 2012 15:10:05 GMT campbell [1993] * src/Clight/test/memorymodel.ma (modified) * src/Cminor/semantics.ma (modified) * src/common/Animation.ma (modified) * src/common/FrontEndMem.ma (added) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (deleted) * src/joint/BEMem.ma (modified) Make front-end memory model only depend on the general definitions by ... Thu, 24 May 2012 09:39:27 GMT campbell [1988] * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/joint/BEGlobalenvs.ma (modified) * src/joint/BEMem.ma (modified) Abstraction of the memory contents in the memory models is no longer ... Thu, 24 May 2012 07:35:08 GMT campbell [1986] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/Globalenvs.ma (modified) Get rid of unused abstraction of Globalenvs. Mon, 09 Apr 2012 13:07:06 GMT campbell [1884] * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) Syntax changes to fit Paolo's commit. Wed, 04 Apr 2012 16:48:27 GMT campbell [1878] * 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) Enforce typing of constants in front-end, plus binops for RTLabs. Wed, 04 Apr 2012 16:48:25 GMT campbell [1874] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/joint/BEValues.ma (modified) First cut at using back-end memory model throughout. Note the ... 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 ... Tue, 21 Feb 2012 10:58:12 GMT campbell [1713] * 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/Cminor/semantics.ma (modified) * src/RTLabs/Traces.ma (modified) * src/RTLabs/semantics.ma (modified) Add a distinguished final state to the front-end languages to match ... Thu, 09 Feb 2012 12:22:28 GMT campbell [1680] * 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) Comment out unused tailcalls in Cminor and RTLabs. (They would be a ... Mon, 23 Jan 2012 17:31:27 GMT campbell [1655] * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) Update Cminor and RTLabs semantics to use new monad definitions. 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. 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: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:35:41 GMT sacerdot [1611] * src/Cminor/toRTLabs.ma (modified) All of Cminor now compiles with the latest lib of Matita. Wed, 14 Dec 2011 14:33:57 GMT sacerdot [1610] * src/Cminor/initialisation.ma (modified) Ported to new lib. 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. Tue, 13 Dec 2011 16:37:40 GMT sacerdot [1603] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) More proofs ported to new lib. Tue, 13 Dec 2011 00:34:37 GMT sacerdot [1599] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/JMCoercions.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AssocList.ma (modified) * src/common/Errors.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Mem.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/BEGlobalenvs.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/adt/priority_set_adt.ma (modified) * src/utilities/adt/set_adt.ma (modified) * src/utilities/adt/table_adt.ma (modified) * src/utilities/binary/division.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/pair.ma (deleted) Start of merging of stuff into the standard library of Matita. Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/Z.ma (modified) Syntax change in Matita: change what where => change where what. 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 ... Tue, 25 Oct 2011 17:12:50 GMT campbell [1464] * src/Cminor/toRTLabs.ma (modified) Use unification hints to simplify the graph monotonicity proofs. Wed, 19 Oct 2011 09:54:13 GMT campbell [1410] * src/Clight/CexecSound.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/FrontEndOps.ma (modified) Remove a few old workarounds. Tue, 18 Oct 2011 10:39:11 GMT ricciott [1401] * src/Clight/TypeComparison.ma (modified) * src/Cminor/initialisation.ma (modified) * src/common/AST.ma (modified) Changes concerning the new behavior of destruct. 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:45:16 GMT sacerdot [1352] * src/Clight/CexecEquiv.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Cminor/semantics.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/semantics.ma (modified) This commit is made necessary by the last Matita change. Inclusion ... 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. Wed, 21 Sep 2011 14:25:36 GMT campbell [1238] * src/Clight/test/search.c.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) Update Cminor and RTLabs to fit SmallstepExec changes. 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. 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, ... 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. Tue, 30 Aug 2011 14:09:20 GMT campbell [1147] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/Cminor/syntax.ma (modified) * src/RTLabs/syntax.ma (modified) Remove some obsolete commented out code, update a couple of comments. 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 ... 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. 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: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, 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 ... 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. Mon, 06 Jun 2011 14:28:07 GMT campbell [888] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) Use simplified conditionals in RTLabs, following the prototype. Mon, 06 Jun 2011 13:55:23 GMT campbell [887] * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) Start bringing RTLabs into line with the prototype compiler: - a ... 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: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 ... 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. Fri, 03 Jun 2011 15:35:27 GMT campbell [878] * src/Cminor/syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/RTL/RTL.ma (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/syntax.ma (modified) Removal of manually inserted record projections. 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 ... Tue, 10 May 2011 15:50:09 GMT campbell [790] * src/Cminor/toRTLabs.ma (modified) * src/common/Mem.ma (modified) A little tidying: get rid of requirement for jmeq in Mem.ma, remove ... Thu, 28 Apr 2011 08:55:49 GMT campbell [780] * src/Cminor/toRTLabs.ma (modified) * src/utilities/lists.ma (modified) Properly update set of registers that are used for pointers in Cminor ... 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 15:09:34 GMT campbell [772] * src/Cminor/toRTLabs.ma (modified) Implement proper support for RTLabs addressing modes. 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. Fri, 22 Apr 2011 09:48:04 GMT campbell [767] * src/Cminor/toRTLabs.ma (modified) Use variable shadowing as a poor man's state monad in cminor to ... Thu, 21 Apr 2011 17:24:04 GMT campbell [766] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/utilities/lists.ma (added) Most of the Cminor to RTLabs stage. Is buggy, generates inefficient ...