|
|
|
@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 …
|
|
|
|
@795
|
10 years |
mulligan |
Changes from this morning.
|
|
|
|
@793
|
10 years |
mulligan |
Work from today on rtlabs -> rtl pass.
|
|
|
|
@790
|
10 years |
campbell |
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …
|
|
|
|
@789
|
10 years |
mulligan |
More work on rtlabs -> rtl pass.
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@781
|
10 years |
campbell |
Implement labelling pass for Clight.
|
|
|
|
@779
|
10 years |
campbell |
Add merging of tries and identifier sets (based on Dominic's earlier …
|
|
|
|
@777
|
10 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@774
|
10 years |
campbell |
Separate out the different forms of addition and subtraction in the …
|
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@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 …
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@751
|
10 years |
campbell |
Initial version of the Cminor syntax and semantics.
|
|
|
|
@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 …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@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.
|
|
|
|
@731
|
10 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@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.
|
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
|
@720
|
10 years |
campbell |
Sort out cost labels.
|
|
|
|
@718
|
10 years |
campbell |
Add an AST type (i.e., intermediate language type) for pointers.
|
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
|
@710
|
10 years |
campbell |
Start of way to import RTLabs from prototype compiler.
|
|
|
|
@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.
|
|
|
|
@695
|
10 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
copied from Deliverables/D4.2-4.3/common:
|
|
|
|
@491
|
10 years |
mulligan |
Initial commit of (part)-formalisation of LIN intermediate language.
|
