|
|
|
@2253
|
9 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
|
@2180
|
9 years |
campbell |
Fix off-by-one error in GenMem?.ma.
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2106
|
9 years |
campbell |
Fix up a couple of proofs broken by recent changes.
|
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@1991
|
9 years |
campbell |
Put the front end transformations together and make an example use it.
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1914
|
9 years |
campbell |
Fix bug in Clight semantics that misses goto-labels inside a cost …
|
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
|
@1875
|
9 years |
campbell |
Update brief memory model test.
|
|
|
|
@1634
|
9 years |
campbell |
Update memory model examples syntax.
|
|
|
|
@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
|
9 years |
campbell |
Update pretty printers and examples.
|
|
|
|
@1139
|
9 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.
|
