# # ChangeLog for src/Clight/test/search.c.ma # # Generated by Trac 1.2 # Mar 7, 2021, 9:54:34 AM Wed, 04 Apr 2012 16:48:26 GMT campbell [1876] * src/Clight/CexecSound.ma (modified) * src/Clight/test/castremoval.test.ma (modified) * src/Clight/test/duff.test.ma (modified) * src/Clight/test/factorial.test.ma (modified) * src/Clight/test/null-op.test.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/test/switcher.test.ma (modified) * src/common/Animation.ma (modified) Update Cexec soundness proof. Change finishes_with predicate to ... Wed, 14 Dec 2011 17:17:53 GMT campbell [1618] * src/Clight/addRuntime.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.test.ma (modified) Minor updates due to recent changes. Tue, 13 Dec 2011 00:34:37 GMT sacerdot [1599] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/JMCoercions.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AssocList.ma (modified) * src/common/Errors.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Mem.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/BEGlobalenvs.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/adt/priority_set_adt.ma (modified) * src/utilities/adt/set_adt.ma (modified) * src/utilities/adt/table_adt.ma (modified) * src/utilities/binary/division.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/pair.ma (deleted) Start of merging of stuff into the standard library of Matita. Wed, 21 Sep 2011 14:25:36 GMT campbell [1238] * src/Clight/test/search.c.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) Update Cminor and RTLabs to fit SmallstepExec changes. Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224] * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IntValue.ma (deleted) Type of programs in common/AST made more dependent. In particular, ... Tue, 30 Aug 2011 10:47:18 GMT campbell [1139] * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/test/insertsort.c.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) Shift init_data out of generic program record so that it only appears ... Thu, 16 Jun 2011 11:32:19 GMT campbell [978] * src/Clight/test/duff.ma (deleted) * src/Clight/test/factorial.c.ma (moved) * src/Clight/test/io.ma (deleted) * src/Clight/test/io2.ma (deleted) * src/Clight/test/search.c.ma (added) * src/Clight/test/switcher.c.ma (moved) Update remaining Clight examples.