|
|
@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 …
|
|
|
@2511
|
8 years |
campbell |
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
@2509
|
8 years |
campbell |
misc note
|
|
|
@2508
|
8 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
@2507
|
8 years |
piccolo |
finished pop case in commutation eval_Seq_no_pc
|
|
|
@2506
|
8 years |
campbell |
Use common definition of measurable.
|
|
|
@2505
|
8 years |
mckinna |
Cleaned up compiler.ma; some refactoring/additional code needed in …
|
|
|
@2504
|
8 years |
mckinna |
More refactoring to support the tidied up compiler.ma
|
|
|
@2503
|
8 years |
mckinna |
tidied up, with new auxiliary defns, some refactoring, some code …
|
|
|
@2502
|
8 years |
campbell |
Sketch a little about how measurable traces might work with RTLabs and …
|
|
|
@2501
|
8 years |
piccolo |
working on lineariseProof. Not yet finished.
|
|
|
@2500
|
8 years |
garnier |
Continuing work on simulation in Clight/Cminor?
|
|
|
@2499
|
8 years |
campbell |
Separate out the RTLabs abstract status record from the proofs about …
|
|
|
@2498
|
8 years |
mckinna |
Refactor:
Typedefs object_code and costlabel_map lifted out from …
|
|
|
@2497
|
8 years |
mckinna |
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
|
|
|
@2496
|
8 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
@2495
|
8 years |
piccolo |
continuing lineariseProof
|
|
|
@2494
|
8 years |
mckinna |
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
|
|
|
@2493
|
8 years |
mckinna |
Change in cst_well_defd to fix previously broken defn of …
|
|
|
@2492
|
8 years |
campbell |
Reduce axiomatisation in compiler.ma.
|
|
|
@2491
|
8 years |
tranquil |
fixed wrt change of list member definition
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
@2489
|
8 years |
campbell |
Conjecture some Clight/Cminor? simulation results.
|
|
|
@2488
|
8 years |
garnier |
glitch fixed
|
|
|
@2487
|
8 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
@2486
|
8 years |
campbell |
First go at a generalised version of measurable.
|
|
|
@2485
|
8 years |
campbell |
Sketch of Clight/Cminor? callstate simulation
|
|
|
@2484
|
8 years |
piccolo |
fixed Traces and semantics
added commutation record (not yet finished) …
|
|
|
@2483
|
8 years |
garnier |
Memory injections for Clight to Cminor, partially axiomatized.
|
|
|
@2482
|
8 years |
campbell |
Note about front-end simulations
|
|
|
@2481
|
8 years |
piccolo |
corrected some inconsistencies
fixed some of lineariseProof
|
|
|
@2480
|
8 years |
mulligan |
Some more changes.
|
|
|
@2479
|
8 years |
mulligan |
A small amount of rewriting as i didn't like the original introduction …
|
|
|
@2478
|
8 years |
tranquil |
unified is_internal_function_of_program and is_internal_function
|
|
|
@2477
|
8 years |
tranquil |
status_simulation reformulated
definition of joint_classify split up …
|
|
|
@2476
|
8 years |
piccolo |
fixed commutation lemmas in lineariseProof
started proof of main …
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
@2474
|
8 years |
tranquil |
changed form of a statement
|
|
|
@2473
|
8 years |
tranquil |
put some generic stuff we need in the back end in extraGlobalenvs …
|
|
|
@2472
|
8 years |
campbell |
Misc clight->cminor notes.
|
|
|
@2471
|
8 years |
campbell |
Tame global environments a little.
|
|
|
@2470
|
8 years |
tranquil |
completely separated program counters from code pointers in joint …
|
|
|
@2469
|
8 years |
campbell |
Fix up opaque type errors from recent changes.
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|