Timeline


and

Mar 31, 2013:

10:01 PM Changeset [3047] by campbell
Switch removal and labelling combined.

Mar 30, 2013:

1:11 AM Changeset [3046] by campbell
Main part of combined switch removal and labelling proof.

Mar 29, 2013:

10:15 PM Changeset [3045] by tranquil
fixed what made test3 fail. However it involves a different notion of …
8:16 PM Changeset [3044] by campbell
Start showing combination of switch removal and labelling is OK. Fix …
6:38 PM Changeset [3043] by sacerdot
New major extraction that should have solved all remaining issues. As …
6:27 PM Changeset [3042] by sacerdot
Repaired.
6:18 PM Changeset [3041] by sacerdot
Repaired
5:51 PM Changeset [3040] by tranquil
fixed LINToASM
5:45 PM Changeset [3039] by tranquil
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
5:27 PM Changeset [3038] by sacerdot
Bug fixed: the stack_cost* variables must be declared before the …
5:19 PM Changeset [3037] by tranquil
* ADDRESS joint instruction now has also an offset * corrected call to …
5:12 PM Changeset [3036] by garnier
Fixing some problems, progress, etc
3:21 PM Changeset [3035] by mckinna
Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
2:39 PM Changeset [3034] by sacerdot
Bug fixed: COST instructions are now assembled as NOP to prevent the …
12:53 PM Changeset [3033] by sacerdot
Bug fixed: sign_extension was extending according to the _second_ bit, …
12:51 PM Changeset [3032] by campbell
Remind myself why ms_rel_normal is reasonable.
12:38 PM Changeset [3031] by campbell
Tidy up RTLabs preclassified_system definitions.
12:09 PM Changeset [3030] by campbell
Break up front-end for correctness proof. Use let rec to prevent …
9:47 AM Changeset [3029] by sacerdot
New extraction after DPH/DPL bug fixing.
9:42 AM Changeset [3028] by sacerdot
Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
12:03 AM Changeset [3027] by sacerdot
Another output used by the plug-in.

Mar 28, 2013:

11:58 PM Changeset [3026] by sacerdot
With -a we now produce also the .cerco file required by the plug-in.
11:21 PM Changeset [3025] by sacerdot
1. two syntax errors in instrumented files fixed 2. the compiler now …
10:53 PM Changeset [3024] by sacerdot
Bug fixed: set_flags was ignoring the cy and ov flags.
9:58 PM Changeset [3023] by sacerdot
Typo fixed. It made all GOTOs jump to random positions in the ASM code.
7:49 PM Changeset [3022] by campbell
Make a couple of tests monadic for easier inversion.
7:11 PM Changeset [3021] by campbell
Replace clight_clock_after with a more sensible definition that uses …
5:28 PM Changeset [3020] by sacerdot
- Options not used removed from the help/interface. - More compliance …
5:27 PM Changeset [3019] by sacerdot
New extraction after ERTLptr abortion.
5:27 PM Changeset [3018] by sacerdot
1) some files repaired 2) all stuff related to the aborted pass …
5:05 PM Changeset [3017] by sacerdot
Repaired.
5:04 PM Changeset [3016] by tranquil
fixed after previous commit
4:58 PM Changeset [3015] by sacerdot
Comment removed
4:58 PM Changeset [3014] by tranquil
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
4:56 PM Changeset [3013] by sacerdot
Temporary parsing files removed.
3:51 PM Changeset [3012] by sacerdot
Debugging code removed after bug fixing.
3:47 PM Changeset [3011] by sacerdot
New extraction.
3:46 PM Changeset [3010] by tranquil
same bug as was in liveness is now fixed
3:09 PM Changeset [3009] by sacerdot
New extraction.
3:07 PM Changeset [3008] by tranquil
corrected bug where the address of pointer calls was not defined as used
2:59 PM Changeset [3007] by campbell
Sketch out how Cminor to RTLabs correctness would fit into the …
1:50 PM Changeset [3006] by sacerdot
New extraction, bugs fixed.
1:49 PM Changeset [3005] by sacerdot
Beginning of making it fully compatible with untrusted one.
1:48 PM Changeset [3004] by tranquil
fixed a bug where when doing an asymetrical op, cast initialization …
1:08 PM Changeset [3003] by sacerdot
Correctness.ma "repaired"
1:05 PM Changeset [3002] by tranquil
fixed previous commit
1:02 PM Changeset [3001] by sacerdot
New extraction.
1:01 PM Changeset [3000] by tranquil
added RTLabs printer
12:47 PM Changeset [2999] by sacerdot
code_memory added to labelled_object_code to avoid recomputing it …
12:12 PM Changeset [2998] by sacerdot
Test on conditional execution. Fails atm.
10:27 AM Changeset [2997] by sacerdot
New extraction.
10:22 AM Changeset [2996] by sacerdot
Printing of graphs now starts from the entry point.
10:03 AM Changeset [2995] by sacerdot
The lIN_printer extracted.
10:02 AM Changeset [2994] by sacerdot
The LIN printer.
9:56 AM Changeset [2993] by sacerdot
1. performance improved: the type inference was inferring …
12:07 AM Changeset [2992] by campbell
Add "only one return" invariant to RTLabs functions.

Mar 27, 2013:

9:57 PM Changeset [2991] by piccolo
Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
7:49 PM Changeset [2990] by campbell
Replace dodgy hypothesis by nice ones, clean up a little.
7:00 PM Changeset [2989] by campbell
Make front-end measurability preservation proof cope with moving the …
6:45 PM Changeset [2988] by sacerdot
Some easy tests.
6:32 PM Changeset [2987] by sacerdot
And again.. :(
6:32 PM Changeset [2986] by sacerdot
New extraction.
6:31 PM Changeset [2985] by sacerdot
Order of printing of lines in LIN fixed again, truly this time. But I …
6:17 PM Changeset [2984] by tranquil
better LINToASM initialization of globals (to be tested!)
6:17 PM Changeset [2983] by sacerdot
LIN code was printed in reverse order. But I have not really …
6:05 PM Changeset [2982] by sacerdot
Pretty priting of LIN implemented.
4:53 PM Changeset [2981] by sacerdot
New extraction after code simplification.
4:50 PM Changeset [2980] by tranquil
fixed b_graph_translate
4:34 PM Changeset [2979] by sacerdot
1. LINToASM: new extraction (fix deletion backtracked) 2. …
4:33 PM Changeset [2978] by tranquil
merged accidentally backtracked changes
4:09 PM Changeset [2977] by sacerdot
New extraction after several bug fixes.
4:09 PM Changeset [2976] by tranquil
* a dangling trivial proof obligation is now closed
4:07 PM Changeset [2975] by tranquil
* RTL premain fixed * fixed bug in back end ops (subtracting to a …
4:03 PM Changeset [2974] by sacerdot
New extraction.
1:11 PM Changeset [2973] by tranquil
semanticUtils adapted to changes in TranslateUtils?
11:42 AM Changeset [2972] by campbell
Remove init from a testcase.
11:41 AM Changeset [2971] by campbell
Single RTLabs return statement.

Mar 26, 2013:

7:13 PM Changeset [2970] by tranquil
now joint_if_entry can change when a preamble is added, so code points …
7:09 PM Changeset [2969] by sacerdot
Dead axiom removed :-)
7:07 PM Changeset [2968] by sacerdot
The initial status memory was not really initialized. Now it is.
6:54 PM Changeset [2967] by sacerdot
Semantics changed so that a terminating joint program that returns an …
6:35 PM Changeset [2966] by sacerdot
Modified by hand files (to improve a little bit the performance).
6:35 PM Changeset [2965] by sacerdot
Code performance improved a bit by hand.
6:33 PM Changeset [2964] by sacerdot
Debugging code removed.
6:32 PM Changeset [2963] by sacerdot
Bug fixed: the pre-main for the final code is now COST k1 …
5:36 PM Changeset [2962] by sacerdot
Most performant algorithm restored.
5:02 PM Changeset [2961] by sacerdot
Bug fixed (stupid typo in pre-main code made the compiler diverge on …
4:51 PM Changeset [2960] by sacerdot
New extraction, it diverges in RTL execution now.
4:46 PM Changeset [2959] by sacerdot
Typo
4:45 PM Changeset [2958] by sacerdot
Error message implemented.
4:41 PM Changeset [2957] by tranquil
fixed semantics_blocks
4:31 PM Changeset [2956] by tranquil
fixed LTL/LIN semantics
4:11 PM Changeset [2955] by tranquil
corrected stupid typo
3:52 PM Changeset [2954] by tranquil
resolved circular dependency for ERTLptr's semantics
3:34 PM Changeset [2953] by campbell
Fix silly label handling bug I realised was there during my talk…
2:01 PM Changeset [2952] by tranquil
* corrected all back-end premains to not pass any arguments to the …

Mar 25, 2013:

11:30 PM Changeset [2951] by sacerdot
New extraction. Novely: a pre-main is used in the back-end. …
10:39 PM Changeset [2950] by sacerdot
linearise repaired (did I do the right thing???)
9:48 PM Changeset [2949] by sacerdot
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …

Mar 24, 2013:

9:17 PM Changeset [2948] by campbell
Finish up measurable to structured proof, exposing the prefix and …
9:17 PM Changeset [2947] by campbell
Init change in measurable to structured file.
11:29 AM Changeset [2946] by tranquil
main novelties: * there is an in-built stack_usage nat in joint …

Mar 23, 2013:

8:43 AM Changeset [2945] by campbell
Minor tweak.
2:31 AM Changeset [2944] by sacerdot
Some progress.
2:07 AM Changeset [2943] by sacerdot
Mauro, I have put a daemon in place of the proof obligation that used …
1:37 AM Changeset [2942] by sacerdot
Many changes: 1. Coloured graphs are now specified in terms of …

Mar 22, 2013:

9:46 PM Changeset [2941] by campbell
Update proof slides.
7:16 PM Changeset [2940] by sacerdot
1. StatusSimulationHelper? changed to allow to use status_rel that …
10:11 AM Changeset [2939] by sacerdot
Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
2:11 AM Changeset [2938] by sacerdot
1. proof of "all eliminable are eliminable" completed 2. the notion of …

Mar 21, 2013:

9:45 PM Changeset [2937] by campbell
Speed up checking of RTLabs/CostInj.ma.
9:45 PM Changeset [2936] by campbell
Disable initialisation code generation in Cminor, propogate init data …
9:37 PM Changeset [2935] by tranquil
separation of RTL semantics in three different versions, and …
8:34 PM Changeset [2934] by sacerdot
Patch to obtain more easily comparable traces.
8:11 PM Changeset [2933] by sacerdot
New extraction, several bug fixed. RTL_semantics fixed by hand, will …
7:58 PM Changeset [2932] by sacerdot
Same comment as previous commit on this file: the previous commit was …
7:31 PM Changeset [2931] by sacerdot
Partial back-track from Paolo's commit, that was partial.
7:14 PM Changeset [2930] by sacerdot
More progress. Some useless parameters have been removed from the …
7:13 PM Changeset [2929] by sacerdot
Bug fixed: the coercion mechanism made you think that the CALL case …
6:26 PM Changeset [2928] by tranquil
some sketches about correctness proof
5:17 PM Changeset [2927] by tranquil
stupid bug in bool_of_beval
4:06 PM Changeset [2926] by tranquil
corrected bug in executing Sub
3:39 PM Changeset [2925] by tranquil
corrected bug in toggle_bool
8:39 AM Changeset [2924] by campbell
Make calls to a known identifier actually use a direct call.
8:38 AM Changeset [2923] by campbell
Remove some leftovers.
2:12 AM Changeset [2922] by sacerdot
Progress: proof of "eliminable statements can be eliminated" almost …
12:56 AM Changeset [2921] by sacerdot
Extracted again.
12:53 AM Changeset [2920] by sacerdot
dos2unix-ed

Mar 20, 2013:

7:21 PM Changeset [2919] by fguidi
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
5:10 PM Changeset [2918] by tranquil
erased stupid accidental paste at the start of file (happened when …
1:20 PM Changeset [2917] by tranquil
made it so that a 0 offset does not generate adding ops when accessing …
12:33 PM Changeset [2916] by tranquil
corrected yet another endianness bug in load and store
9:37 AM Changeset [2915] by sacerdot
Dead code removed.
8:39 AM Changeset [2914] by campbell
Use single definition for stack measurement.
12:24 AM Changeset [2913] by sacerdot
Bug corrected by hand. It will be corrected automatically by next …
12:21 AM Changeset [2912] by sacerdot
Ouch, another bug in the very same function. Fixed too, on an example …
12:12 AM Changeset [2911] by sacerdot
Bug fixed in the translation of casts.

Mar 19, 2013:

11:19 PM Changeset [2910] by sacerdot
Abstract statuses for ASM and OC completed. A simple test program can …
10:21 PM Changeset [2909] by sacerdot
New extraction.
8:00 PM Changeset [2908] by sacerdot
Bug fixed by hand, they will be fixed automatically by the new extraction.
7:48 PM Changeset [2907] by sacerdot
1. a few bugs fixed 2. as_return implemented for ASM & OC
9:54 AM Changeset [2906] by sacerdot
Bug fixed.
8:42 AM Changeset [2905] by sacerdot
Semantics of ASM in place (up to return values and function call …
1:27 AM Changeset [2904] by sacerdot
1. Algorithm modified by hand to make it run faster. The trusted …
1:25 AM Changeset [2903] by sacerdot
Extracted again.
1:24 AM Changeset [2902] by sacerdot
Quick hack to allow printing of OC code. It will be automatically …
1:22 AM Changeset [2901] by sacerdot
1. backendPrinter renamed to printer 2. Clight printing branched into …
1:20 AM Changeset [2900] by sacerdot
Flushing to understand where it is slow.
12:33 AM Changeset [2899] by sacerdot
1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …

Mar 18, 2013:

10:03 AM Changeset [2898] by piccolo
1) simplification of cond and seq case for StatusSimulationHelper?

Mar 16, 2013:

9:08 PM Changeset [2897] by campbell
Minor tidying.
9:08 PM Changeset [2896] by campbell
Complete part of measurable to structured subtraces proof that shows …
9:08 PM Changeset [2895] by campbell
Match up function id from RTLabs Callstate with shadow stack, use in …
9:08 PM Changeset [2894] by campbell
Some progress on showing that the change to structured traces …
9:08 PM Changeset [2893] by campbell
Add tlr_unrepeating.
9:08 PM Changeset [2892] by campbell
Add cost hypotheses.
10:42 AM Changeset [2891] by piccolo
added precondition on seq statement and tested correct in the …

Mar 15, 2013:

11:11 PM Changeset [2890] by sacerdot
Exported again, now the execution is correct up to LIN for a simple …
7:36 PM Changeset [2889] by sacerdot
It works very nice!
7:31 PM Changeset [2888] by tranquil
backtracked some partial changes
7:22 PM Changeset [2887] by tranquil
Corrected bug where eliminable statements where not eliminated. …
7:19 PM Changeset [2886] by piccolo
partial commit
7:06 PM Changeset [2885] by sacerdot
Hint at how to change everything.
6:37 PM Changeset [2884] by sacerdot
Debugging print added.
6:33 PM Changeset [2883] by piccolo
partial commit
5:52 PM Changeset [2882] by sacerdot
5:51 PM Changeset [2881] by sacerdot
5:51 PM Changeset [2880] by sacerdot
12:16 PM Changeset [2879] by tranquil
changed coercion from list of joint_seq to blocks to a more efficient one
11:32 AM Changeset [2878] by tranquil
backtracked some changes that were not ready for commit
11:29 AM Changeset [2877] by garnier
Correction of a bug in my former bug correction.
10:58 AM Changeset [2876] by tranquil
corrected another endianess bug in joint_semantics. Switched some …
1:32 AM Changeset [2875] by sacerdot
Pretty printing of object code integrated too. A couple of axioms make …

Mar 14, 2013:

10:46 PM Changeset [2874] by sacerdot
Syntax fixed: ./cerco [-exec] filename annotationoption
10:37 PM Changeset [2873] by sacerdot
Extracted again.
7:26 PM Changeset [2872] by tassi
Fix list of distributed files so that the debian package can be built
5:34 PM Changeset [2871] by tranquil
op2 evaluation on beval's rendered oblivious to carry bit when …
4:26 PM Changeset [2870] by sacerdot
Proof fixed.
3:40 PM Changeset [2869] by tranquil
some reorganization of definitions, and a new taaf_append_taaf
12:04 AM Changeset [2868] by sacerdot
Pretty printing of ERTL and ERTLptr code.

Mar 13, 2013:

11:12 PM Changeset [2867] by sacerdot
New extraction after indianess bug fixes by Paolo.
4:21 PM Changeset [2866] by tranquil
corrected two bugs of the translation: constant translation used wrong …
2:38 PM Changeset [2865] by sacerdot
2:27 PM Changeset [2864] by sacerdot
I must have drunk yesterday: all RTL passes are printed correctly; the …
2:22 PM Changeset [2863] by piccolo
Added new invariant to good_if Generalized version of cond case for …
2:07 PM Changeset [2862] by sacerdot
Repaired, a reverse was enough.
1:15 PM Changeset [2861] by mckinna
PROVISIONAL commit: Unintentional list reversal cause final step of …
2:02 AM Changeset [2860] by sacerdot
RTL printing, core dumps ATM
1:19 AM Changeset [2859] by sacerdot
Pretty printing improved (now it always starts the visit from lbl 1).
12:52 AM Changeset [2858] by sacerdot
Trying to pretty print the code graph in visit order. Slightly bugged …

Mar 12, 2013:

8:03 PM Changeset [2857] by garnier
CL to CM: some invariants strengthened.
7:11 PM Changeset [2856] by sacerdot
Pretty printing of LTL almost finished.
6:51 PM Changeset [2855] by piccolo
little bug fixed in TranslateUtils?.
5:53 PM Changeset [2854] by sacerdot
Pretty printing of the LTL program.
5:53 PM Changeset [2853] by sacerdot
Pretty printing of line/label numbers.
4:37 PM Changeset [2852] by mckinna
Interim commit to re-establish well-typedness after all the recent …
4:13 PM Changeset [2851] by piccolo
partial commit
3:54 PM Changeset [2850] by garnier
Progress on CL to CM. Some more cases closed modulo some critical …
1:41 PM Changeset [2849] by piccolo
partial commit
10:56 AM Changeset [2848] by sacerdot
The pretty printer for LTL.
10:20 AM Changeset [2847] by sacerdot
2:28 AM Changeset [2846] by sacerdot
Pretty printing of joint programs.

Mar 11, 2013:

6:50 PM Changeset [2845] by piccolo
ERTLptr to LTL correctness proof started
1:28 PM Changeset [2844] by piccolo
Stupid bug fixed
1:02 PM Changeset [2843] by piccolo
1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
12:41 PM Changeset [2842] by sacerdot
The compiler can now show all back-end traces too (assembly and object …
12:40 PM Changeset [2841] by sacerdot
The compiler now computes also the stack cost for every intermediate …
12:18 PM Changeset [2840] by campbell
Remove irrelevant stuff from RTLabs_partial_traces
12:18 PM Changeset [2839] by campbell
Basic structure of RTLabs measurable to structured traces results.

Mar 10, 2013:

1:21 PM Changeset [2838] by garnier
Closing some more cases

Mar 9, 2013:

12:19 PM Changeset [2837] by tranquil
* filled in evaluation of LTL/LIN's extended instrucitons

Mar 8, 2013:

11:55 PM Changeset [2836] by sacerdot
11:54 PM Changeset [2835] by sacerdot
Included Uses.ma which is required by the untrusted code. The …
11:45 PM Changeset [2834] by sacerdot
Execution integrated in the compiler, as it was in the prototype. …
11:40 PM Changeset [2833] by sacerdot
11:40 PM Changeset [2832] by sacerdot
Added abstraction in front of cases daemon for code extraction.
11:38 PM Changeset [2831] by sacerdot
11:37 PM Changeset [2830] by sacerdot
Added abstractions in front of cases daemon for code extraction.
11:18 PM Changeset [2829] by sacerdot
Semantics files committed.
11:17 PM Changeset [2828] by sacerdot
1. New semantics.ma file that puts together all semantics. It …
9:07 PM Changeset [2827] by sacerdot
Everything extracted again.
9:07 PM Changeset [2826] by sacerdot
New error messages.
8:36 PM Changeset [2825] by garnier
Progress, Clight to Cminor
5:37 PM Changeset [2824] by tranquil
* moved sum on lists notation to extranat * used sum on lists to …
3:51 PM Changeset [2823] by tranquil
* corrected bug in ERTL semantics (both delframe and newframe did the …
12:48 PM Changeset [2822] by garnier
A consitent proof state for Clight to Cminor, with some progress (and …
11:44 AM Changeset [2821] by tranquil
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
12:26 AM Changeset [2820] by sacerdot
Proof obligation closed.
12:14 AM Changeset [2819] by sacerdot
Proof obligation closed.

Mar 7, 2013:

11:43 PM Changeset [2818] by sacerdot
"Repaired", using non computational daemons.
10:31 PM Changeset [2817] by sacerdot
Repaired after Paolo's commit.
10:20 PM Changeset [2816] by sacerdot
Repaired after Paolo's commit.
9:41 PM Changeset [2815] by sacerdot
exec superseded by exec_all
9:39 PM Changeset [2814] by sacerdot
frontend superseded by execute_all
9:34 PM Changeset [2813] by sacerdot
RTLabs now printed too
9:23 PM Changeset [2812] by sacerdot
Pre-classified system for RTLabs.
9:22 PM Changeset [2811] by sacerdot
Pre-classified system for RTLabs.
6:36 PM Changeset [2810] by sacerdot
Cminor semantics exported.
6:33 PM Changeset [2809] by sacerdot
6:03 PM Changeset [2808] by tranquil
added local_stacksize to joint internal functions to accomodate for …
5:43 PM Changeset [2807] by mckinna
Yet another ErrorMessage? Removed corresponding axiom in …
2:51 PM Changeset [2806] by tranquil
new b_graph_translate obligations
2:01 PM Changeset [2805] by sacerdot
Now also prints the trace for the labelled Clight.
1:55 PM Changeset [2804] by sacerdot
New executable exec_all. It contains a function to run and print all …
1:54 PM Changeset [2803] by sacerdot
More code extracted, used to debug the compiler.
1:53 PM Changeset [2802] by sacerdot
New file Clight_classified_system with the classified system for …
1:29 PM Changeset [2801] by piccolo
Partial commit not yet finished
1:07 PM Changeset [2800] by campbell
Tidy up Measurable.ma a little, get rid of obsolete comments.
1:04 PM Changeset [2799] by tranquil
* added taaf_to_taa, conversion from trace_any_any_free to …
12:56 PM Changeset [2798] by sacerdot
New error message.
12:55 PM Changeset [2797] by sacerdot
Extracted again after James's cleanup and the implementation of the …
12:10 PM Changeset [2796] by tranquil
* added global notation for existence in Type[1] (\exists[1] x.P) * in …
9:31 AM Changeset [2795] by sacerdot
Added new function Measurable.observe_all_in_measurable to be used to …
7:47 AM Changeset [2794] by mckinna
Minor tweaks/tidying up

Mar 6, 2013:

7:23 PM Changeset [2793] by campbell
Oops, gave fields wrong order during initialisation.
4:50 PM Changeset [2792] by campbell
Make instrumented output a little easier to read.
4:50 PM Changeset [2791] by campbell
Remove dead code in driver.
3:48 PM Changeset [2790] by campbell
Some null handling in conversion from CIL.
3:48 PM Changeset [2789] by campbell
Some changes to the driver to aid debugging.
3:48 PM Changeset [2788] by campbell
Report compiler error
3:48 PM Changeset [2787] by campbell
Output stack costs in driver.
2:59 PM Changeset [2786] by piccolo
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
2:58 PM Changeset [2785] by piccolo
Traces.ma repaired
2:35 PM Changeset [2784] by sacerdot
Repaired after Mauro's commit.
12:09 PM Changeset [2783] by piccolo
modified joint_closed_internal_function definition (added condition on …
3:03 AM Changeset [2782] by sacerdot
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
3:00 AM Changeset [2781] by sacerdot
One more computational daemon closed.
2:59 AM Changeset [2780] by sacerdot
Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …

Mar 5, 2013:

11:50 PM Changeset [2779] by sacerdot
1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
11:34 PM Changeset [2778] by sacerdot
Code to pretty-print the IntelHex? output. At the moment the glue code …
10:03 PM Changeset [2777] by sacerdot
One computational daemon closed.
9:53 PM Changeset [2776] by sacerdot
The compiler now extracts also the stack cost model.
9:52 PM Changeset [2775] by sacerdot
The compiler now computes also the stack cost model.
6:15 PM Changeset [2774] by sacerdot
1. the compiler now outputs both the stack cost model and the max …

Mar 4, 2013:

10:03 AM Changeset [2773] by sacerdot
1. everything extracted again after all bugs in Matita's extraction …
9:55 AM Changeset [2772] by sacerdot
Useless code removed.

Mar 3, 2013:

11:46 PM Changeset [2771] by sacerdot
Some speed up in Policy.ma.
9:58 PM Changeset [2770] by mckinna
WARNING: another big commit, touching many files in ASM/*.ma This …
2:59 PM Changeset [2769] by mckinna
Mistakenly commented out both as_cost_get_label (needed; OK) as well …
2:44 PM Changeset [2768] by mckinna
Nightmare: file no longer typechecks, because defn as_cost_get_labels …
2:03 PM Changeset [2767] by mckinna
WARNING: BIG commit, which pushes code_size_opt check into …
10:39 AM Changeset [2766] by mckinna
pruned redundant dependency on Clight/Cexec?.ma
12:23 AM Changeset [2765] by sacerdot
1. correctness.ma repaired 2. we used the OC_preclassified_system to …

Mar 2, 2013:

11:59 PM Changeset [2764] by sacerdot
preclassified_system for object code
11:42 AM Changeset [2763] by sacerdot
All daemons in compiler.ma closed (i.e. proof obligations added to the …
2:37 AM Changeset [2762] by sacerdot
All repaired up to compiler.ma. Note: one daemon is left for one …
1:50 AM Changeset [2761] by sacerdot
Unused (but not useless) code commented out.
1:29 AM Changeset [2760] by sacerdot
1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …

Mar 1, 2013:

7:56 PM Changeset [2759] by campbell
Print out costs, with choice of style. Note small anti-assertion patch …
7:55 PM Changeset [2758] by campbell
Adapt prototype's Clight printer. Doesn't use cost map yet.
7:13 PM Changeset [2757] by tranquil
many things are still broken, but there is a partial backtrack on …
1:05 PM Changeset [2756] by sacerdot
WARNING: this commit breaks things, sorry, Paolo is going to fix …
11:06 AM Changeset [2755] by tranquil
* changed primitives of abstract status (with stuf that is probably …
10:26 AM Changeset [2754] by sacerdot
1. WARNING: I commented out one of James's function used in …
Note: See TracTimeline for information about the timeline view.