|
|
@1555
|
8 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
@1554
|
8 years |
sacerdot |
Major progress in the proof.
|
|
|
@1553
|
8 years |
boender |
- added lookup_opt_lookup lemma
|
|
|
@1552
|
8 years |
campbell |
Update RTLabs structured trace definition.
|
|
|
@1551
|
8 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
@1550
|
8 years |
sacerdot |
Repaired after use of Russell for execute_1.
|
|
|
@1549
|
8 years |
mulligan |
removed cruft from costsproof.ma file so claudio can work in parallel
|
|
|
@1548
|
8 years |
sacerdot |
…
|
|
|
@1547
|
8 years |
sacerdot |
Invariant on cost of one execution step strengthened.
|
|
|
@1546
|
8 years |
tranquil |
added an option to prevent reindexing transformations from taking …
|
|
|
@1545
|
8 years |
campbell |
Use pointer record in front-end.
|
|
|
@1544
|
8 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1543
|
8 years |
tranquil |
deletion of indexed labels branch
|
|
|
@1542
|
8 years |
tranquil |
merge of indexed labels branch
|
|
|
@1541
|
8 years |
mulligan |
interpret.ma now compiles
|
|
|
@1540
|
8 years |
mulligan |
changes to proof in interrupt.ma
|
|
|
@1539
|
8 years |
tranquil |
branch up to date
|
|
|
@1538
|
8 years |
mulligan |
changes to execute_1_0 proof
|
|
|
@1537
|
8 years |
campbell |
A preliminary definition of the abstract status record for RTLabs.
|
|
|
@1536
|
8 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
@1534
|
8 years |
mulligan |
committing my changes to interpret to prevent any further conflicts
|
|
|
@1533
|
8 years |
sacerdot |
Proof of execute_1 with Russell completed (up to some daemon used before).
|
|
|
@1532
|
8 years |
campbell |
Remove jump classification from structured traces.
|
|
|
@1531
|
8 years |
campbell |
A notion of abstract structured traces.
|
|
|
@1530
|
8 years |
campbell |
Update due to Russell changes.
|
|
|
@1529
|
8 years |
campbell |
Update RTLabs to RTL with unary operation types.
|
|
|
@1528
|
8 years |
campbell |
Update most of Assembly.ma with new syntax and identifier maps.
Change …
|
|
|
@1527
|
8 years |
sacerdot |
More on Russell.
|
|
|
@1526
|
8 years |
sacerdot |
Using Russell to prove some properties.
|
|
|
@1525
|
8 years |
ayache |
D2.2: function pointers using JMP.
|
|
|
@1524
|
8 years |
boender |
- adapted files to new Matita syntax
|
|
|
@1523
|
8 years |
campbell |
Separate out positive and Z definitions from extralib.ma.
Minor syntax …
|
|
|
@1522
|
8 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
@1521
|
8 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
@1520
|
8 years |
campbell |
Generate cost labels with correct type.
|
|
|
@1519
|
8 years |
campbell |
More syntax updates.
|
|
|
@1518
|
8 years |
campbell |
Update to new syntax.
|
|
|
@1517
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1516
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
@1514
|
8 years |
mulligan |
changes from today. matita keeps dieing
|
|
|
@1513
|
8 years |
campbell |
Fix up Clight examples.
|
|
|
@1512
|
8 years |
campbell |
Shorten proof of goal that solves now.
|
|
|
@1511
|
8 years |
mulligan |
proofs, added, changes to execute_1_0 function therefore required to …
|
|
|
@1510
|
8 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
@1509
|
8 years |
mulligan |
i hate subtraction over the nats
|
|
|
@1508
|
8 years |
tranquil |
branched a version of the plug-in that is compatible with the indexed …
|
|
|
@1507
|
8 years |
tranquil |
* added an option to not use ternary expressions in costs, to …
|
|
|
@1506
|
8 years |
mulligan |
changes to costs proof over weekend
|
|
|
@1505
|
8 years |
ayache |
D2.2: addendum on 16 and 32 bits integer and function pointers support.
|
|
|
@1504
|
8 years |
ayache |
8051 ocaml: bug fix in the labelling of do-whiles.
|
|
|
@1503
|
8 years |
mulligan |
inductive type complete
|
|
|
@1502
|
8 years |
mulligan |
changes to inductive defn
|
|
|
@1501
|
8 years |
sacerdot |
We must take in account the labelled_p predicate.
|
|
|
@1500
|
8 years |
sacerdot |
Proof sketch for one of the two main proofs.
|
|
|
@1499
|
8 years |
mulligan |
part way through main statement transcription
|
|
|
@1498
|
8 years |
mulligan |
added new file for proof that costs are preserved at asm level
|
|
|
@1497
|
8 years |
mulligan |
a bit of tidying up, removing dead code, etc.
|
|
|
@1496
|
8 years |
mulligan |
problem fixed with tactics missing a semicolon to stop greedy parsing
|
|
|
@1495
|
8 years |
mulligan |
proper calculation of costs
|
|
|
@1494
|
8 years |
mulligan |
changes to get everything compiling again
|
|
|
@1493
|
8 years |
mulligan |
finished well labeled check, up to injectivity of the label map
|
|
|
@1492
|
8 years |
ayache |
Comment in D2.2 -> LINToASM about function pointers.
|
|
|
@1491
|
8 years |
ayache |
Function pointers good and working.
|
|
|
@1490
|
8 years |
ayache |
Function pointers fixed.
|
|
|
@1489
|
8 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
@1488
|
8 years |
ayache |
Function pointers in D2.2/8051. Bugged for now.
|
|
|
@1487
|
8 years |
mulligan |
committing some code for well labelling
|
|
|
@1486
|
8 years |
mulligan |
finished asm costs
|
|
|
@1485
|
8 years |
sacerdot |
Less nice definitiion of add_with_carries that avoids a quadratic …
|
|
|
@1484
|
8 years |
sacerdot |
…
|
|
|
@1483
|
8 years |
tranquil |
* implemented a first draft of loop unrolling
* correced bugs in CostExpr?
|
|
|
@1482
|
8 years |
sacerdot |
1. very long standing conflict committed (but don't ask me what the …
|
|
|
@1481
|
8 years |
sacerdot |
Proof fixed. The new standard library does not index any longer the …
|
|
|
@1480
|
8 years |
sacerdot |
Proof changed (to use new automation).
BUG FOUND: automation fails if …
|
|
|
@1479
|
8 years |
boender |
- added insert_lookup_opt
- assembly compiles now
|
|
|
@1478
|
8 years |
sacerdot |
Almost completed (up to is_finals).
|
|
|
@1477
|
8 years |
tranquil |
* corrected a bug
* implemented copy propagation
* enhanced constant …
|
|
|
@1476
|
8 years |
sacerdot |
…
|
|
|
@1475
|
8 years |
sacerdot |
Towards the two fullexec transition systems that represent …
|
|
|
@1474
|
8 years |
mulligan |
adding missing asmcosts file for computing the costs of an assembly …
|
|
|
@1473
|
8 years |
tranquil |
* implemented partial redundancy elimination
* added some tools for …
|
|
|
@1472
|
8 years |
mulligan |
moved proof utils to erasure.ma
|
|
|
@1471
|
8 years |
mulligan |
finished erasure and generalised so as to work on arbitrary joint programs
|
|
|
@1470
|
8 years |
mulligan |
finished, pretty ugly though as matita's disambiguation is a …
|
|
|
@1469
|
8 years |
mulligan |
finished new relabelling for graphs subject to one axiom closed
|
|
|
@1468
|
8 years |
tranquil |
* implemented constant propagation
* implementing partial redundancy …
|
|
|
@1467
|
8 years |
mulligan |
small change, adding entry and exit labels into the internal function, …
|
|
|
@1466
|
8 years |
mulligan |
erasure for graph based joint languages almost complete
|
|
|
@1465
|
8 years |
sacerdot |
Dead code removed.
|
|
|
@1464
|
8 years |
campbell |
Use unification hints to simplify the graph monotonicity proofs.
|
|
|
@1463
|
8 years |
mulligan |
added erasure for lin
|
|
|
@1462
|
8 years |
ayache |
Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …
|
|
|
@1461
|
8 years |
mulligan |
rewrote erasure for assembly programs
|
|
|
@1460
|
8 years |
mulligan |
most of cost label erasure for assembly language complete, with one …
|
|
|
@1459
|
8 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
@1458
|
8 years |
mulligan |
added skeleton file for erasure function for joint languages
|
|
|
@1457
|
8 years |
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
|
@1456
|
8 years |
mulligan |
changed type of pointer_of_label in report
|
|
|