|
|
@2611
|
8 years |
sacerdot |
…
|
|
|
@2610
|
8 years |
sacerdot |
…
|
|
|
@2609
|
8 years |
sacerdot |
Bibliography in place.
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
@2607
|
8 years |
sacerdot |
authors fixed
|
|
|
@2606
|
8 years |
sacerdot |
conclusions
|
|
|
@2605
|
8 years |
sacerdot |
A tentative submission to itp-2013.
We will probably not submit the …
|
|
|
@2604
|
8 years |
piccolo |
ERTLtoERTLptr in place.
|
|
|
@2603
|
8 years |
piccolo |
Dead code commented out.
|
|
|
@2602
|
8 years |
piccolo |
Dead code commented out.
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2600
|
8 years |
garnier |
Memory injections are now only defined relatively to block ids, not …
|
|
|
@2599
|
8 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
@2598
|
8 years |
garnier |
Tentative, partial draft for the definition of Clight-Cminor …
|
|
|
@2597
|
8 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
@2596
|
8 years |
campbell |
Use a simpler stack cost map, and then specialise to each semantics.
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
@2594
|
8 years |
garnier |
Some fixes in memory injections, and some holes filled.
|
|
|
@2593
|
8 years |
mckinna |
Finally chased down wicked failure to close case 1.1: of …
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
@2591
|
8 years |
garnier |
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
@2589
|
8 years |
campbell |
Add one of the simulation diagrams
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
@2587
|
8 years |
campbell |
Tweak talk a little.
|
|
|
@2586
|
8 years |
amadio |
r
|
|
|
@2585
|
8 years |
campbell |
Many improvements to proof/structured traces talk.
|
|
|
@2584
|
8 years |
regisgia |
* Update slides.
|
|
|
@2583
|
8 years |
campbell |
Structured traces talk with most of the content; not quite final.
|
|
|
@2582
|
8 years |
garnier |
Some progress on CL to CM.
|
|
|
@2581
|
8 years |
mckinna |
commented out back end entirely until knock-on effects of changes to …
|
|
|
@2580
|
8 years |
campbell |
Note on ptr + int vs int + ptr.
|
|
|
@2579
|
8 years |
regisgia |
* First version of Yann's slides.
|
|
|
@2578
|
8 years |
garnier |
Progress on CL to CM, fixed some stuff in memory injections.
|
|
|
@2577
|
8 years |
tranquil |
abstract of indexed labels talk
|
|
|
@2576
|
8 years |
campbell |
Add conditional test case that also uses switch removal.
|
|
|
@2575
|
8 years |
mckinna |
temporary commit
localised the source of trouble in the proof of
…
|
|
|
@2574
|
8 years |
campbell |
Update labelling simulation proofs due to some changes elsewhere.
|
|
|
@2573
|
8 years |
mckinna |
temporary fixes to ensure {compiler,correctness}.ma recompile
after …
|
|
|
@2572
|
8 years |
garnier |
Progress on toCminorCorrectness.
|
|
|
@2571
|
8 years |
campbell |
Lots of little changes for cl_tailcall and classifier change.
|
|
|
@2570
|
8 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
@2569
|
8 years |
campbell |
Fix Clight semantics for ptr + char. (Compiler works anyway.)
|
|
|
@2568
|
8 years |
campbell |
Relax some Clight type checks to Cminor type checks to avoid …
|
|
|
@2567
|
8 years |
amadio |
r
|
|
|
@2566
|
8 years |
piccolo |
ERTL to ERTLptr pass implemented up to a few things to be
left to the …
|
|
|
@2565
|
8 years |
garnier |
Cl to Cm progress.
|
|
|
@2564
|
8 years |
piccolo |
ERTL fully repaired, useless part of return value of pop_ra
removed.
|
|
|
@2563
|
8 years |
piccolo |
Repairing ERTL: show stopper found.
|
|
|
@2562
|
8 years |
piccolo |
linearise modified
|
|
|
@2561
|
8 years |
tranquil |
* moved CALL as different case than joint_seq: lots of broken code now …
|
|
|
@2560
|
8 years |
garnier |
Fix in trace gen for CL
|
|
|
@2559
|
8 years |
piccolo |
lineariseProof finished
|
|
|
@2558
|
8 years |
amadio |
r
|
|
|
@2557
|
8 years |
tranquil |
minor modification of commented (for now) proof of correctness of …
|
|
|
@2556
|
8 years |
tranquil |
in joint semantics and traces: added a last popped calling address to …
|
|
|
@2555
|
8 years |
piccolo |
lemma eval_call_ok finished
|
|
|
@2554
|
8 years |
garnier |
Proof of expression translation correctness "mostly" done for CL to …
|
|
|
@2553
|
8 years |
tranquil |
as_classify changed to a partial function
added a status for tailcalls
|
|
|
@2552
|
8 years |
mulligan |
Some different ideas, don't seem to be working out well.
|
|
|
@2551
|
8 years |
piccolo |
completed isFinal and fetchStatementSigmaCommute. Fixed exit …
|
|
|
@2550
|
8 years |
mulligan |
Some new ideas that lead to non-termination…
|
|
|
@2549
|
8 years |
mulligan |
Not as straightforward as first imagined…
|
|
|
@2548
|
8 years |
tranquil |
in BackEndOps?, cleaner def of be_op2
new statement of …
|
|
|
@2547
|
8 years |
tranquil |
going on in proof of linearise
simplified by use of monadic functional …
|
|
|
@2546
|
8 years |
mulligan |
Some more progress.
|
|
|
@2545
|
8 years |
garnier |
Comitting current progress of CL to CM
|
|
|
@2544
|
8 years |
mulligan |
More added, painful crash course in learning Agda. Seem to have the …
|
|
|
@2543
|
8 years |
piccolo |
finished stmt_at_sigma_commute
|
|
|
@2542
|
8 years |
mulligan |
Trying an Agda port of the polymorphic variants implementation to see …
|
|
|
@2541
|
8 years |
tranquil |
adapted size notation to last matita lib update (01/12/2012)
that …
|
|
|
@2540
|
8 years |
tranquil |
cl_jump case now provides a proof of costedness of the following state
|
|
|
@2539
|
8 years |
tranquil |
added cl_jump case to trace_any_any_free
|
|
|
@2538
|
8 years |
tranquil |
fixed Traces.ma after changes in joint/semantics.ma
|
|
|
@2537
|
8 years |
tranquil |
rolled back changes on calls in joint. Now the save_frame parameter …
|
|
|
@2536
|
8 years |
piccolo |
finished eval_seq_no_pc_sigma_commute lemma
|
|
|
@2535
|
8 years |
campbell |
Add the trivial C program with check that there's a measurable subtrace.
|
|
|
@2534
|
8 years |
campbell |
Tweak measurable definition to stop at the return from a function.
|
|
|
@2533
|
8 years |
campbell |
Some fall out from removing floats.
|
|
|
@2532
|
8 years |
tranquil |
added FCOND in LIN, and rewritten linearise so that it never adds a …
|
|
|
@2531
|
8 years |
mckinna |
Trivial tweaks.
|
|
|
@2530
|
8 years |
tranquil |
temporary switch to cl_jump treated as cl_other
fixed script for new …
|
|
|
@2529
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
@2528
|
8 years |
piccolo |
added cases PUSH, C_ADDRESS and COPACCS
|
|
|
@2527
|
8 years |
garnier |
Progress on CL to CM.
|
|
|
@2526
|
8 years |
sacerdot |
…
|
|
|
@2525
|
8 years |
sacerdot |
…
|
|
|
@2524
|
8 years |
mulligan |
Avoiding conflicts
|
|
|
@2523
|
8 years |
sacerdot |
…
|
|
|
@2522
|
8 years |
sacerdot |
Generic stuff moved to infrastructure.
|
|
|
@2521
|
8 years |
sacerdot |
..
|
|
|
@2520
|
8 years |
sacerdot |
Now it is nice!
|
|
|
@2519
|
8 years |
mulligan |
To prevent conflicts
|
|
|
@2518
|
8 years |
sacerdot |
…
|
|
|
@2517
|
8 years |
sacerdot |
…
|
|
|
@2516
|
8 years |
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
|
|
@2515
|
8 years |
sacerdot |
…
|
|
|
@2514
|
8 years |
sacerdot |
All .ma files committed: some of them are just in-progress.
|
|
|
@2513
|
8 years |
mckinna |
Minor tweaks. Simplified dependencies again.
|
|
|
@2512
|
8 years |
mckinna |
Simplified dependencies on ASM, to allow rollback to when …
|
|
|