Timeline
Mar 28, 2013:
- 11:58 PM Changeset [3026] by
- With -a we now produce also the .cerco file required by the plug-in.
- 11:21 PM Changeset [3025] by
- 1. two syntax errors in instrumented files fixed 2. the compiler now …
- 10:53 PM Changeset [3024] by
- Bug fixed: set_flags was ignoring the cy and ov flags.
- 9:58 PM Changeset [3023] by
- Typo fixed. It made all GOTOs jump to random positions in the ASM code.
- 7:49 PM Changeset [3022] by
- Make a couple of tests monadic for easier inversion.
- 7:11 PM Changeset [3021] by
- Replace clight_clock_after with a more sensible definition that uses …
- 5:28 PM Changeset [3020] by
- - Options not used removed from the help/interface. - More compliance …
- 5:27 PM Changeset [3019] by
- New extraction after ERTLptr abortion.
- 5:27 PM Changeset [3018] by
- 1) some files repaired 2) all stuff related to the aborted pass …
- 5:05 PM Changeset [3017] by
- Repaired.
- 5:04 PM Changeset [3016] by
- fixed after previous commit
- 4:58 PM Changeset [3015] by
- Comment removed
- 4:58 PM Changeset [3014] by
- ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
- 4:56 PM Changeset [3013] by
- Temporary parsing files removed.
- 3:51 PM Changeset [3012] by
- Debugging code removed after bug fixing.
- 3:47 PM Changeset [3011] by
- New extraction.
- 3:46 PM Changeset [3010] by
- same bug as was in liveness is now fixed
- 3:09 PM Changeset [3009] by
- New extraction.
- 3:07 PM Changeset [3008] by
- corrected bug where the address of pointer calls was not defined as used
- 2:59 PM Changeset [3007] by
- Sketch out how Cminor to RTLabs correctness would fit into the …
- 1:50 PM Changeset [3006] by
- New extraction, bugs fixed.
- 1:49 PM Changeset [3005] by
- Beginning of making it fully compatible with untrusted one.
- 1:48 PM Changeset [3004] by
- fixed a bug where when doing an asymetrical op, cast initialization …
- 1:08 PM Changeset [3003] by
- Correctness.ma "repaired"
- 1:05 PM Changeset [3002] by
- fixed previous commit
- 1:02 PM Changeset [3001] by
- New extraction.
- 1:01 PM Changeset [3000] by
- added RTLabs printer
- 12:47 PM Changeset [2999] by
- code_memory added to labelled_object_code to avoid recomputing it …
- 12:12 PM Changeset [2998] by
- Test on conditional execution. Fails atm.
- 10:27 AM Changeset [2997] by
- New extraction.
- 10:22 AM Changeset [2996] by
- Printing of graphs now starts from the entry point.
- 10:03 AM Changeset [2995] by
- The lIN_printer extracted.
- 10:02 AM Changeset [2994] by
- The LIN printer.
- 9:56 AM Changeset [2993] by
- 1. performance improved: the type inference was inferring …
- 12:07 AM Changeset [2992] by
- Add "only one return" invariant to RTLabs functions.
Mar 27, 2013:
- 9:57 PM Changeset [2991] by
- Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
- 7:49 PM Changeset [2990] by
- Replace dodgy hypothesis by nice ones, clean up a little.
- 7:00 PM Changeset [2989] by
- Make front-end measurability preservation proof cope with moving the …
- 6:45 PM Changeset [2988] by
- Some easy tests.
- 6:32 PM Changeset [2987] by
- And again.. :(
- 6:32 PM Changeset [2986] by
- New extraction.
- 6:31 PM Changeset [2985] by
- Order of printing of lines in LIN fixed again, truly this time. But I …
- 6:17 PM Changeset [2984] by
- better LINToASM initialization of globals (to be tested!)
- 6:17 PM Changeset [2983] by
- LIN code was printed in reverse order. But I have not really …
- 6:05 PM Changeset [2982] by
- Pretty priting of LIN implemented.
- 4:53 PM Changeset [2981] by
- New extraction after code simplification.
- 4:50 PM Changeset [2980] by
- fixed b_graph_translate
- 4:34 PM Changeset [2979] by
- 1. LINToASM: new extraction (fix deletion backtracked) 2. …
- 4:33 PM Changeset [2978] by
- merged accidentally backtracked changes
- 4:09 PM Changeset [2977] by
- New extraction after several bug fixes.
- 4:09 PM Changeset [2976] by
- * a dangling trivial proof obligation is now closed
- 4:07 PM Changeset [2975] by
- * RTL premain fixed * fixed bug in back end ops (subtracting to a …
- 4:03 PM Changeset [2974] by
- New extraction.
- 1:11 PM Changeset [2973] by
- semanticUtils adapted to changes in TranslateUtils?
- 11:42 AM Changeset [2972] by
- Remove init from a testcase.
- 11:41 AM Changeset [2971] by
- Single RTLabs return statement.
Mar 26, 2013:
- 7:13 PM Changeset [2970] by
- now joint_if_entry can change when a preamble is added, so code points …
- 7:09 PM Changeset [2969] by
- Dead axiom removed :-)
- 7:07 PM Changeset [2968] by
- The initial status memory was not really initialized. Now it is.
- 6:54 PM Changeset [2967] by
- Semantics changed so that a terminating joint program that returns an …
- 6:35 PM Changeset [2966] by
- Modified by hand files (to improve a little bit the performance).
- 6:35 PM Changeset [2965] by
- Code performance improved a bit by hand.
- 6:33 PM Changeset [2964] by
- Debugging code removed.
- 6:32 PM Changeset [2963] by
- Bug fixed: the pre-main for the final code is now COST k1 …
- 5:36 PM Changeset [2962] by
- Most performant algorithm restored.
- 5:02 PM Changeset [2961] by
- Bug fixed (stupid typo in pre-main code made the compiler diverge on …
- 4:51 PM Changeset [2960] by
- New extraction, it diverges in RTL execution now.
- 4:46 PM Changeset [2959] by
- Typo
- 4:45 PM Changeset [2958] by
- Error message implemented.
- 4:41 PM Changeset [2957] by
- fixed semantics_blocks
- 4:31 PM Changeset [2956] by
- fixed LTL/LIN semantics
- 4:11 PM Changeset [2955] by
- corrected stupid typo
- 3:52 PM Changeset [2954] by
- resolved circular dependency for ERTLptr's semantics
- 3:34 PM Changeset [2953] by
- Fix silly label handling bug I realised was there during my talk…
- 2:01 PM Changeset [2952] by
- * corrected all back-end premains to not pass any arguments to the …
Mar 25, 2013:
- 11:30 PM Changeset [2951] by
- New extraction. Novely: a pre-main is used in the back-end. …
- 10:39 PM Changeset [2950] by
- linearise repaired (did I do the right thing???)
- 9:48 PM Changeset [2949] by
- Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
Mar 24, 2013:
- 9:17 PM Changeset [2948] by
- Finish up measurable to structured proof, exposing the prefix and …
- 9:17 PM Changeset [2947] by
- Init change in measurable to structured file.
- 11:29 AM Changeset [2946] by
- main novelties: * there is an in-built stack_usage nat in joint …
Mar 23, 2013:
- 8:43 AM Changeset [2945] by
- Minor tweak.
- 2:31 AM Changeset [2944] by
- Some progress.
- 2:07 AM Changeset [2943] by
- Mauro, I have put a daemon in place of the proof obligation that used …
- 1:37 AM Changeset [2942] by
- Many changes: 1. Coloured graphs are now specified in terms of …
Mar 22, 2013:
- 9:46 PM Changeset [2941] by
- Update proof slides.
- 7:16 PM Changeset [2940] by
- 1. StatusSimulationHelper? changed to allow to use status_rel that …
- 10:11 AM Changeset [2939] by
- Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
- 2:11 AM Changeset [2938] by
- 1. proof of "all eliminable are eliminable" completed 2. the notion of …
Mar 21, 2013:
- 9:45 PM Changeset [2937] by
- Speed up checking of RTLabs/CostInj.ma.
- 9:45 PM Changeset [2936] by
- Disable initialisation code generation in Cminor, propogate init data …
- 9:37 PM Changeset [2935] by
- separation of RTL semantics in three different versions, and …
- 8:34 PM Changeset [2934] by
- Patch to obtain more easily comparable traces.
- 8:11 PM Changeset [2933] by
- New extraction, several bug fixed. RTL_semantics fixed by hand, will …
- 7:58 PM Changeset [2932] by
- Same comment as previous commit on this file: the previous commit was …
- 7:31 PM Changeset [2931] by
- Partial back-track from Paolo's commit, that was partial.
- 7:14 PM Changeset [2930] by
- More progress. Some useless parameters have been removed from the …
- 7:13 PM Changeset [2929] by
- Bug fixed: the coercion mechanism made you think that the CALL case …
- 6:26 PM Changeset [2928] by
- some sketches about correctness proof
- 5:17 PM Changeset [2927] by
- stupid bug in bool_of_beval
- 4:06 PM Changeset [2926] by
- corrected bug in executing Sub
- 3:39 PM Changeset [2925] by
- corrected bug in toggle_bool
- 8:39 AM Changeset [2924] by
- Make calls to a known identifier actually use a direct call.
- 8:38 AM Changeset [2923] by
- Remove some leftovers.
- 2:12 AM Changeset [2922] by
- Progress: proof of "eliminable statements can be eliminated" almost …
- 12:56 AM Changeset [2921] by
- Extracted again.
- 12:53 AM Changeset [2920] by
- dos2unix-ed
Mar 20, 2013:
- 7:21 PM Changeset [2919] by
- "MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
- 5:10 PM Changeset [2918] by
- erased stupid accidental paste at the start of file (happened when …
- 1:20 PM Changeset [2917] by
- made it so that a 0 offset does not generate adding ops when accessing …
- 12:33 PM Changeset [2916] by
- corrected yet another endianness bug in load and store
- 9:37 AM Changeset [2915] by
- Dead code removed.
- 8:39 AM Changeset [2914] by
- Use single definition for stack measurement.
- 12:24 AM Changeset [2913] by
- Bug corrected by hand. It will be corrected automatically by next …
- 12:21 AM Changeset [2912] by
- Ouch, another bug in the very same function. Fixed too, on an example …
- 12:12 AM Changeset [2911] by
- Bug fixed in the translation of casts.
Mar 19, 2013:
- 11:19 PM Changeset [2910] by
- Abstract statuses for ASM and OC completed. A simple test program can …
- 10:21 PM Changeset [2909] by
- New extraction.
- 8:00 PM Changeset [2908] by
- Bug fixed by hand, they will be fixed automatically by the new extraction.
- 7:48 PM Changeset [2907] by
- 1. a few bugs fixed 2. as_return implemented for ASM & OC
- 9:54 AM Changeset [2906] by
- Bug fixed.
- 8:42 AM Changeset [2905] by
- Semantics of ASM in place (up to return values and function call …
- 1:27 AM Changeset [2904] by
- 1. Algorithm modified by hand to make it run faster. The trusted …
- 1:25 AM Changeset [2903] by
- Extracted again.
- 1:24 AM Changeset [2902] by
- Quick hack to allow printing of OC code. It will be automatically …
- 1:22 AM Changeset [2901] by
- 1. backendPrinter renamed to printer 2. Clight printing branched into …
- 1:20 AM Changeset [2900] by
- Flushing to understand where it is slow.
- 12:33 AM Changeset [2899] by
- 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Mar 18, 2013:
- 10:03 AM Changeset [2898] by
- 1) simplification of cond and seq case for StatusSimulationHelper? …
Mar 16, 2013:
- 9:08 PM Changeset [2897] by
- Minor tidying.
- 9:08 PM Changeset [2896] by
- Complete part of measurable to structured subtraces proof that shows …
- 9:08 PM Changeset [2895] by
- Match up function id from RTLabs Callstate with shadow stack, use in …
- 9:08 PM Changeset [2894] by
- Some progress on showing that the change to structured traces …
- 9:08 PM Changeset [2893] by
- Add tlr_unrepeating.
- 9:08 PM Changeset [2892] by
- Add cost hypotheses.
- 10:42 AM Changeset [2891] by
- added precondition on seq statement and tested correct in the …
Mar 15, 2013:
- 11:11 PM Changeset [2890] by
- Exported again, now the execution is correct up to LIN for a simple …
- 7:36 PM Changeset [2889] by
- It works very nice!
- 7:31 PM Changeset [2888] by
- backtracked some partial changes
- 7:22 PM Changeset [2887] by
- Corrected bug where eliminable statements where not eliminated. …
- 7:19 PM Changeset [2886] by
- partial commit
- 7:06 PM Changeset [2885] by
- Hint at how to change everything.
- 6:37 PM Changeset [2884] by
- Debugging print added.
- 6:33 PM Changeset [2883] by
- partial commit
- 5:52 PM Changeset [2882] by
- …
- 5:51 PM Changeset [2881] by
- …
- 5:51 PM Changeset [2880] by
- …
- 12:16 PM Changeset [2879] by
- changed coercion from list of joint_seq to blocks to a more efficient one
- 11:32 AM Changeset [2878] by
- backtracked some changes that were not ready for commit
- 11:29 AM Changeset [2877] by
- Correction of a bug in my former bug correction.
- 10:58 AM Changeset [2876] by
- corrected another endianess bug in joint_semantics. Switched some …
- 1:32 AM Changeset [2875] by
- Pretty printing of object code integrated too. A couple of axioms make …
Mar 14, 2013:
- 10:46 PM Changeset [2874] by
- Syntax fixed: ./cerco [-exec] filename annotationoption
- 10:37 PM Changeset [2873] by
- Extracted again.
- 7:26 PM Changeset [2872] by
- Fix list of distributed files so that the debian package can be built
- 5:34 PM Changeset [2871] by
- op2 evaluation on beval's rendered oblivious to carry bit when …
- 4:26 PM Changeset [2870] by
- Proof fixed.
- 3:40 PM Changeset [2869] by
- some reorganization of definitions, and a new taaf_append_taaf
- 12:04 AM Changeset [2868] by
- Pretty printing of ERTL and ERTLptr code.
Mar 13, 2013:
- 11:12 PM Changeset [2867] by
- New extraction after indianess bug fixes by Paolo.
- 4:21 PM Changeset [2866] by
- corrected two bugs of the translation: constant translation used wrong …
- 2:38 PM Changeset [2865] by
- …
- 2:27 PM Changeset [2864] by
- I must have drunk yesterday: all RTL passes are printed correctly; the …
- 2:22 PM Changeset [2863] by
- Added new invariant to good_if Generalized version of cond case for …
- 2:07 PM Changeset [2862] by
- Repaired, a reverse was enough.
- 1:15 PM Changeset [2861] by
- PROVISIONAL commit: Unintentional list reversal cause final step of …
- 2:02 AM Changeset [2860] by
- RTL printing, core dumps ATM
- 1:19 AM Changeset [2859] by
- Pretty printing improved (now it always starts the visit from lbl 1).
- 12:52 AM Changeset [2858] by
- Trying to pretty print the code graph in visit order. Slightly bugged …
Mar 12, 2013:
- 8:03 PM Changeset [2857] by
- CL to CM: some invariants strengthened.
- 7:11 PM Changeset [2856] by
- Pretty printing of LTL almost finished.
- 6:51 PM Changeset [2855] by
- little bug fixed in TranslateUtils?.
- 5:53 PM Changeset [2854] by
- Pretty printing of the LTL program.
- 5:53 PM Changeset [2853] by
- Pretty printing of line/label numbers.
- 4:37 PM Changeset [2852] by
- Interim commit to re-establish well-typedness after all the recent …
- 4:13 PM Changeset [2851] by
- partial commit
- 3:54 PM Changeset [2850] by
- Progress on CL to CM. Some more cases closed modulo some critical …
- 1:41 PM Changeset [2849] by
- partial commit
- 10:56 AM Changeset [2848] by
- The pretty printer for LTL.
- 10:20 AM Changeset [2847] by
- …
- 2:28 AM Changeset [2846] by
- Pretty printing of joint programs.
Mar 11, 2013:
- 6:50 PM Changeset [2845] by
- ERTLptr to LTL correctness proof started
- 1:28 PM Changeset [2844] by
- Stupid bug fixed
- 1:02 PM Changeset [2843] by
- 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
- 12:41 PM Changeset [2842] by
- The compiler can now show all back-end traces too (assembly and object …
- 12:40 PM Changeset [2841] by
- The compiler now computes also the stack cost for every intermediate …
- 12:18 PM Changeset [2840] by
- Remove irrelevant stuff from RTLabs_partial_traces
- 12:18 PM Changeset [2839] by
- Basic structure of RTLabs measurable to structured traces results.
Mar 10, 2013:
- 1:21 PM Changeset [2838] by
- Closing some more cases
Mar 9, 2013:
- 12:19 PM Changeset [2837] by
- * filled in evaluation of LTL/LIN's extended instrucitons
Mar 8, 2013:
- 11:55 PM Changeset [2836] by
- …
- 11:54 PM Changeset [2835] by
- Included Uses.ma which is required by the untrusted code. The …
- 11:45 PM Changeset [2834] by
- Execution integrated in the compiler, as it was in the prototype. …
- 11:40 PM Changeset [2833] by
- …
- 11:40 PM Changeset [2832] by
- Added abstraction in front of cases daemon for code extraction.
- 11:38 PM Changeset [2831] by
- …
- 11:37 PM Changeset [2830] by
- Added abstractions in front of cases daemon for code extraction.
- 11:18 PM Changeset [2829] by
- Semantics files committed.
- 11:17 PM Changeset [2828] by
- 1. New semantics.ma file that puts together all semantics. It …
- 9:07 PM Changeset [2827] by
- Everything extracted again.
- 9:07 PM Changeset [2826] by
- New error messages.
- 8:36 PM Changeset [2825] by
- Progress, Clight to Cminor
- 5:37 PM Changeset [2824] by
- * moved sum on lists notation to extranat * used sum on lists to …
- 3:51 PM Changeset [2823] by
- * corrected bug in ERTL semantics (both delframe and newframe did the …
- 12:48 PM Changeset [2822] by
- A consitent proof state for Clight to Cminor, with some progress (and …
- 11:44 AM Changeset [2821] by
- * implemented preclassified system for joint (in joint/joint_fullexec.ma)
- 12:26 AM Changeset [2820] by
- Proof obligation closed.
- 12:14 AM Changeset [2819] by
- Proof obligation closed.
Mar 7, 2013:
- 11:43 PM Changeset [2818] by
- "Repaired", using non computational daemons.
- 10:31 PM Changeset [2817] by
- Repaired after Paolo's commit.
- 10:20 PM Changeset [2816] by
- Repaired after Paolo's commit.
- 9:41 PM Changeset [2815] by
- exec superseded by exec_all
- 9:39 PM Changeset [2814] by
- frontend superseded by execute_all
- 9:34 PM Changeset [2813] by
- RTLabs now printed too
- 9:23 PM Changeset [2812] by
- Pre-classified system for RTLabs.
- 9:22 PM Changeset [2811] by
- Pre-classified system for RTLabs.
- 6:36 PM Changeset [2810] by
- Cminor semantics exported.
- 6:33 PM Changeset [2809] by
- …
- 6:03 PM Changeset [2808] by
- added local_stacksize to joint internal functions to accomodate for …
- 5:43 PM Changeset [2807] by
- Yet another ErrorMessage? Removed corresponding axiom in …
- 2:51 PM Changeset [2806] by
- new b_graph_translate obligations
- 2:01 PM Changeset [2805] by
- Now also prints the trace for the labelled Clight.
- 1:55 PM Changeset [2804] by
- New executable exec_all. It contains a function to run and print all …
- 1:54 PM Changeset [2803] by
- More code extracted, used to debug the compiler.
- 1:53 PM Changeset [2802] by
- New file Clight_classified_system with the classified system for …
- 1:29 PM Changeset [2801] by
- Partial commit not yet finished
- 1:07 PM Changeset [2800] by
- Tidy up Measurable.ma a little, get rid of obsolete comments.
- 1:04 PM Changeset [2799] by
- * added taaf_to_taa, conversion from trace_any_any_free to …
- 12:56 PM Changeset [2798] by
- New error message.
- 12:55 PM Changeset [2797] by
- Extracted again after James's cleanup and the implementation of the …
- 12:10 PM Changeset [2796] by
- * added global notation for existence in Type[1] (\exists[1] x.P) * in …
- 9:31 AM Changeset [2795] by
- Added new function Measurable.observe_all_in_measurable to be used to …
- 7:47 AM Changeset [2794] by
- Minor tweaks/tidying up
Mar 6, 2013:
- 7:23 PM Changeset [2793] by
- Oops, gave fields wrong order during initialisation.
- 4:50 PM Changeset [2792] by
- Make instrumented output a little easier to read.
- 4:50 PM Changeset [2791] by
- Remove dead code in driver.
- 3:48 PM Changeset [2790] by
- Some null handling in conversion from CIL.
- 3:48 PM Changeset [2789] by
- Some changes to the driver to aid debugging.
- 3:48 PM Changeset [2788] by
- Report compiler error
- 3:48 PM Changeset [2787] by
- Output stack costs in driver.
- 2:59 PM Changeset [2786] by
- Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
- 2:58 PM Changeset [2785] by
- Traces.ma repaired
- 2:35 PM Changeset [2784] by
- Repaired after Mauro's commit.
- 12:09 PM Changeset [2783] by
- modified joint_closed_internal_function definition (added condition on …
- 3:03 AM Changeset [2782] by
- 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
- 3:00 AM Changeset [2781] by
- One more computational daemon closed.
- 2:59 AM Changeset [2780] by
- Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
Mar 5, 2013:
- 11:50 PM Changeset [2779] by
- 1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
- 11:34 PM Changeset [2778] by
- Code to pretty-print the IntelHex? output. At the moment the glue code …
- 10:03 PM Changeset [2777] by
- One computational daemon closed.
- 9:53 PM Changeset [2776] by
- The compiler now extracts also the stack cost model.
- 9:52 PM Changeset [2775] by
- The compiler now computes also the stack cost model.
- 6:15 PM Changeset [2774] by
- 1. the compiler now outputs both the stack cost model and the max …
Mar 4, 2013:
- 10:03 AM Changeset [2773] by
- 1. everything extracted again after all bugs in Matita's extraction …
- 9:55 AM Changeset [2772] by
- Useless code removed.
Mar 3, 2013:
- 11:46 PM Changeset [2771] by
- Some speed up in Policy.ma.
- 9:58 PM Changeset [2770] by
- WARNING: another big commit, touching many files in ASM/*.ma This …
- 2:59 PM Changeset [2769] by
- Mistakenly commented out both as_cost_get_label (needed; OK) as well …
- 2:44 PM Changeset [2768] by
- Nightmare: file no longer typechecks, because defn as_cost_get_labels …
- 2:03 PM Changeset [2767] by
- WARNING: BIG commit, which pushes code_size_opt check into …
- 10:39 AM Changeset [2766] by
- pruned redundant dependency on Clight/Cexec?.ma
- 12:23 AM Changeset [2765] by
- 1. correctness.ma repaired 2. we used the OC_preclassified_system to …
Mar 2, 2013:
- 11:59 PM Changeset [2764] by
- preclassified_system for object code
- 11:42 AM Changeset [2763] by
- All daemons in compiler.ma closed (i.e. proof obligations added to the …
- 2:37 AM Changeset [2762] by
- All repaired up to compiler.ma. Note: one daemon is left for one …
- 1:50 AM Changeset [2761] by
- Unused (but not useless) code commented out.
- 1:29 AM Changeset [2760] by
- 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
Mar 1, 2013:
- 7:56 PM Changeset [2759] by
- Print out costs, with choice of style. Note small anti-assertion patch …
- 7:55 PM Changeset [2758] by
- Adapt prototype's Clight printer. Doesn't use cost map yet.
- 7:13 PM Changeset [2757] by
- many things are still broken, but there is a partial backtrack on …
- 1:05 PM Changeset [2756] by
- WARNING: this commit breaks things, sorry, Paolo is going to fix …
- 11:06 AM Changeset [2755] by
- * changed primitives of abstract status (with stuf that is probably …
- 10:26 AM Changeset [2754] by
- 1. WARNING: I commented out one of James's function used in …
Feb 28, 2013:
- 5:56 PM Changeset [2753] by
- Further tidying up thanks to Claudio's strong_decidable intervention; …
- 2:36 PM Changeset [2752] by
- Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
- 2:29 PM Changeset [2751] by
- Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
- 2:27 PM Changeset [2750] by
- Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
- 2:12 PM Changeset [2749] by
- * Updated version of the Frama-C plugin.
- 2:12 PM Changeset [2748] by
- * Remove the old version of the plugin.
Feb 27, 2013:
- 10:48 PM Changeset [2747] by
- The compiler (frontend + backend)
- 10:46 PM Changeset [2746] by
- 1. debugging code in glue 2. updated version
- 10:46 PM Changeset [2745] by
- 1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
- 10:45 PM Changeset [2744] by
- Build no longer fails.
- 9:27 PM Changeset [2743] by
- Latest version of the compiler, extracted with the latest version of …
- 5:42 PM Changeset [2742] by
- Untrusted register colouring fully branched.
- 5:16 PM Changeset [2741] by
- File used only by untrusted code. Implemented in Matita to exploit …
- 4:59 PM Changeset [2740] by
- Graph colouring terminated up to Uses that will be implemented in Matita.
- 4:37 PM Changeset [2739] by
- The graph colouring algorithm takes in input also the function.
- 2:03 PM Changeset [2738] by
- Porting the graph colouring stuff from the untrusted prototype to the …
Feb 26, 2013:
- 7:37 PM Changeset [2737] by
- Commit of current proof state for Clight to Cminor translation.
- 6:18 PM Changeset [2736] by
- Untrusted fixpoint computation branched in.
- 3:35 PM Changeset [2735] by
- Note about loose end in FEMeasurable.
- 3:31 PM Changeset [2734] by
- yet another puzzling automation failure, in the repaired case: "" …
Note: See TracTimeline
for information about the timeline view.
