Timeline



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

Jul 31, 2012:

6:11 PM Changeset [2283] by mulligan
Work from today.
6:08 PM Changeset [2282] by sacerdot
PUSH case almost finished
2:22 AM Changeset [2281] by sacerdot
12:10 AM Changeset [2280] by sacerdot
Proof repaired.

Jul 30, 2012:

11:44 PM Changeset [2279] by sacerdot
1. Bug fixed in the semantics of PUSH (no indirection performed) 2. …
6:33 PM Changeset [2278] by mulligan
Half of JC case complete
4:54 PM Changeset [2277] by tranquil
* replaced incorrect use of subvector_with
2:36 PM Changeset [2276] by sacerdot
1:05 PM Changeset [2275] by tranquil
* moved around some code (I8051.ma does not depend on ByteValues?.ma …
1:14 AM Changeset [2274] by sacerdot
Dead code commented out and code out of place moved to Test.ma.
12:46 AM Changeset [2273] by sacerdot
1. lemmas moved from all files to Test.ma 2. most of the lemmas in …
Note: See TracTimeline for information about the timeline view.