Timeline



Aug 31, 2012:

4:52 PM Changeset [2315] by campbell
Add some more commentary.
4:12 PM Changeset [2314] by campbell
Move generic definitions from recent commit to appropriate places.
2:39 PM Changeset [2313] by campbell
RTLabs cost checker correct.
2:14 PM Changeset [2312] by garnier
Memory injections, to be revised
2:12 PM Changeset [2311] by garnier
Some more cleaning of switchRemoval …
12:50 PM Changeset [2310] by garnier
Moved a lemma from switchRemoval to positive.
11:35 AM Changeset [2309] by garnier
Removed the superfluous xorb definition and move some basic properties …

Aug 30, 2012:

7:20 PM Changeset [2308] by campbell
More proof (and corrections) on cost checking.
4:47 PM Changeset [2307] by campbell
Half the proofs for sound cost labelling check.
4:47 PM Changeset [2306] by campbell
An insertion sort for testing purposes.
4:47 PM Changeset [2305] by campbell
RTLabs cost spec checking function implemented (lacks proof, or much …

Aug 29, 2012:

11:21 PM Changeset [2304] by garnier
Strengthened proof of associativity of bitvector addition. Some more …

Aug 24, 2012:

5:41 PM Changeset [2303] by campbell
Some preliminary checking of cost labelling properties in RTLabs.
1:11 PM Changeset [2302] by garnier
Finally proved associativity of addition on bitvectors. Rejoice.

Aug 22, 2012:

5:30 PM Changeset [2301] by mulligan
Trying to get the big proof working again

Aug 21, 2012:

7:00 PM Changeset [2300] by campbell
Cut out some dead ends and add some comments to the last commit.
7:00 PM Changeset [2299] by campbell
Soundly labelled RTLabs structured traces are "unrepeating".

Aug 16, 2012:

7:01 PM Changeset [2298] by garnier
WIP: converting switch removal from Z to bitvectors. Does not compile, …
6:03 PM Changeset [2297] by campbell
Nicer form of steps until cost label bound in RTLabs.

Aug 13, 2012:

2:18 PM Changeset [2296] by campbell
Tidy up some ill-placed definitions.
12:21 PM Changeset [2295] by campbell
Start on showing unrepeating property of RTLabs structured traces: …
12:21 PM Changeset [2294] by campbell
Make RTLabs cost spec deterministic.
12:21 PM Changeset [2293] by campbell
Add instruction pointer for call states in RTLabs.

Aug 2, 2012:

6:40 PM Changeset [2292] by campbell
More RTLabs invariants.
5:04 PM Changeset [2291] by campbell
Disable switch removal in compiler.ma for now.
5:04 PM Changeset [2290] by campbell
Remove jump tables from RTLabs -> RTL.
5:04 PM Changeset [2289] by campbell
Update alias
5:04 PM Changeset [2288] by campbell
Remove jumptables from RTLabs. :(
5:04 PM Changeset [2287] by campbell
RTLabs typing for loads and stores.
3:18 PM Changeset [2286] by tranquil
Big update! * merge of all _paolo variants * reorganised some depends …
1:58 PM Changeset [2285] by sacerdot
1. duplicated code erased 2. POP case finished up to lemmas on …

Aug 1, 2012:

4:56 PM Changeset [2284] by sacerdot
PUSH finished
Note: See TracTimeline for information about the timeline view.