Timeline



Nov 17, 2011:

5:41 PM Changeset [1514] by mulligan
changes from today. matita keeps dieing
4:50 PM Changeset [1513] by campbell
Fix up Clight examples.
4:11 PM Changeset [1512] by campbell
Shorten proof of goal that solves now.

Nov 16, 2011:

5:35 PM Changeset [1511] by mulligan
proofs, added, changes to execute_1_0 function therefore required to …
4:38 PM Changeset [1510] by sacerdot
All files ported to new dependent inversion.

Nov 15, 2011:

5:21 PM Changeset [1509] by mulligan
i hate subtraction over the nats
5:12 PM Changeset [1508] by tranquil
branched a version of the plug-in that is compatible with the indexed …
5:11 PM Changeset [1507] by tranquil
* added an option to not use ternary expressions in costs, to …
10:05 AM Changeset [1506] by mulligan
changes to costs proof over weekend

Nov 14, 2011:

1:22 PM Changeset [1505] by ayache
D2.2: addendum on 16 and 32 bits integer and function pointers support.

Nov 10, 2011:

3:39 PM Changeset [1504] by ayache
8051 ocaml: bug fix in the labelling of do-whiles.

Nov 9, 2011:

11:14 AM Changeset [1503] by mulligan
inductive type complete

Nov 8, 2011:

5:26 PM Changeset [1502] by mulligan
changes to inductive defn
1:41 PM Changeset [1501] by sacerdot
We must take in account the labelled_p predicate.
1:34 PM Changeset [1500] by sacerdot
Proof sketch for one of the two main proofs.

Nov 7, 2011:

5:06 PM Changeset [1499] by mulligan
part way through main statement transcription
4:56 PM Changeset [1498] by mulligan
added new file for proof that costs are preserved at asm level
4:51 PM Changeset [1497] by mulligan
a bit of tidying up, removing dead code, etc.
4:01 PM Changeset [1496] by mulligan
problem fixed with tactics missing a semicolon to stop greedy parsing
3:45 PM Changeset [1495] by mulligan
proper calculation of costs
10:56 AM Changeset [1494] by mulligan
changes to get everything compiling again

Nov 4, 2011:

5:01 PM Changeset [1493] by mulligan
finished well labeled check, up to injectivity of the label map
2:49 PM Changeset [1492] by ayache
Comment in D2.2 -> LINToASM about function pointers.
1:39 PM Changeset [1491] by ayache
Function pointers good and working.
1:25 PM Changeset [1490] by ayache
Function pointers fixed.
12:39 PM Changeset [1489] by campbell
Fix up a couple of lemmas affected by the change to add_with_carries.
12:22 PM Changeset [1488] by ayache
Function pointers in D2.2/8051. Bugged for now.

Nov 3, 2011:

5:24 PM Changeset [1487] by mulligan
committing some code for well labelling
2:36 PM Changeset [1486] by mulligan
finished asm costs

Nov 2, 2011:

6:58 PM Changeset [1485] by sacerdot
Less nice definitiion of add_with_carries that avoids a quadratic …
2:46 PM Changeset [1484] by sacerdot
2:40 PM Changeset [1483] by tranquil
* implemented a first draft of loop unrolling * correced bugs in CostExpr?
2:26 PM Changeset [1482] by sacerdot
1. very long standing conflict committed (but don't ask me what the …
2:00 PM Changeset [1481] by sacerdot
Proof fixed. The new standard library does not index any longer the …
1:59 PM Changeset [1480] by sacerdot
Proof changed (to use new automation). BUG FOUND: automation fails if …
8:27 AM Changeset [1479] by boender
- added insert_lookup_opt - assembly compiles now

Nov 1, 2011:

9:39 PM Changeset [1478] by sacerdot
Almost completed (up to is_finals).
6:31 PM Changeset [1477] by tranquil
* corrected a bug * implemented copy propagation * enhanced constant …
5:04 PM Changeset [1476] by sacerdot
3:14 PM Changeset [1475] by sacerdot
Towards the two fullexec transition systems that represent …

Oct 31, 2011:

10:18 AM Changeset [1474] by mulligan
adding missing asmcosts file for computing the costs of an assembly …

Oct 28, 2011:

4:45 PM Changeset [1473] by tranquil
* implemented partial redundancy elimination * added some tools for …
3:05 PM Changeset [1472] by mulligan
moved proof utils to erasure.ma
3:05 PM Changeset [1471] by mulligan
finished erasure and generalised so as to work on arbitrary joint programs

Oct 27, 2011:

5:29 PM Changeset [1470] by mulligan
finished, pretty ugly though as matita's disambiguation is a …
3:36 PM Changeset [1469] by mulligan
finished new relabelling for graphs subject to one axiom closed

Oct 26, 2011:

7:45 PM Changeset [1468] by tranquil
* implemented constant propagation * implementing partial redundancy …
5:25 PM Changeset [1467] by mulligan
small change, adding entry and exit labels into the internal function, …
5:08 PM Changeset [1466] by mulligan
erasure for graph based joint languages almost complete
2:07 PM Changeset [1465] by sacerdot
Dead code removed.

Oct 25, 2011:

7:12 PM Changeset [1464] by campbell
Use unification hints to simplify the graph monotonicity proofs.
5:33 PM Changeset [1463] by mulligan
added erasure for lin
4:11 PM Changeset [1462] by ayache
Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …

Oct 24, 2011:

5:56 PM Changeset [1461] by mulligan
rewrote erasure for assembly programs
4:53 PM Changeset [1460] by mulligan
most of cost label erasure for assembly language complete, with one …
2:34 PM Changeset [1459] by boender
- moved stronger occurs_exactly_once lemma to its proper place in …
11:44 AM Changeset [1458] by mulligan
added skeleton file for erasure function for joint languages

Oct 23, 2011:

10:15 PM Changeset [1457] by sacerdot
Bug fixed: when calling an internal function, the pc block is now set …
6:37 PM Changeset [1456] by mulligan
changed type of pointer_of_label in report
5:51 PM Changeset [1455] by mulligan
ratios changed
4:28 PM Changeset [1454] by mulligan
removed mention of axiomatised code in LIN/semantics.ma

Oct 22, 2011:

4:26 AM Changeset [1453] by sacerdot
4:26 AM Changeset [1452] by sacerdot
Bug fixed: labels MUST be represented as pointers whose block is the …
4:18 AM Changeset [1451] by sacerdot
1. All axioms in LIN/semantics.ma closed 2. succ_pc and …

Oct 21, 2011:

10:37 PM Changeset [1450] by sacerdot
Disambiguation problem avoided.
6:45 PM Changeset [1449] by mulligan
finished d4.3
6:33 PM Changeset [1448] by mulligan
finished columns in d4.2 report
6:30 PM Changeset [1447] by mulligan
changes to columns in tables
6:21 PM Changeset [1446] by sacerdot
6:19 PM Changeset [1445] by mulligan
o'caml sizes done for first table
6:12 PM Changeset [1444] by tranquil
* expression simplification finished
6:08 PM Changeset [1443] by mulligan
sizes added
6:00 PM Changeset [1442] by mulligan
changes fixing wrong deletion of conflicts
5:51 PM Changeset [1441] by mulligan
small change
5:50 PM Changeset [1440] by mulligan
ratios fixed
5:47 PM Changeset [1439] by sacerdot
5:36 PM Changeset [1438] by mulligan
changed claudio's english, added bib file
5:30 PM Changeset [1437] by sacerdot
5:27 PM Changeset [1436] by sacerdot
5:24 PM Changeset [1435] by sacerdot
More on dependent types. One citation is missing.
4:45 PM Changeset [1434] by mulligan
chages to typesetting and some wording changes
2:02 PM Changeset [1433] by tranquil
* added infrastructure to add same-language transformations along the …

Oct 20, 2011:

4:21 PM Changeset [1432] by mulligan
finished d4.2 report
3:57 PM Changeset [1431] by sacerdot
Back-end todo (in Italian only, sorry...)
3:55 PM Changeset [1430] by sacerdot
Bug fixed: push/pop must work on the isp (now added). Note: the sp is …
3:55 PM Changeset [1429] by sacerdot
Useless and removed.
3:32 PM Changeset [1428] by mulligan
finished d4.3 report
3:07 PM Changeset [1427] by mulligan
more added to d4.3 report
2:08 PM Changeset [1426] by boender
removed axiom
11:12 AM Changeset [1425] by mulligan
changes to the fixpoint calculation in ertl

Oct 19, 2011:

7:17 PM Changeset [1424] by sacerdot
1. fold function over BitVectorTries? moved from ERTLToLTL to …
6:05 PM Changeset [1423] by sacerdot
- spill no longer used - BUG IN Interference: generating the destruct …
6:05 PM Changeset [1422] by tranquil
corrected a small bug
5:59 PM Changeset [1421] by tranquil
first draft of peeling optimization: * a framework for heuristics has …
5:50 PM Changeset [1420] by mulligan
more changes
5:25 PM Changeset [1419] by sacerdot
All axioms closed.
5:11 PM Changeset [1418] by mulligan
correct ratios for semantics calculated
5:10 PM Changeset [1417] by boender
- proved that jumps always increase - this should make termination easy
4:43 PM Changeset [1416] by sacerdot
Maps from hardware registers to beval now implemented in ASM/I8051 (in …
4:22 PM Changeset [1415] by sacerdot
1. hwreg_store/retrieve no longer returns a res (but it is still …
4:03 PM Changeset [1414] by mulligan
more added
2:54 PM Changeset [1413] by mulligan
a lot more added, including updated parameters based on csc's recent submit
2:22 PM Changeset [1412] by sacerdot
Tailcalls (via ids or pointers) to internal functions implemented. …
1:39 PM Changeset [1411] by sacerdot
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
11:54 AM Changeset [1410] by campbell
Remove a few old workarounds.
11:30 AM Changeset [1409] by mulligan
added more to appendix discussing code
11:30 AM Changeset [1408] by sacerdot
1. Added joint/BEGlobalenvs that is a modification of …
11:17 AM Changeset [1407] by mulligan
almost finished

Oct 18, 2011:

4:25 PM Changeset [1406] by mulligan
a little more
4:19 PM Changeset [1405] by mulligan
yet more added. apparently there's more parameters than i ever …
3:39 PM Changeset [1404] by boender
- reworked + added - added an axiom to arithmetic, but should be provable
3:12 PM Changeset [1403] by mulligan
more added
1:30 PM Changeset [1402] by mulligan
more added
12:39 PM Changeset [1401] by ricciott
Changes concerning the new behavior of destruct.
12:14 PM Changeset [1400] by mulligan
more added on parameters
11:38 AM Changeset [1399] by mulligan
more work on parameters
Note: See TracTimeline for information about the timeline view.