|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2105
|
9 years |
campbell |
Show some results about globalenvs and program transformations.
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1873
|
9 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1640
|
9 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1465
|
9 years |
sacerdot |
Dead code removed.
|
|
|
|
@1401
|
9 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
|
@1368
|
9 years |
sacerdot |
A bug in the clear tactic makes the previous (correct) commit wrong. …
|
|
|
|
@1367
|
9 years |
sacerdot |
Proof improvement, still somehow a bit slow.
|
|
|
|
@1353
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1350
|
9 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1268
|
9 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
|
@1225
|
9 years |
campbell |
Missing ; in proof
|
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1213
|
9 years |
sacerdot |
1) New values (joint/BEValues.ma) and memory model for the back-ends
…
|
|
|
|
@1139
|
9 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1064
|
10 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
|
@1060
|
10 years |
mulligan |
work from this morning and yesterday
|
|
|
|
@1059
|
10 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
|
@1057
|
10 years |
mulligan |
changes from today
|
|
|
|
@1052
|
10 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
|
@1047
|
10 years |
mulligan |
more work from today
|
|
|
|
@1046
|
10 years |
mulligan |
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
|
|
|
|
@1045
|
10 years |
mulligan |
resolved conflict in rtlabs
|
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@882
|
10 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
|
@881
|
10 years |
campbell |
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
|
|
|
|
@880
|
10 years |
campbell |
Add type information into Cminor.
As a result, the Clight to Cminor …
|
|
|
|
@879
|
10 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
|
@849
|
10 years |
sacerdot |
…
|
|
|
|
@795
|
10 years |
mulligan |
Changes from this morning.
|
|
|
|
@793
|
10 years |
mulligan |
Work from today on rtlabs -> rtl pass.
|
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@747
|
10 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
|
@699
|
10 years |
mulligan |
More or less finished formalisation of LIN.
|
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
copied from Deliverables/D4.2-4.3/common/AST.ma:
|
|
|
|
@491
|
10 years |
mulligan |
Initial commit of (part)-formalisation of LIN intermediate language.
|
