Timeline



Nov 19, 2012:

6:04 PM Changeset [2476] by piccolo
fixed commutation lemmas in lineariseProof started proof of main …
5:13 PM Changeset [2475] by campbell
Get compiler.ma and correctness.ma checking again. Note that the …
10:57 AM Changeset [2474] by tranquil
changed form of a statement

Nov 16, 2012:

6:59 PM Changeset [2473] by tranquil
put some generic stuff we need in the back end in extraGlobalenvs …
6:41 PM Changeset [2472] by campbell
Misc clight->cminor notes.
6:41 PM Changeset [2471] by campbell
Tame global environments a little.

Nov 15, 2012:

7:06 PM Changeset [2470] by tranquil
completely separated program counters from code pointers in joint …
6:33 PM Changeset [2469] by campbell
Fix up opaque type errors from recent changes.
6:12 PM Changeset [2468] by garnier
Floats are gone from the front-end. Some trace amount might remain in …
4:43 PM Changeset [2467] by piccolo
LINEARISE PROOF MODIFIED NOT YED FIXED

Nov 14, 2012:

7:17 PM Changeset [2466] by campbell
Show how global environments in clight to cminor pass match up.
7:17 PM Changeset [2465] by campbell
Remove obsolete comment (runtime functions should be implemented later …
5:38 PM Changeset [2464] by piccolo
adapted lineariseProof to new semantics
1:20 PM Changeset [2463] by tranquil
swapped back call_rel and ret_rel…
10:31 AM Changeset [2462] by tranquil
separated in back end values program counters from code pointers …

Nov 13, 2012:

7:06 PM Changeset [2461] by campbell
First cut of inductive structured traces diagrams.
6:30 PM Changeset [2460] by campbell
Rest of variable characterisation.
6:30 PM Changeset [2459] by campbell
Syntax update
11:38 AM Changeset [2458] by campbell
Clight to Cminor allocates stack variables to disjoint regions within …
11:30 AM Changeset [2457] by tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
11:28 AM Changeset [2456] by boender
- added simple proof

Nov 12, 2012:

4:39 PM Changeset [2455] by campbell
Dump rough notes on RTLabs structured traces existence proof.
4:39 PM Changeset [2454] by campbell
More misc notes on clight->cminor.
4:30 PM Changeset [2453] by tranquil
come changes in monad notation to * avoid pretty printed monsters * …
12:50 PM Changeset [2452] by piccolo
Completed commutation lemmas of fetch_statement

Nov 10, 2012:

5:31 PM Changeset [2451] by mulligan
Structured traces paper for Brian as per e-mail conversation yesterday.

Nov 9, 2012:

6:04 PM Changeset [2450] by garnier
Minor typo
6:01 PM Changeset [2449] by garnier
Documentation added.
4:38 PM Changeset [2448] by garnier
Comitting current state of switch removal.
4:01 PM Changeset [2447] by piccolo
All axioms opened so far and that must be closed here have been closed.
1:21 PM Changeset [2446] by piccolo
Fetch commutation proof reduced to one simple (?) lemma.
11:47 AM Changeset [2445] by piccolo
1. sigma function axiomatically defined (together with its spec). …

Nov 8, 2012:

6:47 PM Changeset [2444] by campbell
Some inversion lemmas for after_n_steps for dealing with >1 source …
2:27 PM Changeset [2443] by tranquil
changed joint's stack pointer and internal stack

Nov 7, 2012:

6:12 PM Changeset [2442] by piccolo
Traces repaired. (By Paolo) Statement of lineariseProof in place.
6:02 PM Changeset [2441] by garnier
Moved general stuff on memories from switchRemoval to MemProperties?, …
5:11 PM Changeset [2440] by piccolo
fixed range_strong and linearise (commit by Paolo, he's to blame in case)
4:42 PM Changeset [2439] by campbell
Get a proper reverse mapping of function blocks to identifiers by …
11:18 AM Changeset [2438] by garnier
Sync of the w.i.p. for switch removal.

Nov 6, 2012:

5:00 PM Changeset [2437] by tranquil
generalised calls to calls with pointers
4:13 PM Changeset [2436] by tranquil
small changes
4:12 PM Changeset [2435] by tranquil
new back end operations
4:04 PM Changeset [2434] by campbell
Misc notes.
4:02 PM Changeset [2433] by campbell
Tidy up Clight pointer comparison.
3:17 PM Changeset [2432] by campbell
Remove off-the-end pointers from front end ops.
1:15 PM Changeset [2431] by campbell
Fix in matita-out branch too.
1:13 PM Changeset [2430] by campbell
Fix casting for conditionals in CompCert?-derived C parser.
12:53 PM Changeset [2429] by garnier
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
12:02 PM Changeset [2428] by campbell
Tighten requirements on switch statements in Clight to only give …

Nov 5, 2012:

11:14 AM Changeset [2427] by mulligan
More work on explanation.

Oct 31, 2012:

5:36 PM Changeset [2426] by boender
- updated stacksize to reflect new developments, completed proof - …
3:33 PM Changeset [2425] by mulligan
Garrigue's stuff completely added to the paper. Need to explain the …
12:59 PM Changeset [2424] by mulligan
Changes to the file including making a start on incorporating …

Oct 30, 2012:

5:23 PM Changeset [2423] by tranquil
as_classifier predicate → as_classify function as_call predicate from …
4:23 PM Changeset [2422] by tranquil
adapted joint to cl_call f
4:18 PM Changeset [2421] by tranquil
added simulation of flat prefix, and comments to explain the code
12:32 PM Changeset [2420] by campbell
Tidy away generic results about folds on positive/identifier maps.
11:52 AM Changeset [2419] by mulligan
Some initial work.

Oct 29, 2012:

6:19 PM Changeset [2418] by campbell
Add a checking function for the uniqueness of cost labels in RTLabs …

Oct 25, 2012:

4:36 PM Changeset [2417] by boender
- reverted changes to StructuredTraces? (shouldn't have been committed …
12:30 PM Changeset [2416] by mulligan
Some more minor changes

Oct 23, 2012:

3:57 PM Changeset [2415] by campbell
Add the ability to map blocks to symbols in preparation for stack space.
2:43 PM Changeset [2414] by mulligan
Added bib file, done a little bit of rearrangement.
11:15 AM Changeset [2413] by tranquil
* tal_rel corrected to include cases where tal_base_call \approx …

Oct 22, 2012:

4:21 PM Changeset [2412] by campbell
Tidy up measurable definition a bit more.

Oct 20, 2012:

8:08 PM Changeset [2411] by sacerdot
Extensible records implemented via option type. One axiom left.
Note: See TracTimeline for information about the timeline view.