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)
@2497
8 years
mckinna
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
(edit)
@2496
8 years
garnier
Some tentative work on the simulation proof for expressions, in order …
(edit)
@2495
8 years
piccolo
continuing lineariseProof
(edit)
@2494
8 years
mckinna
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
(edit)
@2493
8 years
mckinna
Change in cst_well_defd to fix previously broken defn of …
(edit)
@2492
8 years
campbell
Reduce axiomatisation in compiler.ma.
(edit)
@2491
8 years
tranquil
fixed wrt change of list member definition
(edit)
@2490
8 years
tranquil
switched back to Byte immediate (instead of beval ones) propagated …
(edit)
@2489
8 years
campbell
Conjecture some
Clight/Cminor?
simulation results.
(edit)
@2488
8 years
garnier
glitch fixed
(edit)
@2487
8 years
campbell
Set up "after_n_steps" to enforce an invariant on states.
(edit)
@2486
8 years
campbell
First go at a generalised version of measurable.
Diff
Rev
Age
Author
Log Message
(edit)
@2484
8 years
piccolo
fixed Traces and semantics added commutation record (not yet finished) …
(edit)
@2483
8 years
garnier
Memory injections for Clight to Cminor, partially axiomatized.
Diff
Rev
Age
Author
Log Message
(edit)
@2481
8 years
piccolo
corrected some inconsistencies fixed some of lineariseProof
Diff
Rev
Age
Author
Log Message
(edit)
@2478
8 years
tranquil
unified is_internal_function_of_program and is_internal_function
(edit)
@2477
8 years
tranquil
status_simulation reformulated definition of joint_classify split up …
(edit)
@2476
8 years
piccolo
fixed commutation lemmas in lineariseProof started proof of main …
(edit)
@2475
8 years
campbell
Get compiler.ma and correctness.ma checking again. Note that the …
(edit)
@2474
8 years
tranquil
changed form of a statement
(edit)
@2473
8 years
tranquil
put some generic stuff we need in the back end in extraGlobalenvs …
Diff
Rev
Age
Author
Log Message
(edit)
@2471
8 years
campbell
Tame global environments a little.
(edit)
@2470
8 years
tranquil
completely separated program counters from code pointers in joint …
(edit)
@2469
8 years
campbell
Fix up opaque type errors from recent changes.
(edit)
@2468
8 years
garnier
Floats are gone from the front-end. Some trace amount might remain in …
(edit)
@2467
8 years
piccolo
LINEARISE PROOF MODIFIED NOT YED FIXED
(edit)
@2466
8 years
campbell
Show how global environments in clight to cminor pass match up.
(edit)
@2465
8 years
campbell
Remove obsolete comment (runtime functions should be implemented later …
(edit)
@2464
8 years
piccolo
adapted lineariseProof to new semantics
(edit)
@2463
8 years
tranquil
swapped back call_rel and ret_rel…
(edit)
@2462
8 years
tranquil
separated in back end values program counters from code pointers …
Diff
Rev
Age
Author
Log Message
(edit)
@2460
8 years
campbell
Rest of variable characterisation.
(edit)
@2459
8 years
campbell
Syntax update
(edit)
@2458
8 years
campbell
Clight to Cminor allocates stack variables to disjoint regions within …
(edit)
@2457
8 years
tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
(edit)
@2456
8 years
boender
- added simple proof
Diff
Rev
Age
Author
Log Message
(edit)
@2453
8 years
tranquil
come changes in monad notation to * avoid pretty printed monsters * …
(edit)
@2452
8 years
piccolo
Completed commutation lemmas of fetch_statement
Diff
Rev
Age
Author
Log Message
(edit)
@2450
8 years
garnier
Minor typo
(edit)
@2449
8 years
garnier
Documentation added.
(edit)
@2448
8 years
garnier
Comitting current state of switch removal.
(edit)
@2447
8 years
piccolo
All axioms opened so far and that must be closed here have been closed.
(edit)
@2446
8 years
piccolo
Fetch commutation proof reduced to one simple (?) lemma.
(edit)
@2445
8 years
piccolo
1. sigma function axiomatically defined (together with its spec). …
(edit)
@2444
8 years
campbell
Some inversion lemmas for after_n_steps for dealing with >1 source …
(edit)
@2443
8 years
tranquil
changed joint's stack pointer and internal stack
(edit)
@2442
8 years
piccolo
Traces repaired. (By Paolo) Statement of lineariseProof in place.
(edit)
@2441
8 years
garnier
Moved general stuff on memories from switchRemoval to
MemProperties?
, …
(edit)
@2440
8 years
piccolo
fixed range_strong and linearise (commit by Paolo, he's to blame in case)
(edit)
@2439
8 years
campbell
Get a proper reverse mapping of function blocks to identifiers by …
(edit)
@2438
8 years
garnier
Sync of the w.i.p. for switch removal.
(edit)
@2437
8 years
tranquil
generalised calls to calls with pointers
(edit)
@2436
8 years
tranquil
small changes
(edit)
@2435
8 years
tranquil
new back end operations
Diff
Rev
Age
Author
Log Message
(edit)
@2433
8 years
campbell
Tidy up Clight pointer comparison.
(edit)
@2432
8 years
campbell
Remove off-the-end pointers from front end ops.
Diff
Rev
Age
Author
Log Message
(edit)
@2429
8 years
garnier
Restrict semantics of pointer comparison to what
CompCert?
does - i.e. …
(edit)
@2428
8 years
campbell
Tighten requirements on switch statements in Clight to only give …
Diff
Rev
Age
Author
Log Message
(edit)
@2426
8 years
boender
- updated stacksize to reflect new developments, completed proof - …
Diff
Rev
Age
Author
Log Message
(edit)
@2423
8 years
tranquil
as_classifier predicate → as_classify function as_call predicate from …
(edit)
@2422
8 years
tranquil
adapted joint to cl_call f
(edit)
@2421
8 years
tranquil
added simulation of flat prefix, and comments to explain the code
(edit)
@2420
8 years
campbell
Tidy away generic results about folds on positive/identifier maps.
Diff
Rev
Age
Author
Log Message
(edit)
@2418
8 years
campbell
Add a checking function for the uniqueness of cost labels in RTLabs …
(edit)
@2417
8 years
boender
- reverted changes to
StructuredTraces?
(shouldn't have been committed …
Diff
Rev
Age
Author
Log Message
(edit)
@2415
8 years
campbell
Add the ability to map blocks to symbols in preparation for stack space.
Diff
Rev
Age
Author
Log Message
(edit)
@2413
8 years
tranquil
* tal_rel corrected to include cases where tal_base_call \approx …
(edit)
@2412
8 years
campbell
Tidy up measurable definition a bit more.
Diff
Rev
Age
Author
Log Message
(edit)
@2407
8 years
campbell
Sigh, continue in for loops was broken too.
Diff
Rev
Age
Author
Log Message
(edit)
@2399
8 years
campbell
Fill in some details about the statement of correctness.
(edit)
@2398
8 years
boender
- committed start of stacksize
Diff
Rev
Age
Author
Log Message
(edit)
@2395
8 years
campbell
Proper handling of comparison of pointers off-the-end of an object. We …
Diff
Rev
Age
Author
Log Message
(edit)
@2393
8 years
campbell
A pointer comparison test case that illustrates a bug.
(edit)
@2392
8 years
campbell
Labelling translations of && and || need a lot of cost labelling to …
(edit)
@2391
8 years
campbell
Revert "Put the post-loop cost label into the Clight while statement …
(edit)
@2390
8 years
campbell
Tidy up a corner case when generating RTLabs so that we generate less …
(edit)
@2389
8 years
campbell
Fix dowhile statements, and carefully arrange the translation so that …
(edit)
@2388
8 years
campbell
Example of each type of control flow statement, plus minor fix to …
(edit)
@2387
8 years
garnier
Revamped memory extensions, proved stuff on freeing blocks and on …
(edit)
@2386
8 years
garnier
Implementation of constructive finite sets based on lists. Various …
(edit)
@2385
8 years
campbell
Minor housekeeping.
Diff
Rev
Age
Author
Log Message
(edit)
@2353
8 years
campbell
Put the post-loop cost label into the Clight while statement to get …
Diff
Rev
Age
Author
Log Message
(edit)
@2338
8 years
campbell
Use much nicer definition for making several steps in the labelling …
Diff
Rev
Age
Author
Log Message
(edit)
@2335
8 years
campbell
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …
Diff
Rev
Age
Author
Log Message
(edit)
@2332
8 years
garnier
Some progress on switch removal. Small fix in the definition of free, …
Diff
Rev
Age
Author
Log Message
(edit)
@2328
8 years
campbell
Cut down the notion of a Clight labelled state to those where we pick …
(edit)
@2327
8 years
mulligan
Fixed typos in paper highlighted by referees. More substantial …
(edit)
@2326
8 years
campbell
More accurate notion of labelled states in Clight.
(edit)
@2325
8 years
campbell
Fill out some Clight bits and pieces in correctness.ma.
(edit)
@2324
8 years
tranquil
semantics of blocks: function to produce trace from execution of …
(edit)
@2323
8 years
campbell
Some correctness proof comments.
(edit)
@2322
8 years
campbell
Today's correctness groupthink.
Diff
Rev
Age
Author
Log Message
(edit)
@2320
8 years
campbell
Update compiler and correctness with labelling changes.
(edit)
@2319
8 years
campbell
Generate per-program cost labels rather than per-function ones, and …
(edit)
@2318
8 years
boender
- now it compiles
(edit)
@2317
8 years
boender
- small changes to make things compile
(edit)
@2316
8 years
boender
- committed temporary version: true version has to wait until I …
(edit)
@2315
8 years
campbell
Add some more commentary.
(edit)
@2314
8 years
campbell
Move generic definitions from recent commit to appropriate places.
(edit)
@2313
8 years
campbell
RTLabs cost checker correct.
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog