|
|
|
@759
|
10 years |
mulligan |
More work on the RTL to ERTL pass.
|
|
|
|
@758
|
10 years |
campbell |
Implement replacement of global var initialisation data by code in Cminor.
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@756
|
10 years |
mulligan |
Made a start on RTL. Renaming in ERTL and below to move closer to …
|
|
|
|
@754
|
10 years |
mulligan |
Syntax of RTL.
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@752
|
10 years |
mulligan |
Fixed error in BitVectorTrieSet? file.
|
|
|
|
@751
|
10 years |
campbell |
Initial version of the Cminor syntax and semantics.
|
|
|
|
@750
|
10 years |
campbell |
Track some of the changes to the prototype in RTLabs.
Just one …
|
|
|
|
@749
|
10 years |
campbell |
Make definition more explicit to avoid jmeq.
|
|
|
|
@748
|
10 years |
campbell |
Change example statement for easier testing.
|
|
|
|
@747
|
10 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
|
@745
|
10 years |
mulligan |
Changes from yesterday. Slowly implementing the functorized …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@739
|
10 years |
campbell |
Note on identifiers in CHANGES.
|
|
|
|
@738
|
10 years |
campbell |
Use lower case names for identifiers for consistency with CompCert? …
|
|
|
|
@737
|
10 years |
campbell |
Use more abstract identifiers in Clight / RTLabs.
|
|
|
|
@736
|
10 years |
campbell |
Extra type safety for identifiers.
|
|
|
|
@735
|
10 years |
mulligan |
Changes from today
|
|
|
|
@734
|
10 years |
mulligan |
Fixed lin2asm.
|
|
|
|
@733
|
10 years |
mulligan |
Fixed partial commit.
|
|
|
|
@732
|
10 years |
campbell |
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
|
|
|
|
@731
|
10 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@730
|
10 years |
campbell |
A few deviations from the prototype / CompCert? that I can think of offhand.
|
|
|
|
@729
|
10 years |
campbell |
Pretty ugly printer for RTLabs programs.
|
|
|
|
@728
|
10 years |
mulligan |
Changes from last two days.
|
|
|
|
@727
|
10 years |
campbell |
Enough fixes to let an RTLabs program run.
|
|
|
|
@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 …
|
|
|
|
@724
|
10 years |
campbell |
More tractable version of bitvector_of_nat / nat_of_bitvector.
|
|
|
|
@723
|
10 years |
mulligan |
Added dependent type internalising the invariant that LIN function …
|
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
|
@721
|
10 years |
mulligan |
Added diary of changes to project files.
|
|
|
|
@720
|
10 years |
campbell |
Sort out cost labels.
|
|
|
|
@719
|
10 years |
mulligan |
Added missing assembly file ported to matita.
|
|
|
|
@718
|
10 years |
campbell |
Add an AST type (i.e., intermediate language type) for pointers.
|
|
|
|
@717
|
10 years |
campbell |
Clean up Clight examples; better temporary definition of multiply.
|
|
|
|
@716
|
10 years |
mulligan |
Finished translating LTL statements to LIN statements. Need to …
|
|
|
|
@715
|
10 years |
mulligan |
Restored rev from Util as it appears that list reversal is not a part …
|
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
|
@713
|
10 years |
mulligan |
Commit of initial LTL files.
|
|
|
|
@712
|
10 years |
mulligan |
Changes to get things to typecheck.
|
|
|
|
@711
|
10 years |
sacerdot |
…
|
|
|
|
@710
|
10 years |
campbell |
Start of way to import RTLabs from prototype compiler.
|
|
|
|
@709
|
10 years |
sacerdot |
Notations should NOT be redefined. Just add a new interpretation.
|
|
|
|
@708
|
10 years |
campbell |
Use a more normalize-friendly definition of clight_exec to make the …
|
|
|
|
@707
|
10 years |
campbell |
Remove old branch, which was merged after the move to src.
|
|
|
|
@706
|
10 years |
sacerdot |
Fixed (reference to basics/pairs was dandling).
|
|
|
|
@705
|
10 years |
sacerdot |
Ported to new library (notation).
|
|
|
|
@704
|
10 years |
sacerdot |
Minor speedup in one theorem (less automation).
|
|
|
|
@703
|
10 years |
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
|
|
@702
|
10 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@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.
|
|
|
|
@697
|
10 years |
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
|
|
@696
|
10 years |
mulligan |
Added missing I8051 file and completed most of LIN formalisation.
|
|
|
|
@695
|
10 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
|
|
@690
|
10 years |
mulligan |
Moved new matita files into correct place.
|
|
|
|
@689
|
10 years |
mulligan |
Got rid of old Matita development files.
|
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
