|
|
|
@2648
|
8 years |
sacerdot |
Back in sync with the extracted code.
|
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
|
@2646
|
8 years |
sacerdot |
A tag was classified as an error message. Fixed.
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2644
|
8 years |
campbell |
Commit some work on FEMeasurable before trying to do something nicer …
|
|
|
|
@2643
|
8 years |
sacerdot |
We are not proving erasure, so this is dead code.
|
|
|
|
@2642
|
8 years |
piccolo |
fixed joint/Traces after having posed block 0 to be Code
|
|
|
|
@2641
|
8 years |
piccolo |
defined dummy block code equals to 0
|
|
|
|
@2640
|
8 years |
tranquil |
updated RTL and RTLabs to RTL translation
|
|
|
|
@2639
|
8 years |
sacerdot |
We are not going to prove erasure. Thus this becomes dead code.
|
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
|
@2637
|
8 years |
sacerdot |
…
|
|
|
|
@2636
|
8 years |
campbell |
Extracted front-end.
|
|
|
|
@2635
|
8 years |
sacerdot |
…
|
|
|
|
@2634
|
8 years |
sacerdot |
…
|
|
|
|
@2633
|
8 years |
sacerdot |
…
|
|
|
|
@2632
|
8 years |
sacerdot |
…
|
|
|
|
@2631
|
8 years |
sacerdot |
…
|
|
|
|
@2630
|
8 years |
sacerdot |
…
|
|
|
|
@2629
|
8 years |
sacerdot |
…
|
|
|
|
@2628
|
8 years |
sacerdot |
…
|
|
|
|
@2627
|
8 years |
sacerdot |
…
|
|
|
|
@2626
|
8 years |
sacerdot |
…
|
|
|
|
@2625
|
8 years |
sacerdot |
…
|
|
|
|
@2624
|
8 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
|
@2623
|
8 years |
campbell |
Name change update.
|
|
|
|
@2622
|
8 years |
sacerdot |
…
|
|
|
|
@2621
|
8 years |
sacerdot |
…
|
|
|
|
@2620
|
8 years |
campbell |
Sufficient hacking to run the extracted Clight semantics.
|
|
|
|
@2619
|
8 years |
campbell |
Update some test cases.
|
|
|
|
@2618
|
8 years |
campbell |
Tidy up measurable a little.
|
|
|
|
@2617
|
8 years |
campbell |
Trivial simplification on split_trace.
|
|
|
|
@2616
|
8 years |
sacerdot |
…
|
|
|
|
@2615
|
8 years |
sacerdot |
…
|
|
|
|
@2614
|
8 years |
sacerdot |
…
|
|
|
|
@2613
|
8 years |
sacerdot |
…
|
|
|
|
@2612
|
8 years |
sacerdot |
…
|
|
|
|
@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…
|
|
|
|
