source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2861   8 years mckinna PROVISIONAL commit: Unintentional list reversal cause final step of …
(edit) @2860   8 years sacerdot RTL printing, core dumps ATM
(edit) @2859   8 years sacerdot Pretty printing improved (now it always starts the visit from lbl 1).
(edit) @2858   8 years sacerdot Trying to pretty print the code graph in visit order. Slightly bugged …
(edit) @2857   8 years garnier CL to CM: some invariants strengthened.
(edit) @2856   8 years sacerdot Pretty printing of LTL almost finished.
(edit) @2855   8 years piccolo little bug fixed in TranslateUtils?.
(edit) @2854   8 years sacerdot Pretty printing of the LTL program.
(edit) @2853   8 years sacerdot Pretty printing of line/label numbers.
(edit) @2852   8 years mckinna Interim commit to re-establish well-typedness after all the recent …
(edit) @2851   8 years piccolo partial commit
(edit) @2850   8 years garnier Progress on CL to CM. Some more cases closed modulo some critical …
(edit) @2849   8 years piccolo partial commit
(edit) @2848   8 years sacerdot The pretty printer for LTL.
(edit) @2847   8 years sacerdot …
(edit) @2846   8 years sacerdot Pretty printing of joint programs.
(edit) @2845   8 years piccolo ERTLptr to LTL correctness proof started
(edit) @2844   8 years piccolo Stupid bug fixed
(edit) @2843   8 years piccolo 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
(edit) @2842   8 years sacerdot The compiler can now show all back-end traces too (assembly and object …
(edit) @2841   8 years sacerdot The compiler now computes also the stack cost for every intermediate …
(edit) @2840   8 years campbell Remove irrelevant stuff from RTLabs_partial_traces
(edit) @2839   8 years campbell Basic structure of RTLabs measurable to structured traces results.
(edit) @2838   8 years garnier Closing some more cases
(edit) @2837   8 years tranquil * filled in evaluation of LTL/LIN's extended instrucitons
(edit) @2836   8 years sacerdot …
(edit) @2835   8 years sacerdot Included Uses.ma which is required by the untrusted code. The …
(edit) @2834   8 years sacerdot Execution integrated in the compiler, as it was in the prototype. …
(edit) @2833   8 years sacerdot …
(edit) @2832   8 years sacerdot Added abstraction in front of cases daemon for code extraction.
(edit) @2831   8 years sacerdot …
(edit) @2830   8 years sacerdot Added abstractions in front of cases daemon for code extraction.
(edit) @2829   8 years sacerdot Semantics files committed.
(edit) @2828   8 years sacerdot 1. New semantics.ma file that puts together all semantics. It …
(edit) @2827   8 years sacerdot Everything extracted again.
(edit) @2826   8 years sacerdot New error messages.
(edit) @2825   8 years garnier Progress, Clight to Cminor
(edit) @2824   8 years tranquil * moved sum on lists notation to extranat * used sum on lists to …
(edit) @2823   8 years tranquil * corrected bug in ERTL semantics (both delframe and newframe did the …
(edit) @2822   8 years garnier A consitent proof state for Clight to Cminor, with some progress (and …
(edit) @2821   8 years tranquil * implemented preclassified system for joint (in joint/joint_fullexec.ma)
(edit) @2820   8 years sacerdot Proof obligation closed.
(edit) @2819   8 years sacerdot Proof obligation closed.
(edit) @2818   8 years sacerdot "Repaired", using non computational daemons.
(edit) @2817   8 years sacerdot Repaired after Paolo's commit.
(edit) @2816   8 years sacerdot Repaired after Paolo's commit.
(edit) @2815   8 years sacerdot exec superseded by exec_all
(edit) @2814   8 years sacerdot frontend superseded by execute_all
(edit) @2813   8 years sacerdot RTLabs now printed too
(edit) @2812   8 years sacerdot Pre-classified system for RTLabs.
(edit) @2811   8 years sacerdot Pre-classified system for RTLabs.
(edit) @2810   8 years sacerdot Cminor semantics exported.
(edit) @2809   8 years sacerdot …
(edit) @2808   8 years tranquil added local_stacksize to joint internal functions to accomodate for …
(edit) @2807   8 years mckinna Yet another ErrorMessage? Removed corresponding axiom in …
(edit) @2806   8 years tranquil new b_graph_translate obligations
(edit) @2805   8 years sacerdot Now also prints the trace for the labelled Clight.
(edit) @2804   8 years sacerdot New executable exec_all. It contains a function to run and print all …
(edit) @2803   8 years sacerdot More code extracted, used to debug the compiler.
(edit) @2802   8 years sacerdot New file Clight_classified_system with the classified system for …
(edit) @2801   8 years piccolo Partial commit not yet finished
(edit) @2800   8 years campbell Tidy up Measurable.ma a little, get rid of obsolete comments.
(edit) @2799   8 years tranquil * added taaf_to_taa, conversion from trace_any_any_free to …
(edit) @2798   8 years sacerdot New error message.
(edit) @2797   8 years sacerdot Extracted again after James's cleanup and the implementation of the …
(edit) @2796   8 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2795   8 years sacerdot Added new function Measurable.observe_all_in_measurable to be used to …
(edit) @2794   8 years mckinna Minor tweaks/tidying up
(edit) @2793   8 years campbell Oops, gave fields wrong order during initialisation.
(edit) @2792   8 years campbell Make instrumented output a little easier to read.
(edit) @2791   8 years campbell Remove dead code in driver.
(edit) @2790   8 years campbell Some null handling in conversion from CIL.
(edit) @2789   8 years campbell Some changes to the driver to aid debugging.
(edit) @2788   8 years campbell Report compiler error
(edit) @2787   8 years campbell Output stack costs in driver.
(edit) @2786   8 years piccolo Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
(edit) @2785   8 years piccolo Traces.ma repaired
(edit) @2784   8 years sacerdot Repaired after Mauro's commit.
(edit) @2783   8 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2782   8 years sacerdot 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
(edit) @2781   8 years sacerdot One more computational daemon closed.
(edit) @2780   8 years sacerdot Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
(edit) @2779   8 years sacerdot 1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
(edit) @2778   8 years sacerdot Code to pretty-print the IntelHex? output. At the moment the glue code …
(edit) @2777   8 years sacerdot One computational daemon closed.
(edit) @2776   8 years sacerdot The compiler now extracts also the stack cost model.
(edit) @2775   8 years sacerdot The compiler now computes also the stack cost model.
(edit) @2774   8 years sacerdot 1. the compiler now outputs both the stack cost model and the max …
(edit) @2773   8 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
(edit) @2772   8 years sacerdot Useless code removed.
(edit) @2771   8 years sacerdot Some speed up in Policy.ma.
(edit) @2770   8 years mckinna WARNING: another big commit, touching many files in ASM/*.ma This …
(edit) @2769   8 years mckinna Mistakenly commented out both as_cost_get_label (needed; OK) as well …
(edit) @2768   8 years mckinna Nightmare: file no longer typechecks, because defn as_cost_get_labels …
(edit) @2767   8 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
(edit) @2766   8 years mckinna pruned redundant dependency on Clight/Cexec?.ma
(edit) @2765   8 years sacerdot 1. correctness.ma repaired 2. we used the OC_preclassified_system to …
(edit) @2764   8 years sacerdot preclassified_system for object code
(edit) @2763   8 years sacerdot All daemons in compiler.ma closed (i.e. proof obligations added to the …
(edit) @2762   8 years sacerdot All repaired up to compiler.ma. Note: one daemon is left for one …
Note: See TracRevisionLog for help on using the revision log.