Timeline



Nov 25, 2012:

1:33 PM Changeset [2490] by tranquil
switched back to Byte immediate (instead of beval ones) propagated …

Nov 23, 2012:

5:28 PM Changeset [2489] by campbell
Conjecture some Clight/Cminor? simulation results.
4:29 PM Changeset [2488] by garnier
glitch fixed
3:47 PM Changeset [2487] by campbell
Set up "after_n_steps" to enforce an invariant on states.
12:18 PM Changeset [2486] by campbell
First go at a generalised version of measurable.
11:22 AM Changeset [2485] by campbell
Sketch of Clight/Cminor? callstate simulation

Nov 22, 2012:

6:40 PM Changeset [2484] by piccolo
fixed Traces and semantics added commutation record (not yet finished) …
5:05 PM Changeset [2483] by garnier
Memory injections for Clight to Cminor, partially axiomatized.
3:49 PM Changeset [2482] by campbell
Note about front-end simulations
10:09 AM HiPEAC13 edited by amadio
(diff)

Nov 21, 2012:

12:12 PM HiPEAC13 created by campbell

Nov 20, 2012:

6:40 PM Changeset [2481] by piccolo
corrected some inconsistencies fixed some of lineariseProof
6:39 PM Changeset [2480] by mulligan
Some more changes.
5:12 PM Changeset [2479] by mulligan
A small amount of rewriting as i didn't like the original introduction …
2:28 PM Changeset [2478] by tranquil
unified is_internal_function_of_program and is_internal_function
1:41 PM Changeset [2477] by tranquil
status_simulation reformulated definition of joint_classify split up …

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 …
Note: See TracTimeline for information about the timeline view.