# # ChangeLog for C-semantics/test # # Generated by Trac 1.2 # Mar 4, 2021, 1:35:48 PM 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:27 GMT campbell [154] * C-semantics/test/io.c (modified) * C-semantics/test/spacecadet.c (added) Minor test case changes 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. 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 ... 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. 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 ... 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.