#
# ChangeLog for C-semantics
#
# Generated by Trac 1.2
# Jan 24, 2021, 8:19:16 AM

Wed, 06 Oct 2010 15:23:44 GMT campbell [160]
	* C-semantics/acc-0.1.spaces.patch (added)

	Patch to acc to parse 8051 memory spaces and output matita terms.


Wed, 06 Oct 2010 14:21:10 GMT campbell [157]
	* C-semantics/8051-Memory/memory.tex (modified)

	Make proposed memory spaces semantics more explicit.


Wed, 06 Oct 2010 14:17:57 GMT campbell [156]
	* C-semantics/AST.ma (modified)
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/Values.ma (modified)
	* C-semantics/test/pdata1.c (added)
	* C-semantics/test/pdata2.c (added)

	pdata support


Wed, 06 Oct 2010 12:20:30 GMT campbell [155]
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Csem.ma (modified)

	More sensible handling of integer types and pointer casts.


Wed, 06 Oct 2010 12:20:27 GMT campbell [154]
	* C-semantics/test/io.c (modified)
	* C-semantics/test/spacecadet.c (added)

	Minor test case changes


Wed, 06 Oct 2010 12:20:25 GMT campbell [153]
	* C-semantics/AST.ma (modified)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/Values.ma (modified)

	Use appropriate memory chunks for 8051 pointers.


Wed, 06 Oct 2010 12:20:22 GMT campbell [152]
	* C-semantics/CexecIO.ma (modified)

	Force whd form for memory during execution


Tue, 05 Oct 2010 11:50:40 GMT campbell [149]
	* C-semantics/8051-Memory/memory.tex (modified)

	Fill in a few details about 8051 extensions.


Fri, 24 Sep 2010 08:31:34 GMT campbell [127]
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Csem.ma (modified)
	* C-semantics/Csyntax.ma (modified)

	Allow the storage of pointers in suitably large integers.


Fri, 24 Sep 2010 08:31:33 GMT campbell [126]
	* C-semantics/Csyntax.ma (modified)

	Put in real pointer sizes.


Fri, 24 Sep 2010 08:31:32 GMT campbell [125]
	* C-semantics/AST.ma (modified)
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Csem.ma (modified)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Globalenvs.ma (modified)
	* C-semantics/IOMonad.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/Values.ma (modified)
	* C-semantics/test/io.c.ma (modified)

	Unify memory space / pointer types.
	Implement global variable ...


Fri, 24 Sep 2010 08:31:32 GMT campbell [124]
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Csem.ma (modified)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Globalenvs.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/Values.ma (modified)
	* C-semantics/test/io2.c.ma (modified)

	Initial work on Clight semantics with 8051 memory spaces.


Tue, 21 Sep 2010 09:49:04 GMT sacerdot [94]
	* C-semantics/8051-Memory/memory.tex (modified)

	Minor comments.


Wed, 15 Sep 2010 17:00:06 GMT campbell [82]
	* C-semantics/8051-Memory (added)
	* C-semantics/8051-Memory/memory.tex (added)

	Start of document about impact of 8051 memory model on C.


Fri, 27 Aug 2010 13:29:51 GMT campbell [25]
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/IOMonad.ma (modified)
	* C-semantics/SmallstepExec.ma (modified)
	* C-semantics/test/transform1.ma (modified)

	Simplify the IO monad a little.


Fri, 27 Aug 2010 11:21:50 GMT campbell [24]
	* C-semantics/AST.ma (modified)
	* C-semantics/CexecIO.ma (modified)
	* C-semantics/Coqlib.ma (modified)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Globalenvs.ma (modified)
	* C-semantics/IOMonad.ma (added)
	* C-semantics/Mem.ma (modified)
	* C-semantics/SmallstepExec.ma (added)
	* C-semantics/test/transform1.ma (added)

	Separate out IOMonad from the rest of the executable semantics. ...


Thu, 19 Aug 2010 10:36:03 GMT campbell [20]
	* C-semantics/Cexec.ma (modified)
	* C-semantics/CexecIO.ma (added)
	* C-semantics/Smallstep.ma (modified)
	* C-semantics/test/io.c (added)
	* C-semantics/test/io.c.ma (added)
	* C-semantics/test/io2.c (added)
	* C-semantics/test/io2.c.ma (added)

	Add resumption monad based version of the executable semantics with ...


Mon, 26 Jul 2010 17:04:30 GMT campbell [17]
	* C-semantics/Cexec.ma (modified)

	Remainder of the statements for the executable semantics (except for ...


Mon, 26 Jul 2010 15:19:31 GMT campbell [16]
	* C-semantics/Cexec.ma (modified)
	* C-semantics/extralib.ma (modified)

	Add rest of the expressions to executable Clight semantics.


Thu, 22 Jul 2010 14:50:06 GMT campbell [15]
	* C-semantics/Integers.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/README (modified)
	* C-semantics/binary/Z.ma (modified)
	* C-semantics/extralib.ma (modified)

	Make some definitions more normalization friendly by a little 'nlet ...


Wed, 21 Jul 2010 13:08:58 GMT campbell [14]
	* C-semantics/Integers.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/README (modified)
	* C-semantics/Values.ma (modified)
	* C-semantics/extralib.ma (modified)

	Make Integers.ma respect bounds again, and reenable the rest of
	Mem.ma.


Mon, 19 Jul 2010 14:30:09 GMT campbell [13]
	* C-semantics/Cexec.ma (modified)
	* C-semantics/Csem.ma (modified)

	Minor syntactic changes.


Wed, 07 Jul 2010 16:46:46 GMT campbell [12]
	* C-semantics/README (modified)
	* C-semantics/test/memorymodel.ma (modified)

	Make memory model tests more readable.
	Update README.


Wed, 07 Jul 2010 10:55:01 GMT campbell [11]
	* C-semantics/Cexec.ma (modified)
	* C-semantics/Maps.ma (modified)
	* C-semantics/compcert-1.7.1-matita.patch (modified)
	* C-semantics/extralib.ma (modified)

	Fill in some axioms to aid executablity.
	Implement global variable ...


Tue, 06 Jul 2010 09:53:23 GMT campbell [10]
	* C-semantics/AST.ma (modified)
	* C-semantics/Cexec.ma (modified)
	* C-semantics/Coqlib.ma (modified)
	* C-semantics/Integers.ma (modified)
	* C-semantics/Maps.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/binary (added)
	* C-semantics/binary/Z.ma (added)
	* C-semantics/binary/positive.ma (added)
	* C-semantics/extralib.ma (modified)

	Add binary arithmetic libraries, use for integers and identifiers ...


Mon, 21 Jun 2010 14:22:09 GMT campbell [9]
	* C-semantics/AST.ma (modified)
	* C-semantics/Cexec.ma (modified)
	* C-semantics/Integers.ma (modified)
	* C-semantics/Mem.ma (modified)
	* C-semantics/README (modified)
	* C-semantics/compcert-1.7.1-matita.patch (added)
	* C-semantics/test/trivial.ma (modified)

	Enough of an executable semantics to execute a not-quite-trivial ...


Tue, 08 Jun 2010 13:25:47 GMT campbell [5]
	* C-semantics/Cexec.ma (modified)
	* C-semantics/README (modified)

	Add a few execution steps and calculation of the initial state to the ...


Wed, 02 Jun 2010 17:11:14 GMT campbell [4]
	* C-semantics/Cexec.ma (added)
	* C-semantics/Csyntax.ma (modified)
	* C-semantics/Errors.ma (modified)
	* C-semantics/Integers.ma (modified)

	Some experimental work on executable Clight semantics.


Thu, 27 May 2010 09:47:32 GMT campbell [3]
	* C-semantics (added)
	* C-semantics/AST.ma (added)
	* C-semantics/Coqlib.ma (added)
	* C-semantics/Csem.ma (added)
	* C-semantics/Csyntax.ma (added)
	* C-semantics/Errors.ma (added)
	* C-semantics/Events.ma (added)
	* C-semantics/Floats.ma (added)
	* C-semantics/Globalenvs.ma (added)
	* C-semantics/Integers.ma (added)
	* C-semantics/Maps.ma (added)
	* C-semantics/Mem.ma (added)
	* C-semantics/README (added)
	* C-semantics/Smallstep.ma (added)
	* C-semantics/Values.ma (added)
	* C-semantics/extralib.ma (added)
	* C-semantics/root (added)
	* C-semantics/test (added)
	* C-semantics/test/memorymodel.ma (added)
	* C-semantics/test/trivial.ma (added)

	Import work-in-progress port of the CompCert C semantics to matita.