Timeline



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.

Oct 19, 2012:

5:05 PM Changeset [2410] by mulligan
Changes to Section 2.
4:48 PM Changeset [2409] by mulligan
Some text about algebraic data types and their limitations. Needs to …
2:07 PM Changeset [2408] by sacerdot
11:18 AM Changeset [2407] by campbell
Sigh, continue in for loops was broken too.

Oct 18, 2012:

6:35 PM Changeset [2406] by sacerdot
Elimination principle committed.
5:29 PM Changeset [2405] by sacerdot
Type of elimination principle generated + more lemmas.
4:10 PM Changeset [2404] by sacerdot
Example finished.
3:57 PM Changeset [2403] by sacerdot
More work, example almost finished up to recursive type.
3:36 PM Changeset [2402] by sacerdot
Progress on parametric types.
1:41 PM Changeset [2401] by mulligan
For Jaap's delight.
1:40 PM Changeset [2400] by sacerdot
Some tests.

Oct 17, 2012:

6:45 PM Changeset [2399] by campbell
Fill in some details about the statement of correctness.
3:35 PM Changeset [2398] by boender
- committed start of stacksize
12:27 PM Changeset [2397] by mulligan
Knocked the initial skeleton into some form of compilable state
12:20 PM Changeset [2396] by mulligan
Polymorphic variants paper skeleton
Note: See TracTimeline for information about the timeline view.