Timeline


and

Apr 12, 2013:

7:23 PM Changeset [3141] by mckinna
Rephrase Tullio's contribution... more work needed?
7:22 PM Changeset [3140] by campbell
Diagram illustrating nested function calls in structured traces.
7:11 PM Changeset [3139] by mckinna
English tweaks
7:03 PM Changeset [3138] by campbell
Sketch up-to-labelling bit.
6:53 PM Changeset [3137] by mckinna
Tweaks
6:47 PM Changeset [3136] by mckinna
Updates: form and content, incorporating comments from Brian, and from …
6:34 PM Changeset [3135] by campbell
Discussion with Kevin at HiPEAC workshop.
6:27 PM Changeset [3134] by mckinna
Opps uncommitted edits!
6:18 PM Changeset [3133] by mckinna
Underscores!
6:17 PM Changeset [3132] by mckinna
1st version of workshop s reports. Comments/amendments welcome!
6:10 PM Changeset [3131] by campbell
Add rest of correctness.
6:10 PM Changeset [3130] by campbell
Tweak diagram spacing.
6:10 PM Changeset [3129] by campbell
Right version of the diagram.
5:00 PM Changeset [3128] by campbell
Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
4:03 PM Changeset [3127] by piccolo
report on general proof
1:00 AM Changeset [3126] by sacerdot
Splitted into empty report + "stand alone" paper. The paper needs to …

Apr 11, 2013:

7:10 PM Changeset [3125] by sacerdot
6:34 PM Changeset [3124] by sacerdot
6:22 PM Changeset [3123] by sacerdot
3:55 PM Changeset [3122] by sacerdot
3:08 PM Changeset [3121] by sacerdot
2:04 PM Changeset [3120] by sacerdot

Apr 10, 2013:

7:15 PM Changeset [3119] by sacerdot
6:45 PM Changeset [3118] by piccolo
1) finished return case in StatusSimulationHelper? 2) started to write …
6:25 PM Changeset [3117] by sacerdot
5:07 PM Changeset [3116] by sacerdot
1:28 PM Changeset [3115] by campbell
Clean up some left-over lemmas and move comment back into place.
9:48 AM Changeset [3114] by sacerdot
Some progress on pipelines/caches.
9:39 AM cost-plug-in-0.2.tgz attached to WikiStart by regisgia
Frama-C (Nitrogen) Cost plugin

Apr 9, 2013:

7:00 PM Changeset [3113] by sacerdot
Some work on control flow analysis.
6:05 PM Changeset [3112] by tranquil
added invariant that costlabels are only assigned to NOPs (not proved …
6:05 PM Changeset [3111] by sacerdot
Skeleton
6:02 PM Changeset [3110] by sacerdot
5:28 PM Changeset [3109] by sacerdot
New version.

Apr 8, 2013:

11:50 PM Changeset [3108] by sacerdot
Towards D5.2.
1:17 PM Changeset [3107] by regisgia
* External tools to compile the plugin.

Apr 6, 2013:

7:35 PM Changeset [3106] by sacerdot
New extraction.
6:38 PM Changeset [3105] by sacerdot
Pretty printing changed. There is still an inefficiency left: activate …
6:37 PM Changeset [3104] by sacerdot
Performance improvement.
4:19 PM Changeset [3103] by mckinna
Simplified "include" dependencies
4:11 PM Changeset [3102] by mckinna
Removed redundant refs to current_instruction0, which itself has been …
4:08 PM Changeset [3101] by mckinna
Removed redundant lemma execute_1_technical, which is covered by …
4:05 PM Changeset [3100] by mckinna
Removed redundant defn of current_instruction0, which only appears in …
4:02 PM Changeset [3099] by mckinna
Simplified preliminaries: inefficient_address_of_word_labels, and …
11:44 AM Changeset [3098] by sacerdot
Performance improvement.

Apr 5, 2013:

9:53 PM Changeset [3097] by sacerdot
Performance improvement in policy computation.
6:04 PM Changeset [3096] by tranquil
preliminary work on closing correctness.ma

Apr 4, 2013:

9:53 PM Changeset [3095] by sacerdot
Some performance improvement: an heavy computation was done again and …
12:04 PM Changeset [3094] by sacerdot
Makefile with targets: byte opt clean
11:52 AM Changeset [3093] by sacerdot
Makefile replaces build, targets: byte, opt, clean
11:36 AM Changeset [3092] by sacerdot
No more references to Lustre stuff.
11:31 AM Changeset [3091] by sacerdot
11:26 AM Changeset [3090] by tassi
dist: take into account symlink
11:18 AM Changeset [3089] by sacerdot
Symbolic link to the cparser
11:16 AM Changeset [3088] by sacerdot
We now also generate the package for native code.
11:06 AM Changeset [3087] by tassi
script to build tarpall
10:53 AM Changeset [3086] by sacerdot
extracted is now in driver
10:46 AM Changeset [3085] by sacerdot
extracted directory moved into driver to make debian packages more …
10:19 AM Changeset [3084] by amadio
9:58 AM Changeset [3083] by sacerdot
The cost and stack* variables are now initialized with the cost of …
9:31 AM Changeset [3082] by mckinna
Tidying up: the long comment about preamble/renamed_symbols in the …

Apr 3, 2013:

5:54 PM Changeset [3081] by campbell
Tidy up recent work a little.
5:27 PM Changeset [3080] by sacerdot
New extraction.
5:03 PM Changeset [3079] by tranquil
added printing of ERTL, LTL and LIN's ext_seq's.
3:01 PM Changeset [3078] by tranquil
fixed change of Mov
11:49 AM Changeset [3077] by sacerdot
New extraction.
10:13 AM Changeset [3076] by mckinna
simplified include dependencies

Apr 2, 2013:

7:59 PM Changeset [3075] by mckinna
Apologies for late folding in of old changes which were left over from …
7:25 PM Changeset [3074] by campbell
Put some kind of high level proof in for front-end.
6:44 PM Changeset [3073] by sacerdot
New extraction, all tests pass.
6:39 PM Changeset [3072] by tranquil
corrected a bug (translate_store was wrong)
4:49 PM Changeset [3071] by sacerdot
4:49 PM Changeset [3070] by sacerdot
Ext case of RTL implemented.
2:09 PM Changeset [3069] by sacerdot
New extraction.
1:51 PM Changeset [3068] by sacerdot
Debugging code removed.
1:49 PM Changeset [3067] by sacerdot
New test that fails too.
1:48 PM Changeset [3066] by tranquil
* implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
1:37 PM Changeset [3065] by sacerdot
Efficiency of semantics of assembled improved: ticks_of was …
1:02 PM Changeset [3064] by sacerdot
Efficiency of the semantics of assembly improved by avoiding the …
12:16 PM Changeset [3063] by campbell
Remove measure function from FEMeasurable because we're not using it …
11:59 AM Changeset [3062] by sacerdot
Bug fixed in the semantics of Mov: the offset was ignored. Now all …
11:32 AM Changeset [3061] by sacerdot
New extraction.
11:11 AM Changeset [3060] by sacerdot
Bug fixed in the semantics of JMP. The bug was due to a bug in the …
1:25 AM Changeset [3059] by sacerdot
New extraction

Apr 1, 2013:

9:14 PM Changeset [3058] by tranquil
9:14 PM Changeset [3057] by tranquil
lookup of function identifiers was not corrected with sigma
7:17 PM Changeset [3056] by tranquil
fixed a merge gone wrong
7:04 PM Changeset [3055] by campbell
Start getting partial Clight to Cminor proof in shape for …
7:04 PM Changeset [3054] by campbell
Put missing typ check in; adjust proof because I did it a little …
7:04 PM Changeset [3053] by campbell
Cast simplification preserves measurable subtraces.
6:31 PM Changeset [3052] by tranquil
6:28 PM Changeset [3051] by tranquil
fixed order of global initialization in LINToASM. For the moment …
5:18 PM Changeset [3050] by piccolo
1) Added general commutation theorem for monads. 2) Added some …
12:06 AM Changeset [3049] by campbell
Globalenvs and initial states for cast simplification.
12:06 AM Changeset [3048] by campbell
Improve dependency for cast simplification.

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.
Note: See TracTimeline for information about the timeline view.