# # ChangeLog for Deliverables # # Generated by Trac 1.2 # Dec 5, 2019, 8:41:34 PM Tue, 15 Feb 2011 14:37:52 GMT mulligan [520] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more changes Tue, 15 Feb 2011 14:23:53 GMT mulligan [519] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) Footnote fixed Tue, 15 Feb 2011 14:05:02 GMT mulligan [518] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) small changes Tue, 15 Feb 2011 13:53:35 GMT mulligan [517] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more added Tue, 15 Feb 2011 13:12:45 GMT mulligan [516] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) Added section on Tries Tue, 15 Feb 2011 10:49:19 GMT mulligan [515] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) finished tidying the introduction Tue, 15 Feb 2011 09:58:58 GMT mulligan [514] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more tidying Tue, 15 Feb 2011 09:44:32 GMT mulligan [513] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more changes to intro Tue, 15 Feb 2011 09:39:42 GMT mulligan [512] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) tidy up of the intro Mon, 14 Feb 2011 16:30:17 GMT mulligan [511] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) validation section complete Mon, 14 Feb 2011 15:17:42 GMT mulligan [510] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more added, talking about dependent types now Mon, 14 Feb 2011 14:27:57 GMT sacerdot [509] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) Background. Mon, 14 Feb 2011 14:24:55 GMT mulligan [508] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) Changes Mon, 14 Feb 2011 13:15:24 GMT mulligan [507] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) A bit on labels and pseudo-instructions Mon, 14 Feb 2011 10:55:13 GMT mulligan [506] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) a bit more added Mon, 14 Feb 2011 10:14:49 GMT mulligan [505] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) finished sentence Mon, 14 Feb 2011 10:14:12 GMT mulligan [504] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) work on intro committed following claudio's second e-mail Mon, 14 Feb 2011 10:04:53 GMT mulligan [503] * Deliverables/D4.1/ITP-Paper/iramlayout.png (added) * Deliverables/D4.1/ITP-Paper/memorylayout.png (added) Added PNG files for claudio. Fri, 11 Feb 2011 16:45:08 GMT campbell [502] * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/test/ptrbool.c (added) Fix not on nulls on Clight. Fri, 11 Feb 2011 16:35:18 GMT mulligan [501] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more changes Fri, 11 Feb 2011 15:45:38 GMT campbell [500] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Use dependent pointer type to ensure that the representation is ... Fri, 11 Feb 2011 15:45:37 GMT campbell [499] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) pointer_compat is a little more natural if it takes that block rather ... Fri, 11 Feb 2011 15:45:36 GMT campbell [498] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Make block type a little more abstract; remove knowledge about the ... Fri, 11 Feb 2011 15:45:35 GMT campbell [497] * Deliverables/D3.1/C-semantics/Mem.ma (modified) Remove bogus pointer compatibility case. Fri, 11 Feb 2011 15:45:28 GMT campbell [496] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) First pass at moving regions to block type. Fri, 11 Feb 2011 14:16:15 GMT mulligan [495] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more added Fri, 11 Feb 2011 11:11:12 GMT mulligan [494] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) more added Fri, 11 Feb 2011 10:40:03 GMT mulligan [493] * Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) incorporated some text from the eu report that needs to be pared down Fri, 11 Feb 2011 09:22:44 GMT mulligan [492] * Deliverables/D4.1/ITP-Paper (added) * Deliverables/D4.1/ITP-Paper/itp-2011.tex (added) * Deliverables/D4.1/ITP-Paper/llncs.cls (added) Initial commit of outline of prospective itp-2011 paper. Thu, 10 Feb 2011 14:28:59 GMT mulligan [491] * Deliverables/D4.2-4.3/ASM (added) * Deliverables/D4.2-4.3/ASM/I8051.ma (added) * Deliverables/D4.2-4.3/LIN (added) * Deliverables/D4.2-4.3/LIN/LIN.ma (added) * Deliverables/D4.2-4.3/LIN/LinToAsm.ma (added) * Deliverables/D4.2-4.3/common (added) * Deliverables/D4.2-4.3/common/AST.ma (added) * Deliverables/D4.2-4.3/common/CostLabel.ma (added) * Deliverables/D4.2-4.3/utilities (added) * Deliverables/D4.2-4.3/utilities/BitVectorTrieSet.ma (added) * Deliverables/D4.2-4.3/utilities/Compare.ma (added) * Deliverables/D4.2-4.3/utilities/StringTools.ma (added) Initial commit of (part)-formalisation of LIN intermediate language. Wed, 09 Feb 2011 17:22:34 GMT campbell [490] * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml (modified) Update syntax of Matita Clight term printer. Wed, 09 Feb 2011 17:22:34 GMT campbell [489] * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cutil.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/myocamlbuild_config.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/acc.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightInterpret.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightToCminor.ml (modified) Pointer fixes for the temporary version of the compiler that can ... Wed, 09 Feb 2011 10:58:37 GMT campbell [488] * Deliverables/D3.1/C-semantics/oldlib (added) * Deliverables/D3.1/C-semantics/oldlib/eq.ma (added) Some missing equality constants used by destruct. Wed, 09 Feb 2011 10:49:17 GMT campbell [487] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Animation.ma (modified) * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecEquiv.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Coqlib.ma (modified) * Deliverables/D3.1/C-semantics/CostLabel.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Errors.ma (modified) * Deliverables/D3.1/C-semantics/Events.ma (modified) * Deliverables/D3.1/C-semantics/Floats.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/IOMonad.ma (modified) * Deliverables/D3.1/C-semantics/Integers.ma (modified) * Deliverables/D3.1/C-semantics/Maps.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Smallstep.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) * Deliverables/D3.1/C-semantics/binary/Z.ma (modified) * Deliverables/D3.1/C-semantics/binary/positive.ma (modified) * Deliverables/D3.1/C-semantics/extralib.ma (modified) Port Clight semantics to the new-new matita syntax. Fri, 04 Feb 2011 12:52:46 GMT ayache [486] * Deliverables/D2.1/report.log (modified) * Deliverables/D2.1/report.pdf (modified) * Deliverables/D2.2 (added) * Deliverables/D2.2/8051 (added) * Deliverables/D2.2/8051/Makefile (added) * Deliverables/D2.2/8051/Makefile.config (added) * Deliverables/D2.2/8051/Makefile.generic (added) * Deliverables/D2.2/8051/Makefile.local (added) * Deliverables/D2.2/8051/README (added) * Deliverables/D2.2/8051/_tags (added) * Deliverables/D2.2/8051/acc.odocl (added) * Deliverables/D2.2/8051/admin (added) * Deliverables/D2.2/8051/admin/myocamldoc (added) * Deliverables/D2.2/8051/cparser (added) * Deliverables/D2.2/8051/cparser/.depend (added) * Deliverables/D2.2/8051/cparser/AddCasts.ml (added) * Deliverables/D2.2/8051/cparser/AddCasts.mli (added) * Deliverables/D2.2/8051/cparser/Bitfields.ml (added) * Deliverables/D2.2/8051/cparser/Bitfields.mli (added) * Deliverables/D2.2/8051/cparser/Builtins.ml (added) * Deliverables/D2.2/8051/cparser/Builtins.mli (added) * Deliverables/D2.2/8051/cparser/C.mli (added) * Deliverables/D2.2/8051/cparser/CBuiltins.ml (added) * Deliverables/D2.2/8051/cparser/Cabs.ml (added) * Deliverables/D2.2/8051/cparser/Cabshelper.ml (added) * Deliverables/D2.2/8051/cparser/Ceval.ml (added) * Deliverables/D2.2/8051/cparser/Ceval.mli (added) * Deliverables/D2.2/8051/cparser/Cleanup.ml (added) * Deliverables/D2.2/8051/cparser/Cleanup.mli (added) * Deliverables/D2.2/8051/cparser/Cprint.ml (added) * Deliverables/D2.2/8051/cparser/Cprint.mli (added) * Deliverables/D2.2/8051/cparser/Cutil.ml (added) * Deliverables/D2.2/8051/cparser/Cutil.mli (added) * Deliverables/D2.2/8051/cparser/Elab.ml (added) * Deliverables/D2.2/8051/cparser/Elab.mli (added) * Deliverables/D2.2/8051/cparser/Env.ml (added) * Deliverables/D2.2/8051/cparser/Env.mli (added) * Deliverables/D2.2/8051/cparser/Errors.ml (added) * Deliverables/D2.2/8051/cparser/Errors.mli (added) * Deliverables/D2.2/8051/cparser/GCC.ml (added) * Deliverables/D2.2/8051/cparser/GCC.mli (added) * Deliverables/D2.2/8051/cparser/Lexer.mli (added) * Deliverables/D2.2/8051/cparser/Lexer.mll (added) * Deliverables/D2.2/8051/cparser/Machine.ml (added) * Deliverables/D2.2/8051/cparser/Machine.mli (added) * Deliverables/D2.2/8051/cparser/Main.ml (added) * Deliverables/D2.2/8051/cparser/Makefile (added) * Deliverables/D2.2/8051/cparser/Parse.ml (added) * Deliverables/D2.2/8051/cparser/Parse.mli (added) * Deliverables/D2.2/8051/cparser/Parse_aux.ml (added) * Deliverables/D2.2/8051/cparser/Parse_aux.mli (added) * Deliverables/D2.2/8051/cparser/Parser.mly (added) * Deliverables/D2.2/8051/cparser/Rename.ml (added) * Deliverables/D2.2/8051/cparser/Rename.mli (added) * Deliverables/D2.2/8051/cparser/SimplExpr.ml (added) * Deliverables/D2.2/8051/cparser/SimplExpr.mli (added) * Deliverables/D2.2/8051/cparser/StructAssign.ml (added) * Deliverables/D2.2/8051/cparser/StructAssign.mli (added) * Deliverables/D2.2/8051/cparser/StructByValue.ml (added) * Deliverables/D2.2/8051/cparser/StructByValue.mli (added) * Deliverables/D2.2/8051/cparser/Transform.ml (added) * Deliverables/D2.2/8051/cparser/Transform.mli (added) * Deliverables/D2.2/8051/cparser/Unblock.ml (added) * Deliverables/D2.2/8051/cparser/Unblock.mli (added) * Deliverables/D2.2/8051/cparser/uint64.c (added) * Deliverables/D2.2/8051/distributed_files (added) * Deliverables/D2.2/8051/doc (added) * Deliverables/D2.2/8051/doc/html (added) * Deliverables/D2.2/8051/doc/html/style.css (added) * Deliverables/D2.2/8051/doc/src (added) * Deliverables/D2.2/8051/doc/src/main (added) * Deliverables/D2.2/8051/myocamlbuild.ml (added) * Deliverables/D2.2/8051/myocamlbuild_config.ml (added) * Deliverables/D2.2/8051/src (added) * Deliverables/D2.2/8051/src/ASM (added) * Deliverables/D2.2/8051/src/ASM/ASM.mli (added) * Deliverables/D2.2/8051/src/ASM/ASMCosts.ml (added) * Deliverables/D2.2/8051/src/ASM/ASMCosts.mli (added) * Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml (added) * Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli (added) * Deliverables/D2.2/8051/src/ASM/ASMPrinter.ml (added) * Deliverables/D2.2/8051/src/ASM/ASMPrinter.mli (added) * Deliverables/D2.2/8051/src/ASM/BitVectors.ml (added) * Deliverables/D2.2/8051/src/ASM/BitVectors.mli (added) * Deliverables/D2.2/8051/src/ASM/I8051.ml (added) * Deliverables/D2.2/8051/src/ASM/I8051.mli (added) * Deliverables/D2.2/8051/src/ASM/IntelHex.ml (added) * Deliverables/D2.2/8051/src/ASM/IntelHex.mli (added) * Deliverables/D2.2/8051/src/ASM/MIPS.ml (added) * Deliverables/D2.2/8051/src/ASM/MIPS.mli (added) * Deliverables/D2.2/8051/src/ASM/MIPSInterpret.ml (added) * Deliverables/D2.2/8051/src/ASM/MIPSInterpret.mli (added) * Deliverables/D2.2/8051/src/ASM/MIPSOps.mli (added) * Deliverables/D2.2/8051/src/ASM/Parser.ml (added) * Deliverables/D2.2/8051/src/ASM/Parser.mli (added) * Deliverables/D2.2/8051/src/ASM/Physical.ml (added) * Deliverables/D2.2/8051/src/ASM/Physical.mli (added) * Deliverables/D2.2/8051/src/ASM/Util.ml (added) * Deliverables/D2.2/8051/src/ASM/arch.mli (added) * Deliverables/D2.2/8051/src/ASM/printOps.ml (added) * Deliverables/D2.2/8051/src/ASM/printOps.mli (added) * Deliverables/D2.2/8051/src/ERTL (added) * Deliverables/D2.2/8051/src/ERTL/ERTL.mli (added) * Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml (added) * Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.mli (added) * Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml (added) * Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.mli (added) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml (added) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.mli (added) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml (added) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.mli (added) * Deliverables/D2.2/8051/src/ERTL/build.ml (added) * Deliverables/D2.2/8051/src/ERTL/build.mli (added) * Deliverables/D2.2/8051/src/ERTL/liveness.ml (added) * Deliverables/D2.2/8051/src/ERTL/liveness.mli (added) * Deliverables/D2.2/8051/src/ERTL/spill.ml (added) * Deliverables/D2.2/8051/src/ERTL/spill.mli (added) * Deliverables/D2.2/8051/src/ERTL/uses.ml (added) * Deliverables/D2.2/8051/src/ERTL/uses.mli (added) * Deliverables/D2.2/8051/src/LIN (added) * Deliverables/D2.2/8051/src/LIN/LIN.mli (added) * Deliverables/D2.2/8051/src/LIN/LINInterpret.ml (added) * Deliverables/D2.2/8051/src/LIN/LINInterpret.mli (added) * Deliverables/D2.2/8051/src/LIN/LINPrinter.ml (added) * Deliverables/D2.2/8051/src/LIN/LINPrinter.mli (added) * Deliverables/D2.2/8051/src/LIN/LINToASM.ml (added) * Deliverables/D2.2/8051/src/LIN/LINToASM.mli (added) * Deliverables/D2.2/8051/src/LTL (added) * Deliverables/D2.2/8051/src/LTL/LTL.mli (added) * Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml (added) * Deliverables/D2.2/8051/src/LTL/LTLInterpret.mli (added) * Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml (added) * Deliverables/D2.2/8051/src/LTL/LTLPrinter.mli (added) * Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml (added) * Deliverables/D2.2/8051/src/LTL/LTLToLIN.mli (added) * Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml (added) * Deliverables/D2.2/8051/src/LTL/LTLToLINI.mli (added) * Deliverables/D2.2/8051/src/LTL/branch.ml (added) * Deliverables/D2.2/8051/src/LTL/branch.mli (added) * Deliverables/D2.2/8051/src/RTL (added) * Deliverables/D2.2/8051/src/RTL/RTL.mli (added) * Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml (added) * Deliverables/D2.2/8051/src/RTL/RTLInterpret.mli (added) * Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml (added) * Deliverables/D2.2/8051/src/RTL/RTLPrinter.mli (added) * Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml (added) * Deliverables/D2.2/8051/src/RTL/RTLToERTL.mli (added) * Deliverables/D2.2/8051/src/RTL/RTLtailcall.ml (added) * Deliverables/D2.2/8051/src/RTL/RTLtailcall.mli (added) * Deliverables/D2.2/8051/src/RTLabs (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.mli (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml (added) * Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.mli (added) * Deliverables/D2.2/8051/src/acc.ml (added) * Deliverables/D2.2/8051/src/acc.mli (added) * Deliverables/D2.2/8051/src/checker.ml (added) * Deliverables/D2.2/8051/src/checker.mli (added) * Deliverables/D2.2/8051/src/clight (added) * Deliverables/D2.2/8051/src/clight/clight.mli (added) * Deliverables/D2.2/8051/src/clight/clightAnnotator.ml (added) * Deliverables/D2.2/8051/src/clight/clightAnnotator.mli (added) * Deliverables/D2.2/8051/src/clight/clightFlags.ml (added) * Deliverables/D2.2/8051/src/clight/clightFromC.ml (added) * Deliverables/D2.2/8051/src/clight/clightInterpret.ml (added) * Deliverables/D2.2/8051/src/clight/clightInterpret.mli (added) * Deliverables/D2.2/8051/src/clight/clightLabelling.ml (added) * Deliverables/D2.2/8051/src/clight/clightLabelling.mli (added) * Deliverables/D2.2/8051/src/clight/clightParser.ml (added) * Deliverables/D2.2/8051/src/clight/clightParser.mli (added) * Deliverables/D2.2/8051/src/clight/clightPrinter.ml (added) * Deliverables/D2.2/8051/src/clight/clightPrinter.mli (added) * Deliverables/D2.2/8051/src/clight/clightToCminor.ml (added) * Deliverables/D2.2/8051/src/clight/clightToCminor.mli (added) * Deliverables/D2.2/8051/src/clight/clightUtils.ml (added) * Deliverables/D2.2/8051/src/clight/clightUtils.mli (added) * Deliverables/D2.2/8051/src/cminor (added) * Deliverables/D2.2/8051/src/cminor/cminor.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorAnnotator.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorFold.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorFold.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorInterpret.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorLabelling.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorLabelling.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorLexer.mll (added) * Deliverables/D2.2/8051/src/cminor/cminorParser.mly (added) * Deliverables/D2.2/8051/src/cminor/cminorPointers.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorPointers.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorPrinter.mli (added) * Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml (added) * Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.mli (added) * Deliverables/D2.2/8051/src/common (added) * Deliverables/D2.2/8051/src/common/AST.mli (added) * Deliverables/D2.2/8051/src/common/atom.ml (added) * Deliverables/D2.2/8051/src/common/atom.mli (added) * Deliverables/D2.2/8051/src/common/atomSig.mli (added) * Deliverables/D2.2/8051/src/common/costLabel.ml (added) * Deliverables/D2.2/8051/src/common/costLabel.mli (added) * Deliverables/D2.2/8051/src/common/hdwRegister.ml (added) * Deliverables/D2.2/8051/src/common/hdwRegister.mli (added) * Deliverables/D2.2/8051/src/common/intValue.ml (added) * Deliverables/D2.2/8051/src/common/intValue.mli (added) * Deliverables/D2.2/8051/src/common/label.ml (added) * Deliverables/D2.2/8051/src/common/label.mli (added) * Deliverables/D2.2/8051/src/common/memory.ml (added) * Deliverables/D2.2/8051/src/common/memory.mli (added) * Deliverables/D2.2/8051/src/common/primitive.ml (added) * Deliverables/D2.2/8051/src/common/primitive.mli (added) * Deliverables/D2.2/8051/src/common/register.ml (added) * Deliverables/D2.2/8051/src/common/register.mli (added) * Deliverables/D2.2/8051/src/common/value.ml (added) * Deliverables/D2.2/8051/src/common/value.mli (added) * Deliverables/D2.2/8051/src/dev_test.ml (added) * Deliverables/D2.2/8051/src/driver.ml (added) * Deliverables/D2.2/8051/src/driver.mli (added) * Deliverables/D2.2/8051/src/languages.ml (added) * Deliverables/D2.2/8051/src/languages.mli (added) * Deliverables/D2.2/8051/src/options.ml (added) * Deliverables/D2.2/8051/src/options.mli (added) * Deliverables/D2.2/8051/src/utilities (added) * Deliverables/D2.2/8051/src/utilities/Fix.ml (added) * Deliverables/D2.2/8051/src/utilities/Fix.mli (added) * Deliverables/D2.2/8051/src/utilities/bijection.ml (added) * Deliverables/D2.2/8051/src/utilities/bijection.mli (added) * Deliverables/D2.2/8051/src/utilities/coloring.ml (added) * Deliverables/D2.2/8051/src/utilities/coloring.mli (added) * Deliverables/D2.2/8051/src/utilities/error.ml (added) * Deliverables/D2.2/8051/src/utilities/error.mli (added) * Deliverables/D2.2/8051/src/utilities/integer.ml (added) * Deliverables/D2.2/8051/src/utilities/integer.mli (added) * Deliverables/D2.2/8051/src/utilities/interference.ml (added) * Deliverables/D2.2/8051/src/utilities/interference.mli (added) * Deliverables/D2.2/8051/src/utilities/misc.ml (added) * Deliverables/D2.2/8051/src/utilities/misc.mli (added) * Deliverables/D2.2/8051/src/utilities/miscPottier.ml (added) * Deliverables/D2.2/8051/src/utilities/miscPottier.mli (added) * Deliverables/D2.2/8051/src/utilities/myMap.ml (added) * Deliverables/D2.2/8051/src/utilities/myMap.mli (added) * Deliverables/D2.2/8051/src/utilities/option.ml (added) * Deliverables/D2.2/8051/src/utilities/option.mli (added) * Deliverables/D2.2/8051/src/utilities/optionsParsing.ml (added) * Deliverables/D2.2/8051/src/utilities/position.ml (added) * Deliverables/D2.2/8051/src/utilities/position.mli (added) * Deliverables/D2.2/8051/src/utilities/print.ml (added) * Deliverables/D2.2/8051/src/utilities/print.mli (added) * Deliverables/D2.2/8051/src/utilities/printCFG.ml (added) * Deliverables/D2.2/8051/src/utilities/printCFG.mli (added) * Deliverables/D2.2/8051/src/utilities/printPottier.ml (added) * Deliverables/D2.2/8051/src/utilities/printPottier.mli (added) * Deliverables/D2.2/8051/src/utilities/prioritySet.ml (added) * Deliverables/D2.2/8051/src/utilities/prioritySet.mli (added) * Deliverables/D2.2/8051/src/utilities/setMap.ml (added) * Deliverables/D2.2/8051/src/utilities/setMap.mli (added) * Deliverables/D2.2/8051/src/utilities/stringSig.mli (added) * Deliverables/D2.2/8051/src/utilities/stringTools.ml (added) * Deliverables/D2.2/8051/src/utilities/stringTools.mli (added) * Deliverables/D2.2/8051/src/utilities/syntacticAnalysis.ml (added) * Deliverables/D2.2/8051/src/utilities/syntacticAnalysis.mli (added) * Deliverables/D2.2/8051/src/utilities/unionFind.ml (added) * Deliverables/D2.2/8051/src/utilities/unionFind.mli (added) * Deliverables/D2.2/8051/tests (added) * Deliverables/D2.2/8051/tests/Makefile (added) * Deliverables/D2.2/8051/tests/clight (added) * Deliverables/D2.2/8051/tests/clight/Makefile (added) * Deliverables/D2.2/8051/tests/clight/array.c (added) * Deliverables/D2.2/8051/tests/clight/array.c.expected (added) * Deliverables/D2.2/8051/tests/clight/array.log.expected (added) * Deliverables/D2.2/8051/tests/clight/binop.c (added) * Deliverables/D2.2/8051/tests/clight/binop.c.expected (added) * Deliverables/D2.2/8051/tests/clight/binop.log.expected (added) * Deliverables/D2.2/8051/tests/clight/complets.c (added) * Deliverables/D2.2/8051/tests/clight/complets.c.expected (added) * Deliverables/D2.2/8051/tests/clight/complets.log.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.ASM.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.Clight.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.Cminor.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.ERTL.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.LIN.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.LTL.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.RTL.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.RTLabs.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.c (added) * Deliverables/D2.2/8051/tests/clight/fib.c.expected (added) * Deliverables/D2.2/8051/tests/clight/fib.log.expected (added) * Deliverables/D2.2/8051/tests/clight/fir4.c (added) * Deliverables/D2.2/8051/tests/clight/fir4.c.expected (added) * Deliverables/D2.2/8051/tests/clight/fir4.log.expected (added) * Deliverables/D2.2/8051/tests/clight/fir_complexe.c (added) * Deliverables/D2.2/8051/tests/clight/fir_complexe.c.expected (added) * Deliverables/D2.2/8051/tests/clight/fir_complexe.log.expected (added) * Deliverables/D2.2/8051/tests/clight/for.c (added) * Deliverables/D2.2/8051/tests/clight/for.c.expected (added) * Deliverables/D2.2/8051/tests/clight/for.log.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.ASM.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.Clight.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.Cminor.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.ERTL.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.LIN.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.LTL.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.RTL.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.RTLabs.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.c (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.c.expected (added) * Deliverables/D2.2/8051/tests/clight/ifthenelse.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testCOMP_tri.c (added) * Deliverables/D2.2/8051/tests/clight/testCOMP_tri.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testCOMP_tri.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_LE.c (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_LE.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_LE.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_double.c (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_double.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_double.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_ecriture.c (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_ecriture.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_ecriture.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_lecture.c (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_lecture.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_Array_lecture.log.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_boucle.c (added) * Deliverables/D2.2/8051/tests/clight/testTB_boucle.c.expected (added) * Deliverables/D2.2/8051/tests/clight/testTB_boucle.log.expected (added) * Deliverables/D2.2/Report (added) * Deliverables/D2.2/Report/report.pdf (added) * Deliverables/D2.3/8051/myocamlbuild_config.ml (modified) Deliverable D2.2 Wed, 02 Feb 2011 11:41:05 GMT campbell [485] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecEquiv.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Errors.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/test/insertsort.c (modified) * Deliverables/D3.1/C-semantics/test/string.c (added) Fix treatment of pointers in initialisation data, a little like later ... Fri, 28 Jan 2011 13:41:49 GMT campbell [484] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Separate out null values from integer zeros. Fri, 28 Jan 2011 13:41:48 GMT campbell [483] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Use pointer-specific "chunks" of memory for pointer loads and stores, ... Fri, 28 Jan 2011 13:41:46 GMT campbell [482] * Deliverables/D3.1/C-semantics/Values.ma (modified) Note the purpose of the region in a pointer value. Tue, 25 Jan 2011 17:22:21 GMT campbell [481] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) Tcomp_ptr should take the memory region and use that to calculate its ... Tue, 25 Jan 2011 16:30:37 GMT campbell [480] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) "memory_space" to "region" replacement to match ocaml code Tue, 25 Jan 2011 16:30:36 GMT campbell [479] * Deliverables/D3.1/C-semantics/test/insertsort.c (added) Test of linked list insertion sort. Tue, 25 Jan 2011 16:30:36 GMT campbell [478] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Animation.ma (modified) * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Events.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Prevent clashes between names in AST and other parts of the ... Mon, 24 Jan 2011 13:57:45 GMT mulligan [477] * Deliverables/LIN.ma (added) Added file for LIN. Mon, 24 Jan 2011 13:37:51 GMT mulligan [476] * Deliverables/D4.2-4.3 (added) Commiting directory for formalization of intermediate compiler languages. Mon, 24 Jan 2011 09:47:38 GMT mulligan [475] * Deliverables/D4.1/Matita/new-matita-development (added) * Deliverables/D4.1/Matita/new-matita-development/ASM.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Arithmetic.ma (added) * Deliverables/D4.1/Matita/new-matita-development/BitVector.ma (added) * Deliverables/D4.1/Matita/new-matita-development/BitVectorTrie.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Char.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Fetch.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Interpret.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Status.ma (added) * Deliverables/D4.1/Matita/new-matita-development/String.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Util.ma (added) * Deliverables/D4.1/Matita/new-matita-development/Vector.ma (added) Matita interpreter ported to latest version of matita (the one with ... Fri, 21 Jan 2011 13:31:00 GMT campbell [474] * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Events.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/depends (modified) Reduce "include"s to reduce compilation time. (Will be undone when ... Fri, 21 Jan 2011 13:31:00 GMT campbell [473] * Deliverables/D3.1/C-semantics/Coqlib.ma (modified) * Deliverables/D3.1/C-semantics/depends (modified) Track changes in nlibrary list-theory.ma -> list.ma Fri, 21 Jan 2011 10:08:00 GMT mulligan [472] * Deliverables/D4.1/Matita/Debug.ma (modified) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/depends (modified) More changes to debug and testing files to get them to work with the ... Fri, 21 Jan 2011 09:19:52 GMT mulligan [471] * Deliverables/D4.1/Matita/Bool.ma (deleted) * Deliverables/D4.1/Matita/Cartesian.ma (deleted) * Deliverables/D4.1/Matita/Compare.ma (deleted) * Deliverables/D4.1/Matita/Connectives.ma (deleted) * Deliverables/D4.1/Matita/Either.ma (deleted) * Deliverables/D4.1/Matita/Exponential.ma (deleted) * Deliverables/D4.1/Matita/List.ma (deleted) * Deliverables/D4.1/Matita/Maybe.ma (deleted) * Deliverables/D4.1/Matita/Nat.ma (deleted) Deleted (now) superfluous custom library files in favour of using ... Fri, 21 Jan 2011 09:18:27 GMT mulligan [470] * Deliverables/D4.1/Matita/Interpret.ma (modified) Finished moving development over to standard library. Fri, 21 Jan 2011 09:02:21 GMT campbell [469] * Deliverables/D3.1/C-semantics/SmallstepExec.ma (modified) Update work-in-progress file to match current development. Fri, 21 Jan 2011 09:02:21 GMT campbell [468] * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) Missing changes to completeness proof for function pointer type fix. Fri, 21 Jan 2011 09:02:20 GMT campbell [467] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) Update some of the commented-out parts of Globalenvs for testing. Thu, 20 Jan 2011 17:46:21 GMT mulligan [466] * Deliverables/D4.1/Matita/Interpret.ma (modified) Most of execute_1 checked. Need to fix negations, though, in rest in ... Thu, 20 Jan 2011 17:10:07 GMT mulligan [465] * Deliverables/D4.1/Matita/ASM.ma (modified) * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/Fetch.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) * Deliverables/D4.1/Matita/String.ma (modified) * Deliverables/D4.1/Matita/Test.ma (modified) * Deliverables/D4.1/Matita/Util.ma (modified) * Deliverables/D4.1/Matita/Vector.ma (modified) * Deliverables/D4.1/Matita/depends (modified) Moved over to standard library. Thu, 20 Jan 2011 12:35:13 GMT mulligan [464] * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) Fixed strange bug/typo in BitVectorTrie.ma Thu, 20 Jan 2011 12:33:25 GMT mulligan [463] * Deliverables/D4.1/Matita/DoTest.ma (modified) Fixed DoTest so that it doesn't take an hour to typecheck. Thu, 20 Jan 2011 12:32:32 GMT mulligan [462] * Deliverables/D4.1/Matita/Arithmetic.ma (modified) * Deliverables/D4.1/Matita/BitVector.ma (modified) * Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) * Deliverables/D4.1/Matita/depends (modified) Added bitvector arithmetic for Brian. Wed, 19 Jan 2011 17:23:28 GMT campbell [461] * Deliverables/D2.3/8051-memoryspaces-branch/cparser/C.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Ceval.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cprint.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cutil.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightInterpret.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightToCminor.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/cminor/cminorPrinter.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/AST.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/intValue.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/intValue.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/memory.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/memory.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/value.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/common/value.mli (modified) Handle null pointer constants properly for generic pointers ... Wed, 19 Jan 2011 17:23:27 GMT campbell [460] * Deliverables/D2.3/8051-memoryspaces-branch/cparser/AddCasts.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Bitfields.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Builtins.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/C.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Ceval.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cleanup.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cprint.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cutil.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Elab.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Env.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Env.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/GCC.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Lexer.mll (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Parser.mly (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Rename.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/SimplExpr.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/StructAssign.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/StructByValue.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Transform.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/cparser/Unblock.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/myocamlbuild_config.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/acc.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightAnnotator.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightInterpret.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml (added) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightToCminor.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/languages.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/languages.mli (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/options.ml (modified) * Deliverables/D2.3/8051-memoryspaces-branch/src/options.mli (modified) Port memory spaces changes to latest prototype compiler. Wed, 19 Jan 2011 16:22:54 GMT campbell [459] * Deliverables/D2.3/8051-memoryspaces-branch (copied) Create branch of the prototype compiler for memory space support Wed, 19 Jan 2011 14:16:39 GMT campbell [458] * Deliverables/D3.1/C-semantics/test/null-local.c (added) * Deliverables/D3.1/C-semantics/test/null.c (added) * Deliverables/D3.1/C-semantics/test/spaces.c (added) Add a few more pointer tests. Wed, 19 Jan 2011 14:06:10 GMT campbell [457] * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/test/funptr.ma (added) Correct checking of function pointers. Wed, 19 Jan 2011 10:45:13 GMT campbell [456] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) Add 24bit initialisation data for null generic pointers. Wed, 19 Jan 2011 09:58:43 GMT mulligan [455] * Deliverables/D4.1/ASMInterpret.mli (modified) Merge commit. Tue, 18 Jan 2011 18:23:28 GMT sacerdot [454] * Deliverables/D4.1/ASM.mli (modified) * Deliverables/D4.1/ASMCosts.ml (added) * Deliverables/D4.1/ASMCosts.mli (added) * Deliverables/D4.1/ASMInterpret.ml (modified) * Deliverables/D4.1/ASMInterpret.mli (modified) * Deliverables/D4.1/Physical.ml (modified) * Deliverables/D4.1/Physical.mli (modified) * Deliverables/D4.1/Pretty.ml (modified) * Deliverables/D4.1/Pretty.mli (modified) * Deliverables/D4.1/Util.ml (modified) CSC + Nicolas + Dominic: 1) back-porting of changes by Nicolas from ... Mon, 17 Jan 2011 09:36:28 GMT ayache [453] * Deliverables/D2.3 (added) * Deliverables/D2.3/8051 (added) * Deliverables/D2.3/8051/Makefile (added) * Deliverables/D2.3/8051/Makefile.config (added) * Deliverables/D2.3/8051/Makefile.generic (added) * Deliverables/D2.3/8051/Makefile.local (added) * Deliverables/D2.3/8051/README (added) * Deliverables/D2.3/8051/TODO (added) * Deliverables/D2.3/8051/_tags (added) * Deliverables/D2.3/8051/acc.odocl (added) * Deliverables/D2.3/8051/admin (added) * Deliverables/D2.3/8051/admin/myocamldoc (added) * Deliverables/D2.3/8051/cparser (added) * Deliverables/D2.3/8051/cparser/.depend (added) * Deliverables/D2.3/8051/cparser/AddCasts.ml (added) * Deliverables/D2.3/8051/cparser/AddCasts.mli (added) * Deliverables/D2.3/8051/cparser/Bitfields.ml (added) * Deliverables/D2.3/8051/cparser/Bitfields.mli (added) * Deliverables/D2.3/8051/cparser/Builtins.ml (added) * Deliverables/D2.3/8051/cparser/Builtins.mli (added) * Deliverables/D2.3/8051/cparser/C.mli (added) * Deliverables/D2.3/8051/cparser/CBuiltins.ml (added) * Deliverables/D2.3/8051/cparser/Cabs.ml (added) * Deliverables/D2.3/8051/cparser/Cabshelper.ml (added) * Deliverables/D2.3/8051/cparser/Ceval.ml (added) * Deliverables/D2.3/8051/cparser/Ceval.mli (added) * Deliverables/D2.3/8051/cparser/Cleanup.ml (added) * Deliverables/D2.3/8051/cparser/Cleanup.mli (added) * Deliverables/D2.3/8051/cparser/Cprint.ml (added) * Deliverables/D2.3/8051/cparser/Cprint.mli (added) * Deliverables/D2.3/8051/cparser/Cutil.ml (added) * Deliverables/D2.3/8051/cparser/Cutil.mli (added) * Deliverables/D2.3/8051/cparser/Elab.ml (added) * Deliverables/D2.3/8051/cparser/Elab.mli (added) * Deliverables/D2.3/8051/cparser/Env.ml (added) * Deliverables/D2.3/8051/cparser/Env.mli (added) * Deliverables/D2.3/8051/cparser/Errors.ml (added) * Deliverables/D2.3/8051/cparser/Errors.mli (added) * Deliverables/D2.3/8051/cparser/GCC.ml (added) * Deliverables/D2.3/8051/cparser/GCC.mli (added) * Deliverables/D2.3/8051/cparser/Lexer.mli (added) * Deliverables/D2.3/8051/cparser/Lexer.mll (added) * Deliverables/D2.3/8051/cparser/Machine.ml (added) * Deliverables/D2.3/8051/cparser/Machine.mli (added) * Deliverables/D2.3/8051/cparser/Main.ml (added) * Deliverables/D2.3/8051/cparser/Makefile (added) * Deliverables/D2.3/8051/cparser/Parse.ml (added) * Deliverables/D2.3/8051/cparser/Parse.mli (added) * Deliverables/D2.3/8051/cparser/Parse_aux.ml (added) * Deliverables/D2.3/8051/cparser/Parse_aux.mli (added) * Deliverables/D2.3/8051/cparser/Parser.mly (added) * Deliverables/D2.3/8051/cparser/Rename.ml (added) * Deliverables/D2.3/8051/cparser/Rename.mli (added) * Deliverables/D2.3/8051/cparser/SimplExpr.ml (added) * Deliverables/D2.3/8051/cparser/SimplExpr.mli (added) * Deliverables/D2.3/8051/cparser/StructAssign.ml (added) * Deliverables/D2.3/8051/cparser/StructAssign.mli (added) * Deliverables/D2.3/8051/cparser/StructByValue.ml (added) * Deliverables/D2.3/8051/cparser/StructByValue.mli (added) * Deliverables/D2.3/8051/cparser/Transform.ml (added) * Deliverables/D2.3/8051/cparser/Transform.mli (added) * Deliverables/D2.3/8051/cparser/Unblock.ml (added) * Deliverables/D2.3/8051/cparser/Unblock.mli (added) * Deliverables/D2.3/8051/cparser/uint64.c (added) * Deliverables/D2.3/8051/distributed_files (added) * Deliverables/D2.3/8051/doc (added) * Deliverables/D2.3/8051/doc/html (added) * Deliverables/D2.3/8051/doc/html/style.css (added) * Deliverables/D2.3/8051/doc/src (added) * Deliverables/D2.3/8051/doc/src/main (added) * Deliverables/D2.3/8051/log (added) * Deliverables/D2.3/8051/myocamlbuild.ml (added) * Deliverables/D2.3/8051/myocamlbuild_config.ml (added) * Deliverables/D2.3/8051/src (added) * Deliverables/D2.3/8051/src/ASM (added) * Deliverables/D2.3/8051/src/ASM/ASM.mli (added) * Deliverables/D2.3/8051/src/ASM/ASMCosts.ml (added) * Deliverables/D2.3/8051/src/ASM/ASMCosts.mli (added) * Deliverables/D2.3/8051/src/ASM/ASMInterpret.ml (added) * Deliverables/D2.3/8051/src/ASM/ASMInterpret.mli (added) * Deliverables/D2.3/8051/src/ASM/ASMPrinter.ml (added) * Deliverables/D2.3/8051/src/ASM/ASMPrinter.mli (added) * Deliverables/D2.3/8051/src/ASM/BitVectors.ml (added) * Deliverables/D2.3/8051/src/ASM/BitVectors.mli (added) * Deliverables/D2.3/8051/src/ASM/I8051.ml (added) * Deliverables/D2.3/8051/src/ASM/I8051.mli (added) * Deliverables/D2.3/8051/src/ASM/IntelHex.ml (added) * Deliverables/D2.3/8051/src/ASM/IntelHex.mli (added) * Deliverables/D2.3/8051/src/ASM/MIPS.ml (added) * Deliverables/D2.3/8051/src/ASM/MIPS.mli (added) * Deliverables/D2.3/8051/src/ASM/MIPSInterpret.ml (added) * Deliverables/D2.3/8051/src/ASM/MIPSInterpret.mli (added) * Deliverables/D2.3/8051/src/ASM/MIPSOps.mli (added) * Deliverables/D2.3/8051/src/ASM/Parser.ml (added) * Deliverables/D2.3/8051/src/ASM/Parser.mli (added) * Deliverables/D2.3/8051/src/ASM/Physical.ml (added) * Deliverables/D2.3/8051/src/ASM/Physical.mli (added) * Deliverables/D2.3/8051/src/ASM/Util.ml (added) * Deliverables/D2.3/8051/src/ASM/arch.mli (added) * Deliverables/D2.3/8051/src/ASM/printOps.ml (added) * Deliverables/D2.3/8051/src/ASM/printOps.mli (added) * Deliverables/D2.3/8051/src/ERTL (added) * Deliverables/D2.3/8051/src/ERTL/ERTL.mli (added) * Deliverables/D2.3/8051/src/ERTL/ERTLInterpret.ml (added) * Deliverables/D2.3/8051/src/ERTL/ERTLInterpret.mli (added) * Deliverables/D2.3/8051/src/ERTL/ERTLPrinter.ml (added) * Deliverables/D2.3/8051/src/ERTL/ERTLPrinter.mli (added) * Deliverables/D2.3/8051/src/ERTL/ERTLToLTL.ml (added) * Deliverables/D2.3/8051/src/ERTL/ERTLToLTL.mli (added) * Deliverables/D2.3/8051/src/ERTL/ERTLToLTLI.ml (added) * Deliverables/D2.3/8051/src/ERTL/ERTLToLTLI.mli (added) * Deliverables/D2.3/8051/src/ERTL/build.ml (added) * Deliverables/D2.3/8051/src/ERTL/build.mli (added) * Deliverables/D2.3/8051/src/ERTL/liveness.ml (added) * Deliverables/D2.3/8051/src/ERTL/liveness.mli (added) * Deliverables/D2.3/8051/src/ERTL/spill.ml (added) * Deliverables/D2.3/8051/src/ERTL/spill.mli (added) * Deliverables/D2.3/8051/src/ERTL/uses.ml (added) * Deliverables/D2.3/8051/src/ERTL/uses.mli (added) * Deliverables/D2.3/8051/src/LIN (added) * Deliverables/D2.3/8051/src/LIN/LIN.mli (added) * Deliverables/D2.3/8051/src/LIN/LINInterpret.ml (added) * Deliverables/D2.3/8051/src/LIN/LINInterpret.mli (added) * Deliverables/D2.3/8051/src/LIN/LINPrinter.ml (added) * Deliverables/D2.3/8051/src/LIN/LINPrinter.mli (added) * Deliverables/D2.3/8051/src/LIN/LINToASM.ml (added) * Deliverables/D2.3/8051/src/LIN/LINToASM.mli (added) * Deliverables/D2.3/8051/src/LTL (added) * Deliverables/D2.3/8051/src/LTL/LTL.mli (added) * Deliverables/D2.3/8051/src/LTL/LTLInterpret.ml (added) * Deliverables/D2.3/8051/src/LTL/LTLInterpret.mli (added) * Deliverables/D2.3/8051/src/LTL/LTLPrinter.ml (added) * Deliverables/D2.3/8051/src/LTL/LTLPrinter.mli (added) * Deliverables/D2.3/8051/src/LTL/LTLToLIN.ml (added) * Deliverables/D2.3/8051/src/LTL/LTLToLIN.mli (added) * Deliverables/D2.3/8051/src/LTL/LTLToLINI.ml (added) * Deliverables/D2.3/8051/src/LTL/LTLToLINI.mli (added) * Deliverables/D2.3/8051/src/LTL/branch.ml (added) * Deliverables/D2.3/8051/src/LTL/branch.mli (added) * Deliverables/D2.3/8051/src/RTL (added) * Deliverables/D2.3/8051/src/RTL/RTL.mli (added) * Deliverables/D2.3/8051/src/RTL/RTLInterpret.ml (added) * Deliverables/D2.3/8051/src/RTL/RTLInterpret.mli (added) * Deliverables/D2.3/8051/src/RTL/RTLPrinter.ml (added) * Deliverables/D2.3/8051/src/RTL/RTLPrinter.mli (added) * Deliverables/D2.3/8051/src/RTL/RTLToERTL.ml (added) * Deliverables/D2.3/8051/src/RTL/RTLToERTL.mli (added) * Deliverables/D2.3/8051/src/RTL/RTLtailcall.ml (added) * Deliverables/D2.3/8051/src/RTL/RTLtailcall.mli (added) * Deliverables/D2.3/8051/src/RTLabs (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabs.mli (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsInterpret.ml (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsInterpret.mli (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsPrinter.ml (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsPrinter.mli (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsToRTL.ml (added) * Deliverables/D2.3/8051/src/RTLabs/RTLabsToRTL.mli (added) * Deliverables/D2.3/8051/src/acc.ml (added) * Deliverables/D2.3/8051/src/acc.mli (added) * Deliverables/D2.3/8051/src/checker.ml (added) * Deliverables/D2.3/8051/src/checker.mli (added) * Deliverables/D2.3/8051/src/clight (added) * Deliverables/D2.3/8051/src/clight/clight.mli (added) * Deliverables/D2.3/8051/src/clight/clightAnnotator.ml (added) * Deliverables/D2.3/8051/src/clight/clightAnnotator.mli (added) * Deliverables/D2.3/8051/src/clight/clightFlags.ml (added) * Deliverables/D2.3/8051/src/clight/clightFromC.ml (added) * Deliverables/D2.3/8051/src/clight/clightInterpret.ml (added) * Deliverables/D2.3/8051/src/clight/clightInterpret.mli (added) * Deliverables/D2.3/8051/src/clight/clightLabelling.ml (added) * Deliverables/D2.3/8051/src/clight/clightLabelling.mli (added) * Deliverables/D2.3/8051/src/clight/clightParser.ml (added) * Deliverables/D2.3/8051/src/clight/clightParser.mli (added) * Deliverables/D2.3/8051/src/clight/clightPrinter.ml (added) * Deliverables/D2.3/8051/src/clight/clightPrinter.mli (added) * Deliverables/D2.3/8051/src/clight/clightToCminor.ml (added) * Deliverables/D2.3/8051/src/clight/clightToCminor.mli (added) * Deliverables/D2.3/8051/src/cminor (added) * Deliverables/D2.3/8051/src/cminor/cminor.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorAnnotator.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorAnnotator.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorFold.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorFold.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorInterpret.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorInterpret.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorLabelling.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorLabelling.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorLexer.mll (added) * Deliverables/D2.3/8051/src/cminor/cminorParser.mly (added) * Deliverables/D2.3/8051/src/cminor/cminorPointers.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorPointers.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorPrinter.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorPrinter.mli (added) * Deliverables/D2.3/8051/src/cminor/cminorToRTLabs.ml (added) * Deliverables/D2.3/8051/src/cminor/cminorToRTLabs.mli (added) * Deliverables/D2.3/8051/src/common (added) * Deliverables/D2.3/8051/src/common/AST.mli (added) * Deliverables/D2.3/8051/src/common/atom.ml (added) * Deliverables/D2.3/8051/src/common/atom.mli (added) * Deliverables/D2.3/8051/src/common/atomSig.mli (added) * Deliverables/D2.3/8051/src/common/costLabel.ml (added) * Deliverables/D2.3/8051/src/common/costLabel.mli (added) * Deliverables/D2.3/8051/src/common/hdwRegister.ml (added) * Deliverables/D2.3/8051/src/common/hdwRegister.mli (added) * Deliverables/D2.3/8051/src/common/intValue.ml (added) * Deliverables/D2.3/8051/src/common/intValue.mli (added) * Deliverables/D2.3/8051/src/common/label.ml (added) * Deliverables/D2.3/8051/src/common/label.mli (added) * Deliverables/D2.3/8051/src/common/memory.ml (added) * Deliverables/D2.3/8051/src/common/memory.mli (added) * Deliverables/D2.3/8051/src/common/primitive.ml (added) * Deliverables/D2.3/8051/src/common/primitive.mli (added) * Deliverables/D2.3/8051/src/common/register.ml (added) * Deliverables/D2.3/8051/src/common/register.mli (added) * Deliverables/D2.3/8051/src/common/value.ml (added) * Deliverables/D2.3/8051/src/common/value.mli (added) * Deliverables/D2.3/8051/src/dev_test.ml (added) * Deliverables/D2.3/8051/src/driver.ml (added) * Deliverables/D2.3/8051/src/driver.mli (added) * Deliverables/D2.3/8051/src/languages.ml (added) * Deliverables/D2.3/8051/src/languages.mli (added) * Deliverables/D2.3/8051/src/options.ml (added) * Deliverables/D2.3/8051/src/options.mli (added) * Deliverables/D2.3/8051/src/utilities (added) * Deliverables/D2.3/8051/src/utilities/Fix.ml (added) * Deliverables/D2.3/8051/src/utilities/Fix.mli (added) * Deliverables/D2.3/8051/src/utilities/bijection.ml (added) * Deliverables/D2.3/8051/src/utilities/bijection.mli (added) * Deliverables/D2.3/8051/src/utilities/coloring.ml (added) * Deliverables/D2.3/8051/src/utilities/coloring.mli (added) * Deliverables/D2.3/8051/src/utilities/error.ml (added) * Deliverables/D2.3/8051/src/utilities/error.mli (added) * Deliverables/D2.3/8051/src/utilities/integer.ml (added) * Deliverables/D2.3/8051/src/utilities/integer.mli (added) * Deliverables/D2.3/8051/src/utilities/interference.ml (added) * Deliverables/D2.3/8051/src/utilities/interference.mli (added) * Deliverables/D2.3/8051/src/utilities/misc.ml (added) * Deliverables/D2.3/8051/src/utilities/misc.mli (added) * Deliverables/D2.3/8051/src/utilities/miscPottier.ml (added) * Deliverables/D2.3/8051/src/utilities/miscPottier.mli (added) * Deliverables/D2.3/8051/src/utilities/myMap.ml (added) * Deliverables/D2.3/8051/src/utilities/myMap.mli (added) * Deliverables/D2.3/8051/src/utilities/option.ml (added) * Deliverables/D2.3/8051/src/utilities/option.mli (added) * Deliverables/D2.3/8051/src/utilities/optionsParsing.ml (added) * Deliverables/D2.3/8051/src/utilities/position.ml (added) * Deliverables/D2.3/8051/src/utilities/position.mli (added) * Deliverables/D2.3/8051/src/utilities/print.ml (added) * Deliverables/D2.3/8051/src/utilities/print.mli (added) * Deliverables/D2.3/8051/src/utilities/printCFG.ml (added) * Deliverables/D2.3/8051/src/utilities/printCFG.mli (added) * Deliverables/D2.3/8051/src/utilities/printPottier.ml (added) * Deliverables/D2.3/8051/src/utilities/printPottier.mli (added) * Deliverables/D2.3/8051/src/utilities/prioritySet.ml (added) * Deliverables/D2.3/8051/src/utilities/prioritySet.mli (added) * Deliverables/D2.3/8051/src/utilities/setMap.ml (added) * Deliverables/D2.3/8051/src/utilities/setMap.mli (added) * Deliverables/D2.3/8051/src/utilities/stringSig.mli (added) * Deliverables/D2.3/8051/src/utilities/stringTools.ml (added) * Deliverables/D2.3/8051/src/utilities/stringTools.mli (added) * Deliverables/D2.3/8051/src/utilities/syntacticAnalysis.ml (added) * Deliverables/D2.3/8051/src/utilities/syntacticAnalysis.mli (added) * Deliverables/D2.3/8051/src/utilities/unionFind.ml (added) * Deliverables/D2.3/8051/src/utilities/unionFind.mli (added) * Deliverables/D2.3/8051/tests (added) * Deliverables/D2.3/8051/tests/Makefile (added) * Deliverables/D2.3/8051/tests/benchs (added) * Deliverables/D2.3/8051/tests/benchs/Makefile (added) * Deliverables/D2.3/8051/tests/benchs/acc.run (added) * Deliverables/D2.3/8051/tests/benchs/badsort.c (added) * Deliverables/D2.3/8051/tests/benchs/fib.c (added) * Deliverables/D2.3/8051/tests/benchs/mat_det.c (added) * Deliverables/D2.3/8051/tests/benchs/meantime.sh (added) * Deliverables/D2.3/8051/tests/benchs/min.c (added) * Deliverables/D2.3/8051/tests/benchs/quicksort.c (added) * Deliverables/D2.3/8051/tests/benchs/search.c (added) * Deliverables/D2.3/8051/tests/clight (added) * Deliverables/D2.3/8051/tests/clight/Makefile (added) * Deliverables/D2.3/8051/tests/clight/array.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/array.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/array.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/array.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/array.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/array.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/array.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/array.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/array.c (added) * Deliverables/D2.3/8051/tests/clight/array.c.expected (added) * Deliverables/D2.3/8051/tests/clight/array.log.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.c (added) * Deliverables/D2.3/8051/tests/clight/binop.c.expected (added) * Deliverables/D2.3/8051/tests/clight/binop.log.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.c (added) * Deliverables/D2.3/8051/tests/clight/complets.c.expected (added) * Deliverables/D2.3/8051/tests/clight/complets.log.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.c (added) * Deliverables/D2.3/8051/tests/clight/fib.c.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.log.expected (added) * Deliverables/D2.3/8051/tests/clight/fib.s.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.c (added) * Deliverables/D2.3/8051/tests/clight/fir4.c.expected (added) * Deliverables/D2.3/8051/tests/clight/fir4.log.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.c (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.c.expected (added) * Deliverables/D2.3/8051/tests/clight/fir_complexe.log.expected (added) * Deliverables/D2.3/8051/tests/clight/for.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/for.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/for.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/for.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/for.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/for.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/for.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/for.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/for.c (added) * Deliverables/D2.3/8051/tests/clight/for.c.expected (added) * Deliverables/D2.3/8051/tests/clight/for.log.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.c (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.c.expected (added) * Deliverables/D2.3/8051/tests/clight/ifthenelse.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.c (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testCOMP_tri.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.c (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_LE.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.c (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_double.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.c (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_ecriture.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.c (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_Array_lecture.log.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.ASM.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.Clight.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.Cminor.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.ERTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.LIN.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.LTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.RTL.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.RTLabs.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.c (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.c.expected (added) * Deliverables/D2.3/8051/tests/clight/testTB_boucle.log.expected (added) Import of the Paris's sources. Fri, 14 Jan 2011 16:01:44 GMT mulligan [452] * Deliverables/D4.1/IntelHex.mli (modified) Added function to interface. Fri, 14 Jan 2011 15:54:56 GMT mulligan [451] * Deliverables/D4.1/Test.ml (modified) Removed more debugging stuff from Test.ml. Fri, 14 Jan 2011 15:54:00 GMT mulligan [450] * Deliverables/D4.1/Test.ml (modified) Comment added for Nicolas. Fri, 14 Jan 2011 15:51:40 GMT mulligan [449] * Deliverables/D4.1/Test.ml (modified) Removed debugging code from Test.ml. Fri, 14 Jan 2011 15:49:51 GMT mulligan [448] * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/Parser.ml (modified) * Deliverables/D4.1/Physical.ml (modified) * Deliverables/D4.1/Physical.mli (modified) * Deliverables/D4.1/Test.ml (modified) Got Intel HEX format exportation working. Fri, 14 Jan 2011 14:30:29 GMT mulligan [447] * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/Test.ml (modified) Checksum seems to be working now on most lines, barring three? Weird ... Fri, 14 Jan 2011 13:14:17 GMT mulligan [446] * Deliverables/D4.1/IntelHex.ml (modified) Checksum calculation added. Seems to still be buggy. Fri, 14 Jan 2011 12:33:37 GMT mulligan [445] * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/Test.ml (modified) Debugging hex output. Seems mcu8051 really doesn't like what's been ... Thu, 13 Jan 2011 13:19:14 GMT mulligan [444] * Deliverables/D4.1/ASMInterpret.ml (modified) * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/IntelHex.mli (modified) * Deliverables/D4.1/Test.ml (modified) Got Test.native to compile. Added functions for exporting intel hex ... Thu, 13 Jan 2011 10:35:18 GMT mulligan [443] * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/IntelHex.mli (modified) Wrote exportation code. Need to test it. Thu, 13 Jan 2011 09:54:42 GMT mulligan [442] * Deliverables/D4.1/IntelHex.ml (modified) * Deliverables/D4.1/IntelHex.mli (modified) * Deliverables/D4.1/Physical.ml (modified) * Deliverables/D4.1/Physical.mli (modified) Partial implementation of Nicolas' requested feature (extraction of ... Wed, 12 Jan 2011 14:22:14 GMT mulligan [441] * Deliverables/D4.1/ASMInterpret.ml (modified) Fixed bug in PUSH spotted by Nicolas. Thu, 16 Dec 2010 17:17:52 GMT mulligan [440] * Deliverables/D4.1/ASMInterpret.ml (modified) indentation changes by emacs Thu, 16 Dec 2010 17:17:14 GMT mulligan [439] * Deliverables/D4.1/Matita/Debug.ma (added) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/Interpret.ma (modified) * Deliverables/D4.1/Matita/Status.ma (modified) * Deliverables/D4.1/Matita/depends (modified) Changes to get everything to compile. Thu, 16 Dec 2010 02:05:31 GMT sacerdot [438] * Deliverables/D4.1/Report/report.tex (modified) Final version. Wed, 15 Dec 2010 22:35:37 GMT sacerdot [437] * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/Test.ma (modified) * Deliverables/D4.1/ToMatita.ml (modified) 1. new function assembly_unlabelled_program 2. the new function is ... Wed, 15 Dec 2010 22:20:05 GMT sacerdot [436] * Deliverables/D4.1/Matita/depends (modified) ... Wed, 15 Dec 2010 22:19:49 GMT sacerdot [435] * Deliverables/D4.1/Matita/Universes.ma (deleted) * Deliverables/D4.1/Matita/depends (modified) logic/pts.ma is now used in place of Universes.ma Wed, 15 Dec 2010 18:50:44 GMT mulligan [434] * Deliverables/D4.1/Report/report.tex (modified) Types added. Wed, 15 Dec 2010 18:42:04 GMT mulligan [433] * Deliverables/D4.1/Report/report.tex (modified) Most things added, just need to fill in types in table. Wed, 15 Dec 2010 18:21:02 GMT mulligan [432] * Deliverables/D4.1/Matita/Bool.ma (modified) * Deliverables/D4.1/Matita/Cartesian.ma (modified) * Deliverables/D4.1/Matita/Char.ma (modified) * Deliverables/D4.1/Matita/Compare.ma (modified) * Deliverables/D4.1/Matita/Plogic (deleted) * Deliverables/D4.1/Matita/depends (modified) * Deliverables/D4.1/Matita/root (modified) Removed Plogic/ Wed, 15 Dec 2010 17:38:59 GMT mulligan [431] * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/DoTest.ma (modified) * Deliverables/D4.1/Matita/README (modified) * Deliverables/D4.1/Matita/Test.ma (modified) * Deliverables/D4.1/Matita/depends (modified) - README updated - Test and DoTest fixed to work on assembly_program ... Wed, 15 Dec 2010 16:42:27 GMT mulligan [430] * Deliverables/D4.1/ToMatita.ml (modified) - ToMatita now generates a list of labelled_instructions (used to be ... Wed, 15 Dec 2010 16:16:29 GMT mulligan [429] * Deliverables/D4.1/README (modified) * Deliverables/D4.1/Test.ml (modified) * Deliverables/D4.1/ToMatita.ml (modified) 1) README upated 2) executable now reads the name of the HEX file ... Wed, 15 Dec 2010 16:04:37 GMT mulligan [428] * Deliverables/D4.1/ToMatita.ml (modified) Changed instr. to labelled_instr. Wed, 15 Dec 2010 16:01:44 GMT mulligan [427] * Deliverables/D4.1/ToMatita.ml (modified) Removed interpret.ma from ToMatita Wed, 15 Dec 2010 16:00:01 GMT mulligan [426] * Deliverables/D4.1/Makefile (modified) * Deliverables/D4.1/Test.ml (moved) * Deliverables/D4.1/ToMatita.ml (moved) Changes to ocaml code and makefile. Tue, 14 Dec 2010 15:55:01 GMT mulligan [425] * Deliverables/D4.1/Matita/Assembly.ma (modified) * Deliverables/D4.1/Matita/Map.ma (deleted) Removed Map.ma as no longer needed. Everything else seems to build ... Tue, 14 Dec 2010 15:51:19 GMT mulligan [424] * Deliverables/D4.1/Report/report.tex (modified) Tidied up English in last addition. Tue, 14 Dec 2010 15:49:35 GMT mulligan [423] * Deliverables/D4.1/Report/report.tex (modified) Discussed partiality in the case of assembly: use of Maybe monad. Tue, 14 Dec 2010 15:38:21 GMT mulligan [422] * Deliverables/D4.1/Report/report.tex (modified) Tweaks to the report. Tue, 14 Dec 2010 15:13:55 GMT mulligan [421] * Deliverables/D4.1/Matita/Assembly.ma (modified) Removed duplicate "assembly1" function. Removed Ocaml code from file.