Timeline


and

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 …

Jul 27, 2012:

5:53 PM Changeset [2272] by mulligan
Changed proof strategy for main lemma after noticed that the current …

Jul 26, 2012:

5:02 PM Changeset [2271] by garnier
Proof of correction for the semantics of expressions under memory …
3:57 PM Changeset [2270] by mulligan
Bug spotted and fixed in write_at_stack_pointer
3:29 PM Changeset [2269] by sacerdot
Proof completely repaired up to …
2:56 PM Changeset [2268] by mulligan
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
12:05 PM Changeset [2267] by sacerdot
Call is now proved using the new strategy.
10:43 AM Changeset [2266] by sacerdot
All daemons closed in Jmp case.
3:48 AM Changeset [2265] by sacerdot
Commented out code removed.
12:38 AM Changeset [2264] by sacerdot
1) Major change: we now always use the efficient way of resolving …

Jul 25, 2012:

6:55 PM Changeset [2263] by garnier
Finished proving semantics preservation under memory injections for …
5:54 PM Changeset [2262] by mulligan
Changes from today.
5:04 PM Changeset [2261] by mulligan
Resolved conflict
4:52 PM Changeset [2260] by sacerdot
Now we use the efficient lookup_address.
4:37 PM Changeset [2259] by mulligan
For Claudio
1:47 PM Changeset [2258] by sacerdot
1. lemma generalized 2. automation replaced with expansion to make …
1:13 PM Changeset [2257] by mulligan
Daemon in SETB case closed.
12:12 PM Changeset [2256] by mulligan
MOV and MOVX cases complete

Jul 24, 2012:

8:12 PM Changeset [2255] by garnier
Had to modify the definition of memory injections to prove that …
7:40 PM Changeset [2254] by campbell
Fix up invariants in Cminor semantics.
7:40 PM Changeset [2253] by campbell
Cminor to RTLabs is now a total function.
7:40 PM Changeset [2252] by campbell
Use the return statement invariant. Restructure the invariants for …
7:40 PM Changeset [2251] by campbell
Add new invariant to Cminor that return typs should be respected.
7:40 PM Changeset [2250] by campbell
Tidy up Clight to Cminor pass a bit.
7:40 PM Changeset [2249] by campbell
Tweak Cminor invariant to be slightly more readable/extendable.
7:15 PM Changeset [2248] by sacerdot
Final changes. All daemons removed, but the real one (open goal).
6:00 PM Changeset [2247] by mulligan
Work on the MOV instruction from today and bug fixes in set_arg_1.
5:51 PM Changeset [2246] by sacerdot
Final technical lemma streamlined. Maybe it can be streamlined even more.
4:50 PM Changeset [2245] by sacerdot
Temporary commit to have a backtracking point. Yes, I know this breaks …
2:47 PM Changeset [2244] by sacerdot
Technical lemma used.
2:31 PM Changeset [2243] by sacerdot
One more lemma streamlined, one to go + one to be completed.
1:01 PM Changeset [2242] by sacerdot
jump_expansion_step3 streamlined
11:51 AM Changeset [2241] by boender
- merged changes by Claudio
11:40 AM Changeset [2240] by sacerdot
All "interesting" technical lemmas singled out, proofs to be uncommented.
11:09 AM Changeset [2239] by sacerdot
One more lemma polished.

Jul 23, 2012:

11:31 PM Changeset [2238] by sacerdot
Taken out lemma integrated.
11:11 PM Changeset [2237] by sacerdot
Even shorter version.
10:46 PM Changeset [2236] by sacerdot
One subproof made shorter.
9:22 PM Changeset [2235] by sacerdot
Towards smaller proofs.
7:31 PM Changeset [2234] by garnier
Progress on proving semantics preservation under memory injections.
4:51 PM Changeset [2233] by tranquil
* completed update of ERTL semantics * some minor changes in joint …
2:05 PM Changeset [2232] by campbell
Remove unused block structure in Cminor.
12:44 PM Changeset [2231] by garnier
Various tiny lemmas used in at least two files in the fornt-end.
10:35 AM Changeset [2230] by sacerdot
Glue proof maximally simplified or sort of.

Jul 20, 2012:

9:38 PM Changeset [2229] by sacerdot
More cleaning up, ready for more aggressive factorization.
9:10 PM Changeset [2228] by sacerdot
Further proof reduction.
8:28 PM Changeset [2227] by garnier
* New version of the switch removal algorithm, described at the top of …
6:36 PM Changeset [2226] by campbell
Whole program proof.
6:15 PM Changeset [2225] by sacerdot
Minor and major improvements everywhere, shortened proofs.
4:29 PM Changeset [2224] by campbell
Proper whole program result in RTLabs/Traces
4:29 PM Changeset [2223] by campbell
Simplify RTLabs structure traces proofs by getting rid of wrong …
10:58 AM Changeset [2222] by sacerdot
More robust to possible future changes to the "in match" semantics …
10:46 AM Changeset [2221] by boender
- removed cases daemon from PolicyFront?
2:05 AM Changeset [2220] by sacerdot
Some minor speed up and daemon-uncommenting.
Note: See TracTimeline for information about the timeline view.