# # ChangeLog for Deliverables/D3.1 # # Generated by Trac 1.2 # Jan 26, 2021, 11:45:07 PM Wed, 16 Feb 2011 15:25:02 GMT campbell [535] * Deliverables/D3.1/C-semantics/Integers.ma (modified) * Deliverables/D3.1/C-semantics/Smallstep.ma (modified) * Deliverables/D3.1/C-semantics/cerco/BitVector.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Util.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Vector.ma (modified) * Deliverables/D3.1/C-semantics/extralib.ma (modified) Minimal integration of bitvectors into Clight semantics - does a ... Wed, 16 Feb 2011 15:25:01 GMT campbell [534] * Deliverables/D3.1/C-semantics/cerco/Util.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Vector.ma (modified) Fix a couple of bugs with branched 4.1 stuff. Wed, 16 Feb 2011 15:25:00 GMT campbell [533] * Deliverables/D3.1/C-semantics/cerco/Arithmetic.ma (modified) * Deliverables/D3.1/C-semantics/cerco/BitVectorTrie.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Char.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Util.ma (modified) * Deliverables/D3.1/C-semantics/cerco/Vector.ma (modified) Make stuff from D4.1 work with my copy of matita. Wed, 16 Feb 2011 14:27:39 GMT campbell [531] * Deliverables/D3.1/C-semantics/cerco (copied) Create temporary branch of D4.1 matita development to help integrate ... 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 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. 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. 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 ... 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 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. 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. Mon, 13 Dec 2010 17:48:38 GMT campbell [417] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Minor typo. Mon, 13 Dec 2010 17:38:40 GMT campbell [416] * Deliverables/D3.1/C-semantics/acc-0.1.spaces.patch (modified) Fix printing of switch statements as matita terms. Mon, 13 Dec 2010 17:35:05 GMT campbell [415] * Deliverables/D3.1/C-semantics/test/duff.c (added) * Deliverables/D3.1/C-semantics/test/duff.ma (added) * Deliverables/D3.1/C-semantics/test/factorial.c (added) * Deliverables/D3.1/C-semantics/test/factorial.ma (added) A couple of amusing examples. Mon, 13 Dec 2010 16:52:19 GMT campbell [413] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Add example of executing C semantics. Mon, 13 Dec 2010 16:52:18 GMT campbell [412] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Add example of animation. Mon, 13 Dec 2010 16:11:00 GMT campbell [411] * Deliverables/D3.1/C-semantics/IOMonad.ma (modified) Note associativity of IOMonad, subject to extensionality. Mon, 13 Dec 2010 14:58:29 GMT campbell [409] * Deliverables/D3.1/C-semantics/Animation.ma (added) * Deliverables/D3.1/C-semantics/depends (modified) * Deliverables/D3.1/C-semantics/test/memorymodel.ma (modified) * Deliverables/D3.1/C-semantics/test/trivial.ma (modified) Update a couple of examples; put support for animation in its own file. Mon, 13 Dec 2010 12:04:14 GMT campbell [408] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Add missing diagram. Mon, 13 Dec 2010 11:43:12 GMT campbell [407] * Deliverables/D3.1/Report/report.tex (modified) Mention version of compcert used. Mon, 13 Dec 2010 11:12:50 GMT campbell [406] * Deliverables/D3.1/8051-Memory (moved) Move description of 8051 memory model out of C semantics. Mon, 13 Dec 2010 10:47:21 GMT campbell [405] * Deliverables/D3.1/C-semantics (moved) Move C semantics to the appropriate deliverable directory. Sun, 12 Dec 2010 23:02:29 GMT campbell [402] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Revise D3.1, add notes on files. Wed, 08 Dec 2010 17:08:05 GMT campbell [393] * C-semantics/CexecIOcomplete.ma (modified) * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) A few more details in D3.1. Mon, 06 Dec 2010 16:17:40 GMT campbell [381] * Deliverables/D3.1/Report/report.bib (modified) * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Some d3.1 work. Mon, 29 Nov 2010 17:42:10 GMT campbell [335] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Quick pass through 3.1 text. Wed, 27 Oct 2010 14:27:28 GMT campbell [207] * Deliverables/D3.1/Report/report.pdf (modified) * Deliverables/D3.1/Report/report.tex (modified) Add memory extensions and rework parts of D3.1. Tue, 19 Oct 2010 11:42:08 GMT campbell [197] * Deliverables/D3.1 (added) * Deliverables/D3.1/Report (added) * Deliverables/D3.1/Report/report.bib (added) * Deliverables/D3.1/Report/report.pdf (added) * Deliverables/D3.1/Report/report.tex (added) Add some first draft text for 3.1.