|
|
|
@1618
|
9 years |
campbell |
Minor updates due to recent changes.
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1513
|
9 years |
campbell |
Fix up Clight examples.
|
|
|
|
@1332
|
9 years |
campbell |
Summation example updated (needs computational K).
|
|
|
|
@1276
|
9 years |
campbell |
Support for replacing operations with runtime support functions in …
|
|
|
|
@1238
|
9 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
|
@1226
|
9 years |
campbell |
Adjust pretty printers for change in program records, try a test of each.
|
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1198
|
9 years |
campbell |
Clight cast removal (NB: quite different from the prototype).
|
|
|
|
@1157
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@978
|
10 years |
campbell |
Update remaining Clight examples.
|
|
|
|
@965
|
10 years |
campbell |
Update some Clight examples.
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@881
|
10 years |
campbell |
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
|
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@781
|
10 years |
campbell |
Implement labelling pass for Clight.
|
|
|
|
@776
|
10 years |
campbell |
Fix up some minor null pointer issues in Clight.
Add corresponding …
|
|
|
|
@770
|
10 years |
campbell |
Clight and Cminor examples for switch statement.
|
|
|
|
@758
|
10 years |
campbell |
Implement replacement of global var initialisation data by code in Cminor.
|
|
|
|
@748
|
10 years |
campbell |
Change example statement for easier testing.
|
|
|
|
@731
|
10 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@726
|
10 years |
campbell |
Change identifiers to Words in Clight and RTLabs semantics.
|
|
|
|
@725
|
10 years |
campbell |
Do some light manual disambiguation to make Clight examples go through …
|
|
|
|
@717
|
10 years |
campbell |
Clean up Clight examples; better temporary definition of multiply.
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
copied from Deliverables/D3.1/C-semantics/test:
|
|
|
|
@502
|
10 years |
campbell |
Fix not on nulls on Clight.
|
