|
|
@1733
|
8 years |
campbell |
More on front-end.
|
|
|
@1732
|
8 years |
campbell |
More on front-end.
|
|
|
@1731
|
8 years |
campbell |
A bit of front-end proof outline.
|
|
|
@1728
|
8 years |
mulligan |
avoiding conflicts
|
|
|
@1727
|
8 years |
boender |
- added last RTL - ERTL diagrams
|
|
|
@1726
|
8 years |
mulligan |
Finished description of LTL to LIN
|
|
|
@1725
|
8 years |
mulligan |
commit to avoid conflicts
|
|
|
@1724
|
8 years |
boender |
- added diagrams to RTL to ERTL section
|
|
|
@1723
|
8 years |
mulligan |
added more to header of file, commit to avoid conflicts with jaap
|
|
|
@1722
|
8 years |
mulligan |
changes to english in third part of report
|
|
|
@1721
|
8 years |
mulligan |
some changes to the report
|
|
|
@1720
|
8 years |
sacerdot |
New draft.
|
|
|
@1718
|
8 years |
mulligan |
added skull.sty for daemon (skull) symbol
|
|
|
@1717
|
8 years |
mulligan |
added diagrams.sty for drawing commutative diagrams
|
|
|
@1716
|
8 years |
mulligan |
proof outline, as requested by referees, being typed up in latex
|
|
|
@1715
|
8 years |
sacerdot |
Some progress.
|
|
|
@1714
|
8 years |
sacerdot |
…
|
|
|
@1708
|
8 years |
mulligan |
Change to the execution of the MOVC instruction
|
|
|
@1704
|
8 years |
amadio |
typo
|
|
|
@1703
|
8 years |
tranquil |
minimal change
|
|
|
@1702
|
8 years |
tranquil |
updated the report and changed a bit the names
|
|
|
@1701
|
8 years |
tranquil |
added updated compiler tarball
|
|
|
@1700
|
8 years |
tranquil |
updated README
|
|
|
@1699
|
8 years |
amadio |
5.1 up
|
|
|
@1698
|
8 years |
tranquil |
minor modifications
|
|
|
@1694
|
8 years |
tranquil |
indexed labels branch
|
|
|
@1690
|
8 years |
tranquil |
nested loops are not supported yet, the only test had one
|
|
|
@1689
|
8 years |
tranquil |
kept out the wrapper (which I did not touch, so not sure it works)
|
|
|
@1688
|
8 years |
amadio |
up d5.1-5.3
|
|
|
@1687
|
8 years |
tranquil |
corrected title
|
|
|
@1686
|
8 years |
tranquil |
corrected abstract
|
|
|
@1685
|
8 years |
tranquil |
adjusted comparison with aiT
|
|
|
@1683
|
8 years |
tranquil |
abstract and running example
|
|
|
@1679
|
8 years |
ayache |
Frama-C plug-in (sources+documentation)
|
|
|
@1678
|
8 years |
mulligan |
finished editing the english in the report
|
|
|
@1677
|
8 years |
mulligan |
changes to paolo's english in the report, about a 1/4 of the way through
|
|
|
@1676
|
8 years |
tranquil |
corrected some faults
still TODO: running example, language corrections
|
|
|
@1674
|
8 years |
tranquil |
corrected some faults
still TODO: running example, language corrections
|
|
|
@1673
|
8 years |
tranquil |
report on indexed labels
TODO: corrections, examples, etc
|
|
|
@1664
|
8 years |
tranquil |
corrected a bug in loop peeling where continue and breaks were not …
|
|
|
@1662
|
8 years |
amadio |
rev
|
|
|
@1661
|
8 years |
amadio |
rev
|
|
|
@1660
|
8 years |
ayache |
Deliverable: Frama-C plug-in (D5.1-5.3)
|
|
|
@1659
|
8 years |
amadio |
|
|
|
@1657
|
8 years |
amadio |
preliminary version of D5
|
|
|
@1635
|
8 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
@1590
|
8 years |
tranquil |
* got back to previous implementation of multiplication in RTLabs -> …
|
|
|
@1589
|
8 years |
tranquil |
* turned to argument-less return statements for RTLabs and RTL (there …
|
|
|
@1585
|
8 years |
tranquil |
fighting with a bug of the translation from RTL to ERTL
|
|
|
@1584
|
8 years |
tranquil |
* new form of translation written in graphUtilites (mainly as a test …
|
|
|
@1580
|
8 years |
tranquil |
implemented constant propagation in LTL
cleaned up translations in …
|
|
|
@1572
|
8 years |
tranquil |
* corrected previous bug
* finished propagating immediates
|
|
|
@1569
|
8 years |
tranquil |
* added in repository some missing files…
|
|
|
@1568
|
8 years |
tranquil |
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
|
|
|
@1546
|
8 years |
tranquil |
added an option to prevent reindexing transformations from taking …
|
|
|
@1543
|
8 years |
tranquil |
deletion of indexed labels branch
|
|
|
@1542
|
8 years |
tranquil |
merge of indexed labels branch
|
|
|
@1539
|
8 years |
tranquil |
branch up to date
|
|
|
@1525
|
8 years |
ayache |
D2.2: function pointers using JMP.
|
|
|
@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 …
|
|
|
@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.
|
|
|
@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.
|
|
|
@1488
|
8 years |
ayache |
Function pointers in D2.2/8051. Bugged for now.
|
|
|
@1483
|
8 years |
tranquil |
* implemented a first draft of loop unrolling
* correced bugs in CostExpr?
|
|
|
@1477
|
8 years |
tranquil |
* corrected a bug
* implemented copy propagation
* enhanced constant …
|
|
|
@1473
|
8 years |
tranquil |
* implemented partial redundancy elimination
* added some tools for …
|
|
|
@1468
|
8 years |
tranquil |
* implemented constant propagation
* implementing partial redundancy …
|
|
|
@1462
|
8 years |
ayache |
Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …
|
|
|
@1456
|
8 years |
mulligan |
changed type of pointer_of_label in report
|
|
|
@1455
|
8 years |
mulligan |
ratios changed
|
|
|
@1454
|
8 years |
mulligan |
removed mention of axiomatised code in LIN/semantics.ma
|
|
|
@1449
|
8 years |
mulligan |
finished d4.3
|
|
|
@1448
|
8 years |
mulligan |
finished columns in d4.2 report
|
|
|
@1447
|
8 years |
mulligan |
changes to columns in tables
|
|
|
@1446
|
8 years |
sacerdot |
…
|
|
|
@1445
|
8 years |
mulligan |
o'caml sizes done for first table
|
|
|
@1444
|
8 years |
tranquil |
* expression simplification finished
|
|
|
@1443
|
8 years |
mulligan |
sizes added
|
|
|
@1442
|
8 years |
mulligan |
changes fixing wrong deletion of conflicts
|
|
|
@1441
|
8 years |
mulligan |
small change
|
|
|
@1440
|
8 years |
mulligan |
ratios fixed
|
|
|
@1439
|
8 years |
sacerdot |
…
|
|
|
@1438
|
8 years |
mulligan |
changed claudio's english, added bib file
|
|
|
@1437
|
8 years |
sacerdot |
…
|
|
|
@1436
|
8 years |
sacerdot |
…
|
|
|
@1435
|
8 years |
sacerdot |
More on dependent types. One citation is missing.
|
|
|
@1434
|
8 years |
mulligan |
chages to typesetting and some wording changes
|
|
|
@1433
|
8 years |
tranquil |
* added infrastructure to add same-language transformations along the …
|
|
|
@1432
|
8 years |
mulligan |
finished d4.2 report
|
|
|
@1428
|
8 years |
mulligan |
finished d4.3 report
|
|
|
@1427
|
8 years |
mulligan |
more added to d4.3 report
|
|
|
@1422
|
8 years |
tranquil |
corrected a small bug
|
|
|
@1421
|
8 years |
tranquil |
first draft of peeling optimization:
* a framework for heuristics has …
|
|
|
@1420
|
8 years |
mulligan |
more changes
|
|
|
@1418
|
8 years |
mulligan |
correct ratios for semantics calculated
|
|
|
@1414
|
8 years |
mulligan |
more added
|
|
|