# # ChangeLog for Deliverables/D5.1 # # Generated by Trac 1.2 # Jan 25, 2021, 6:31:40 PM Mon, 08 Apr 2013 11:17:55 GMT regisgia [3107] * Deliverables/D5.1/external-tools (added) * Deliverables/D5.1/external-tools/README (added) * Deliverables/D5.1/external-tools/frama-c (added) * Deliverables/D5.1/external-tools/frama-c/frama-c-Nitrogen-20111001.tar.gz (added) * Deliverables/D5.1/external-tools/jessie (added) * Deliverables/D5.1/external-tools/jessie/README (added) * Deliverables/D5.1/external-tools/jessie/why2.bz2 (added) * Deliverables/D5.1/external-tools/why3 (added) * Deliverables/D5.1/external-tools/why3/README (added) * Deliverables/D5.1/external-tools/why3/why3.bz2 (added) * External tools to compile the plugin. Thu, 28 Feb 2013 13:12:13 GMT regisgia [2749] * Deliverables/D5.1/frama-c-cost-plugin (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/distributed_files (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/frama-c_jessie (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/arith.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/arithSig.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/cerco.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/completeMap.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/compute.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/cost.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/cost_value.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/emap.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/eset.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/misc.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/blowfish.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/blowfish.h (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/bubble_sort.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/des.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/rnd.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/safer.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/saferk64.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/fail/seal.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/3-way.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/LFSR.C (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/LFSR2.C (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/a5.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/fact.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/is_sorted.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/mmb.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/random.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/plugin/tests/success/tab_sum.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/_tags (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/error.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/error.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/main.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/misc.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/misc.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/options.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/options.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/optionsParsing.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/position.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/position.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/tests (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/tests/parity (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/tests/parity/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/tests/parity/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Carbon/wrapper/tests/parity/parity.lus (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/Makefile.in (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/configure.ac (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/distributed_files (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/frama-c_jessie.in (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/arith.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/arithSig.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/cerco.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/completeMap.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/compute.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/compute_simple.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/compute_simple_stack_size.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/cost.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/cost_value.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/emap.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/eset.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/misc.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/multiset.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/normAtLabels.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/normAtLabels.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/parameters.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/simplify_terms.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/blowfish.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/blowfish.h (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/bubble_sort.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/des.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/rnd.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/safer.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/saferk64.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/fail/seal.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/3-way-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/3-way.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR2.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR_char-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/LFSR_char.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/a5-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/a5-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/a5.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/add_pragma.sh (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/binary_search.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/binary_search_char-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/binary_search_char.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/blowfish-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/bubble_sort-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/bubble_sort-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/convert_lemma_axiom.sh (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/des-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/fact-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/fact-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/fact.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/is_sorted-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/is_sorted-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/is_sorted.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/matrix_sum-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/matrix_sum-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/mmb-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/mmb.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/mmb_char-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/mmb_char.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/random-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/random-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/random.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/reverse_list-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/reverse_list-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/reverse_list.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/rnd-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/rnd-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/safer-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/saferk64-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/seal-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/tab_sum-acc-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/tab_sum-acc.mips-instrumented.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/plugin/tests/success/tab_sum.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/Makefile.in (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/_tags (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/error.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/error.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/main.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/misc.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/misc.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/options.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/options.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/optionsParsing.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/position.ml (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/position.mli (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/fail (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/fail/jessie_fail.c (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/parity (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/parity/Makefile (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/parity/README (added) * Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/wrapper/tests/parity/parity.lus (added) * Updated version of the Frama-C plugin. Thu, 28 Feb 2013 13:12:07 GMT regisgia [2748] * Deliverables/D5.1/cost-plug-in/Makefile (deleted) * Deliverables/D5.1/cost-plug-in/README (deleted) * Deliverables/D5.1/cost-plug-in/distributed_files (deleted) * Deliverables/D5.1/cost-plug-in/plugin/Makefile (deleted) * Deliverables/D5.1/cost-plug-in/plugin/README (deleted) * Deliverables/D5.1/cost-plug-in/plugin/cerco.ml (deleted) * Deliverables/D5.1/cost-plug-in/plugin/compute.ml (deleted) * Deliverables/D5.1/cost-plug-in/plugin/cost.ml (deleted) * Deliverables/D5.1/cost-plug-in/plugin/cost_value.ml (deleted) * Deliverables/D5.1/cost-plug-in/plugin/help/mailinglisthelp (deleted) * Deliverables/D5.1/cost-plug-in/plugin/stringTools.ml (deleted) * Deliverables/D5.1/cost-plug-in/plugin/tests/bubble_sort.c (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/Makefile (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/README (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/_tags (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/error.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/error.mli (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/main.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/misc.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/misc.mli (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/options.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/options.mli (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/optionsParsing.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/position.ml (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/position.mli (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/Makefile (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/README (deleted) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/parity.lus (deleted) * Remove the old version of the plugin. Tue, 22 May 2012 06:13:09 GMT amadio [1981] * Deliverables/D5.1/report.pdf (added) update 5.1 Tue, 22 May 2012 06:12:23 GMT amadio [1980] * Deliverables/D5.1/fopara.pdf (deleted) * Deliverables/D5.1/plugin.pdf (deleted) * Deliverables/D5.1/report.tex (deleted) * Deliverables/D5.1/tlca.pdf (deleted) update 5.1 Thu, 26 Jan 2012 09:04:02 GMT amadio [1661] * Deliverables/D2.1/report.pdf (modified) * Deliverables/D5.1-5.3 (deleted) * Deliverables/D5.1/plugin.pdf (modified) rev Thu, 26 Jan 2012 07:43:27 GMT amadio [1659] * Deliverables/D5.1/report.tex (modified) Wed, 25 Jan 2012 16:40:37 GMT amadio [1657] * Deliverables/D5.1/fopara.pdf (added) * Deliverables/D5.1/plugin.pdf (added) * Deliverables/D5.1/report.tex (added) * Deliverables/D5.1/tlca.pdf (added) preliminary version of D5 Fri, 25 Nov 2011 18:43:39 GMT tranquil [1568] * Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml (modified) * Deliverables/D2.2/8051/src/ASM/I8051.ml (modified) * Deliverables/D2.2/8051/src/ASM/I8051.mli (modified) * Deliverables/D2.2/8051/src/ERTL/ERTL.mli (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml (modified) * Deliverables/D2.2/8051/src/ERTL/build.ml (modified) * Deliverables/D2.2/8051/src/ERTL/liveness.ml (modified) * Deliverables/D2.2/8051/src/ERTL/uses.ml (modified) * Deliverables/D2.2/8051/src/LIN/LIN.mli (modified) * Deliverables/D2.2/8051/src/LIN/LINInterpret.ml (modified) * Deliverables/D2.2/8051/src/LIN/LINPrinter.ml (modified) * Deliverables/D2.2/8051/src/LIN/LINToASM.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTL.mli (modified) * Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml (modified) * Deliverables/D2.2/8051/src/RTL/RTL.mli (modified) * Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml (modified) * Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml (modified) * Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml (modified) * Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli (modified) * Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml (modified) * Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml (modified) * Deliverables/D2.2/8051/src/common/intValue.ml (modified) * Deliverables/D2.2/8051/src/common/intValue.mli (modified) * Deliverables/D2.2/8051/src/common/memory.ml (modified) * Deliverables/D2.2/8051/src/common/value.ml (modified) * Deliverables/D2.2/8051/src/common/value.mli (modified) * Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cost.ml (modified) * Immediates introduced (but not fully used yet in RTLabs to RTL ... Tue, 15 Nov 2011 16:12:58 GMT tranquil [1508] * Deliverables/D5.1/cost-plug-in-indexed-labels-branch (copied) * Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cerco.ml (modified) * Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/compute.ml (modified) * Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cost.ml (modified) * Deliverables/D5.1/cost-plug-in-indexed-labels-branch/plugin/cost_value.ml (modified) branched a version of the plug-in that is compatible with the indexed ... Tue, 25 Oct 2011 14:11:11 GMT ayache [1462] * Deliverables/D2.1/report.log (modified) * Deliverables/D2.1/report.pdf (modified) * Deliverables/D2.2/8051/distributed_files (modified) * Deliverables/D2.2/8051/src/ASM/ASM.mli (modified) * Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml (modified) * Deliverables/D2.2/8051/src/ERTL/ERTL.mli (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml (modified) * Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml (modified) * Deliverables/D2.2/8051/src/ERTL/liveness.ml (modified) * Deliverables/D2.2/8051/src/ERTL/uses.ml (modified) * Deliverables/D2.2/8051/src/LIN/LIN.mli (modified) * Deliverables/D2.2/8051/src/LIN/LINInterpret.ml (modified) * Deliverables/D2.2/8051/src/LIN/LINPrinter.ml (modified) * Deliverables/D2.2/8051/src/LIN/LINToASM.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTL.mli (modified) * Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml (modified) * Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml (modified) * Deliverables/D2.2/8051/src/LTL/branch.ml (modified) * Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml (modified) * Deliverables/D2.2/8051/src/acc.ml (modified) * Deliverables/D2.2/8051/src/clight/clightAnnotator.ml (modified) * Deliverables/D2.2/8051/src/clight/clightAnnotator.mli (modified) * Deliverables/D2.2/8051/src/clight/clightParser.ml (modified) * Deliverables/D2.2/8051/src/clight/clightParser.mli (modified) * Deliverables/D2.2/8051/src/clight/clightSwitch.ml (modified) * Deliverables/D2.2/8051/src/clight/clightToCminor.ml (modified) * Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml (modified) * Deliverables/D2.2/8051/src/dev_test.ml (modified) * Deliverables/D2.2/8051/src/languages.ml (modified) * Deliverables/D2.2/8051/src/languages.mli (modified) * Deliverables/D2.2/8051/src/options.ml (modified) * Deliverables/D2.2/8051/src/options.mli (modified) * Deliverables/D2.2/8051/src/utilities/stringSig.mli (modified) * Deliverables/D2.2/8051/src/utilities/stringTools.ml (modified) * Deliverables/D5.1 (added) * Deliverables/D5.1/cost-plug-in (added) * Deliverables/D5.1/cost-plug-in/Makefile (added) * Deliverables/D5.1/cost-plug-in/README (added) * Deliverables/D5.1/cost-plug-in/distributed_files (added) * Deliverables/D5.1/cost-plug-in/plugin (added) * Deliverables/D5.1/cost-plug-in/plugin/Makefile (added) * Deliverables/D5.1/cost-plug-in/plugin/README (added) * Deliverables/D5.1/cost-plug-in/plugin/cerco.ml (added) * Deliverables/D5.1/cost-plug-in/plugin/compute.ml (added) * Deliverables/D5.1/cost-plug-in/plugin/cost.ml (added) * Deliverables/D5.1/cost-plug-in/plugin/cost_value.ml (added) * Deliverables/D5.1/cost-plug-in/plugin/help (added) * Deliverables/D5.1/cost-plug-in/plugin/help/mailinglisthelp (added) * Deliverables/D5.1/cost-plug-in/plugin/stringTools.ml (added) * Deliverables/D5.1/cost-plug-in/plugin/tests (added) * Deliverables/D5.1/cost-plug-in/plugin/tests/bubble_sort.c (added) * Deliverables/D5.1/cost-plug-in/wrapper (added) * Deliverables/D5.1/cost-plug-in/wrapper/Makefile (added) * Deliverables/D5.1/cost-plug-in/wrapper/README (added) * Deliverables/D5.1/cost-plug-in/wrapper/_tags (added) * Deliverables/D5.1/cost-plug-in/wrapper/error.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/error.mli (added) * Deliverables/D5.1/cost-plug-in/wrapper/main.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/misc.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/misc.mli (added) * Deliverables/D5.1/cost-plug-in/wrapper/options.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/options.mli (added) * Deliverables/D5.1/cost-plug-in/wrapper/optionsParsing.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/position.ml (added) * Deliverables/D5.1/cost-plug-in/wrapper/position.mli (added) * Deliverables/D5.1/cost-plug-in/wrapper/tests (added) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity (added) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/Makefile (added) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/README (added) * Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/parity.lus (added) Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been ...