#
# ChangeLog for src/RTLabs/debug.ma
#
# Generated by Trac 1.2
# Dec 10, 2019, 7:48:12 PM

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 ...


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 ...


Wed, 27 Apr 2011 09:47:38 GMT campbell [775]
	* src/RTLabs/debug.ma (added)

	A few useful definitions for when RTLabs programs fail.