|
|
|
@1781
|
9 years |
mulligan |
Reinstated the lstlisting style
|
|
|
|
@1780
|
9 years |
mulligan |
finished rtl to ertl
|
|
|
|
@1779
|
9 years |
mulligan |
…
|
|
|
|
@1778
|
9 years |
sacerdot |
…
|
|
|
|
@1777
|
9 years |
mulligan |
…
|
|
|
|
@1776
|
9 years |
sacerdot |
…
|
|
|
|
@1775
|
9 years |
sacerdot |
…
|
|
|
|
@1774
|
9 years |
sacerdot |
…
|
|
|
|
@1773
|
9 years |
sacerdot |
…
|
|
|
|
@1772
|
9 years |
mulligan |
…
|
|
|
|
@1771
|
9 years |
mulligan |
some typos fixed, commit mostly to avoid conflicts
|
|
|
|
@1770
|
9 years |
mulligan |
…
|
|
|
|
@1769
|
9 years |
sacerdot |
..
|
|
|
|
@1768
|
9 years |
sacerdot |
…
|
|
|
|
@1767
|
9 years |
mulligan |
…
|
|
|
|
@1766
|
9 years |
mulligan |
avoid conflicts
|
|
|
|
@1763
|
9 years |
mulligan |
to avoid conflicts
|
|
|
|
@1762
|
9 years |
sacerdot |
Changes and fixes.
|
|
|
|
@1761
|
9 years |
sacerdot |
…
|
|
|
|
@1760
|
9 years |
mulligan |
avoiding conflicts
|
|
|
|
@1759
|
9 years |
sacerdot |
Tentative agenda.
|
|
|
|
@1758
|
9 years |
campbell |
Minor improvements to front-end; add an overall statement.
|
|
|
|
@1757
|
9 years |
sacerdot |
…
|
|
|
|
@1756
|
9 years |
sacerdot |
Improved outline.
|
|
|
|
@1755
|
9 years |
sacerdot |
…
|
|
|
|
@1754
|
9 years |
sacerdot |
…
|
|
|
|
@1753
|
9 years |
sacerdot |
…
|
|
|
|
@1752
|
9 years |
sacerdot |
…
|
|
|
|
@1751
|
9 years |
mulligan |
Commit to avoid conflicts with Claudio
|
|
|
|
@1750
|
9 years |
tranquil |
start of ERTL to LTL
|
|
|
|
@1749
|
9 years |
sacerdot |
Rephrased introduction.
|
|
|
|
@1748
|
9 years |
mulligan |
commit to avoid conflicts
|
|
|
|
@1747
|
9 years |
boender |
- New and updated version of effort table
|
|
|
|
@1746
|
9 years |
campbell |
Revisions to front-end text.
|
|
|
|
@1745
|
9 years |
sacerdot |
Conclusions.
|
|
|
|
@1744
|
9 years |
boender |
- New version of effort table
|
|
|
|
@1743
|
9 years |
mulligan |
diagrams finished, adding text
|
|
|
|
@1742
|
9 years |
boender |
- committed new version of effort table
|
|
|
|
@1741
|
9 years |
sacerdot |
…
|
|
|
|
@1740
|
9 years |
sacerdot |
…
|
|
|
|
@1739
|
9 years |
sacerdot |
Footnote for optimizations.
|
|
|
|
@1738
|
9 years |
boender |
- small change (layout)
|
|
|
|
@1737
|
9 years |
boender |
- small change
|
|
|
|
@1735
|
9 years |
mulligan |
a bit more added
|
|
|
|
@1734
|
9 years |
mulligan |
followed brian's lead in explaining the backend translation steps with …
|
|
|
|
@1733
|
9 years |
campbell |
More on front-end.
|
|
|
|
@1732
|
9 years |
campbell |
More on front-end.
|
|
|
|
@1731
|
9 years |
campbell |
A bit of front-end proof outline.
|
|
|
|
@1728
|
9 years |
mulligan |
avoiding conflicts
|
|
|
|
@1727
|
9 years |
boender |
- added last RTL - ERTL diagrams
|
|
|
|
@1726
|
9 years |
mulligan |
Finished description of LTL to LIN
|
|
|
|
@1725
|
9 years |
mulligan |
commit to avoid conflicts
|
|
|
|
@1724
|
9 years |
boender |
- added diagrams to RTL to ERTL section
|
|
|
|
@1723
|
9 years |
mulligan |
added more to header of file, commit to avoid conflicts with jaap
|
|
|
|
@1722
|
9 years |
mulligan |
changes to english in third part of report
|
|
|
|
@1721
|
9 years |
mulligan |
some changes to the report
|
|
|
|
@1720
|
9 years |
sacerdot |
New draft.
|
|
|
|
@1718
|
9 years |
mulligan |
added skull.sty for daemon (skull) symbol
|
|
|
|
@1717
|
9 years |
mulligan |
added diagrams.sty for drawing commutative diagrams
|
|
|
|
@1716
|
9 years |
mulligan |
proof outline, as requested by referees, being typed up in latex
|
|
|
|
@1715
|
9 years |
sacerdot |
Some progress.
|
|
|
|
@1714
|
9 years |
sacerdot |
…
|
|
|
|
@1708
|
9 years |
mulligan |
Change to the execution of the MOVC instruction
|
|
|
|
@1704
|
9 years |
amadio |
typo
|
|
|
|
@1703
|
9 years |
tranquil |
minimal change
|
|
|
|
@1702
|
9 years |
tranquil |
updated the report and changed a bit the names
|
|
|
|
@1701
|
9 years |
tranquil |
added updated compiler tarball
|
|
|
|
@1700
|
9 years |
tranquil |
updated README
|
|
|
|
@1699
|
9 years |
amadio |
5.1 up
|
|
|
|
@1698
|
9 years |
tranquil |
minor modifications
|
|
|
|
@1694
|
9 years |
tranquil |
indexed labels branch
|
|
|
|
@1690
|
9 years |
tranquil |
nested loops are not supported yet, the only test had one
|
|
|
|
@1689
|
9 years |
tranquil |
kept out the wrapper (which I did not touch, so not sure it works)
|
|
|
|
@1688
|
9 years |
amadio |
up d5.1-5.3
|
|
|
|
@1687
|
9 years |
tranquil |
corrected title
|
|
|
|
@1686
|
9 years |
tranquil |
corrected abstract
|
|
|
|
@1685
|
9 years |
tranquil |
adjusted comparison with aiT
|
|
|
|
@1683
|
9 years |
tranquil |
abstract and running example
|
|
|
|
@1679
|
9 years |
ayache |
Frama-C plug-in (sources+documentation)
|
|
|
|
@1678
|
9 years |
mulligan |
finished editing the english in the report
|
|
|
|
@1677
|
9 years |
mulligan |
changes to paolo's english in the report, about a 1/4 of the way through
|
|
|
|
@1676
|
9 years |
tranquil |
corrected some faults
still TODO: running example, language corrections
|
|
|
|
@1674
|
9 years |
tranquil |
corrected some faults
still TODO: running example, language corrections
|
|
|
|
@1673
|
9 years |
tranquil |
report on indexed labels
TODO: corrections, examples, etc
|
|
|
|
@1664
|
9 years |
tranquil |
corrected a bug in loop peeling where continue and breaks were not …
|
|
|
|
@1662
|
9 years |
amadio |
rev
|
|
|
|
@1661
|
9 years |
amadio |
rev
|
|
|
|
@1660
|
9 years |
ayache |
Deliverable: Frama-C plug-in (D5.1-5.3)
|
|
|
|
@1659
|
9 years |
amadio |
|
|
|
|
@1657
|
9 years |
amadio |
preliminary version of D5
|
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1590
|
9 years |
tranquil |
* got back to previous implementation of multiplication in RTLabs -> …
|
|
|
|
@1589
|
9 years |
tranquil |
* turned to argument-less return statements for RTLabs and RTL (there …
|
|
|
|
@1585
|
9 years |
tranquil |
fighting with a bug of the translation from RTL to ERTL
|
|
|
|
@1584
|
9 years |
tranquil |
* new form of translation written in graphUtilites (mainly as a test …
|
|
|
|
@1580
|
9 years |
tranquil |
implemented constant propagation in LTL
cleaned up translations in …
|
|
|
|
@1572
|
9 years |
tranquil |
* corrected previous bug
* finished propagating immediates
|
|
|
|
@1569
|
9 years |
tranquil |
* added in repository some missing files…
|
|
|
|
@1568
|
9 years |
tranquil |
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
|
|
|
|
@1546
|
9 years |
tranquil |
added an option to prevent reindexing transformations from taking …
|
|
|
|
