Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
Older Revisions
→
source:
src
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2588
7 years
garnier
modified
Cexec/Csem?
semantics: . force andbool and orbool types to be …
Diff
Rev
Age
Author
Log Message
(edit)
@2582
7 years
garnier
Some progress on CL to CM.
(edit)
@2581
7 years
mckinna
commented out back end entirely until knock-on effects of changes to …
Diff
Rev
Age
Author
Log Message
(edit)
@2578
7 years
garnier
Progress on CL to CM, fixed some stuff in memory injections.
Diff
Rev
Age
Author
Log Message
(edit)
@2576
7 years
campbell
Add conditional test case that also uses switch removal.
(edit)
@2575
7 years
mckinna
temporary commit localised the source of trouble in the proof of …
(edit)
@2574
7 years
campbell
Update labelling simulation proofs due to some changes elsewhere.
(edit)
@2573
7 years
mckinna
temporary fixes to ensure {compiler,correctness}.ma recompile after …
(edit)
@2572
7 years
garnier
Progress on toCminorCorrectness.
(edit)
@2571
7 years
campbell
Lots of little changes for cl_tailcall and classifier change.
(edit)
@2570
7 years
piccolo
ERTLtoERTLptr in place
(edit)
@2569
7 years
campbell
Fix Clight semantics for ptr + char. (Compiler works anyway.)
(edit)
@2568
7 years
campbell
Relax some Clight type checks to Cminor type checks to avoid …
Diff
Rev
Age
Author
Log Message
(edit)
@2566
7 years
piccolo
ERTL to ERTLptr pass implemented up to a few things to be left to the …
(edit)
@2565
7 years
garnier
Cl to Cm progress.
(edit)
@2564
7 years
piccolo
ERTL fully repaired, useless part of return value of pop_ra removed.
(edit)
@2563
7 years
piccolo
Repairing ERTL: show stopper found.
(edit)
@2562
7 years
piccolo
linearise modified
(edit)
@2561
7 years
tranquil
* moved CALL as different case than joint_seq: lots of broken code now …
(edit)
@2560
7 years
garnier
Fix in trace gen for CL
(edit)
@2559
7 years
piccolo
lineariseProof finished
Diff
Rev
Age
Author
Log Message
(edit)
@2557
7 years
tranquil
minor modification of commented (for now) proof of correctness of …
(edit)
@2556
7 years
tranquil
in joint semantics and traces: added a last popped calling address to …
(edit)
@2555
7 years
piccolo
lemma eval_call_ok finished
(edit)
@2554
7 years
garnier
Proof of expression translation correctness "mostly" done for CL to …
(edit)
@2553
7 years
tranquil
as_classify changed to a partial function added a status for tailcalls
Diff
Rev
Age
Author
Log Message
(edit)
@2551
7 years
piccolo
completed isFinal and fetchStatementSigmaCommute. Fixed exit …
Diff
Rev
Age
Author
Log Message
(edit)
@2548
7 years
tranquil
in
BackEndOps?
, cleaner def of be_op2 new statement of …
(edit)
@2547
7 years
tranquil
going on in proof of linearise simplified by use of monadic functional …
Diff
Rev
Age
Author
Log Message
(edit)
@2545
7 years
garnier
Comitting current progress of CL to CM
Diff
Rev
Age
Author
Log Message
(edit)
@2543
7 years
piccolo
finished stmt_at_sigma_commute
Diff
Rev
Age
Author
Log Message
(edit)
@2541
7 years
tranquil
adapted size notation to last matita lib update (01/12/2012) that …
(edit)
@2540
7 years
tranquil
cl_jump case now provides a proof of costedness of the following state
(edit)
@2539
7 years
tranquil
added cl_jump case to trace_any_any_free
(edit)
@2538
7 years
tranquil
fixed Traces.ma after changes in joint/semantics.ma
(edit)
@2537
7 years
tranquil
rolled back changes on calls in joint. Now the save_frame parameter …
(edit)
@2536
7 years
piccolo
finished eval_seq_no_pc_sigma_commute lemma
(edit)
@2535
7 years
campbell
Add the trivial C program with check that there's a measurable subtrace.
(edit)
@2534
7 years
campbell
Tweak measurable definition to stop at the return from a function.
(edit)
@2533
7 years
campbell
Some fall out from removing floats.
(edit)
@2532
7 years
tranquil
added FCOND in LIN, and rewritten linearise so that it never adds a …
(edit)
@2531
7 years
mckinna
Trivial tweaks.
(edit)
@2530
7 years
tranquil
temporary switch to cl_jump treated as cl_other fixed script for new …
(edit)
@2529
7 years
tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
(edit)
@2528
7 years
piccolo
added cases PUSH, C_ADDRESS and COPACCS
(edit)
@2527
7 years
garnier
Progress on CL to CM.
Diff
Rev
Age
Author
Log Message
(edit)
@2516
7 years
mckinna
removed typedefs; restored older versions; moved typedefs to …
Diff
Rev
Age
Author
Log Message
(edit)
@2513
7 years
mckinna
Minor tweaks. Simplified dependencies again.
(edit)
@2512
7 years
mckinna
Simplified dependencies on ASM, to allow rollback to when …
(edit)
@2511
7 years
campbell
Conjecture main Cminor/RTLabs simulation results. Add a few notes …
(edit)
@2510
7 years
garnier
Some progress on the Cl -> Cm front
Diff
Rev
Age
Author
Log Message
(edit)
@2508
7 years
mckinna
more tweaks. compiler and correctness still build.
(edit)
@2507
7 years
piccolo
finished pop case in commutation eval_Seq_no_pc
(edit)
@2506
7 years
campbell
Use common definition of measurable.
(edit)
@2505
7 years
mckinna
Cleaned up compiler.ma; some refactoring/additional code needed in …
(edit)
@2504
7 years
mckinna
More refactoring to support the tidied up compiler.ma
(edit)
@2503
7 years
mckinna
tidied up, with new auxiliary defns, some refactoring, some code …
(edit)
@2502
7 years
campbell
Sketch a little about how measurable traces might work with RTLabs and …
(edit)
@2501
7 years
piccolo
working on lineariseProof. Not yet finished.
(edit)
@2500
7 years
garnier
Continuing work on simulation in
Clight/Cminor?
(edit)
@2499
7 years
campbell
Separate out the RTLabs abstract status record from the proofs about …
(edit)
@2498
7 years
mckinna
Refactor: Typedefs object_code and costlabel_map lifted out from …
(edit)
@2497
7 years
mckinna
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
(edit)
@2496
7 years
garnier
Some tentative work on the simulation proof for expressions, in order …
(edit)
@2495
7 years
piccolo
continuing lineariseProof
(edit)
@2494
7 years
mckinna
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
(edit)
@2493
7 years
mckinna
Change in cst_well_defd to fix previously broken defn of …
(edit)
@2492
7 years
campbell
Reduce axiomatisation in compiler.ma.
(edit)
@2491
7 years
tranquil
fixed wrt change of list member definition
(edit)
@2490
7 years
tranquil
switched back to Byte immediate (instead of beval ones) propagated …
(edit)
@2489
7 years
campbell
Conjecture some
Clight/Cminor?
simulation results.
(edit)
@2488
7 years
garnier
glitch fixed
(edit)
@2487
7 years
campbell
Set up "after_n_steps" to enforce an invariant on states.
(edit)
@2486
7 years
campbell
First go at a generalised version of measurable.
Diff
Rev
Age
Author
Log Message
(edit)
@2484
7 years
piccolo
fixed Traces and semantics added commutation record (not yet finished) …
(edit)
@2483
7 years
garnier
Memory injections for Clight to Cminor, partially axiomatized.
Diff
Rev
Age
Author
Log Message
(edit)
@2481
7 years
piccolo
corrected some inconsistencies fixed some of lineariseProof
Diff
Rev
Age
Author
Log Message
(edit)
@2478
7 years
tranquil
unified is_internal_function_of_program and is_internal_function
(edit)
@2477
7 years
tranquil
status_simulation reformulated definition of joint_classify split up …
(edit)
@2476
7 years
piccolo
fixed commutation lemmas in lineariseProof started proof of main …
(edit)
@2475
7 years
campbell
Get compiler.ma and correctness.ma checking again. Note that the …
(edit)
@2474
7 years
tranquil
changed form of a statement
(edit)
@2473
7 years
tranquil
put some generic stuff we need in the back end in extraGlobalenvs …
Diff
Rev
Age
Author
Log Message
(edit)
@2471
7 years
campbell
Tame global environments a little.
(edit)
@2470
7 years
tranquil
completely separated program counters from code pointers in joint …
(edit)
@2469
7 years
campbell
Fix up opaque type errors from recent changes.
(edit)
@2468
7 years
garnier
Floats are gone from the front-end. Some trace amount might remain in …
(edit)
@2467
7 years
piccolo
LINEARISE PROOF MODIFIED NOT YED FIXED
(edit)
@2466
7 years
campbell
Show how global environments in clight to cminor pass match up.
(edit)
@2465
7 years
campbell
Remove obsolete comment (runtime functions should be implemented later …
(edit)
@2464
7 years
piccolo
adapted lineariseProof to new semantics
(edit)
@2463
7 years
tranquil
swapped back call_rel and ret_rel…
(edit)
@2462
7 years
tranquil
separated in back end values program counters from code pointers …
Diff
Rev
Age
Author
Log Message
(edit)
@2460
7 years
campbell
Rest of variable characterisation.
(edit)
@2459
7 years
campbell
Syntax update
(edit)
@2458
7 years
campbell
Clight to Cminor allocates stack variables to disjoint regions within …
(edit)
@2457
7 years
tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
(edit)
@2456
7 years
boender
- added simple proof
Diff
Rev
Age
Author
Log Message
(edit)
@2453
7 years
tranquil
come changes in monad notation to * avoid pretty printed monsters * …
(edit)
@2452
7 years
piccolo
Completed commutation lemmas of fetch_statement
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog