|
|
|
@854
|
10 years |
mulligan |
commit to avoid conflicts
|
|
|
|
@853
|
10 years |
sacerdot |
…
|
|
|
|
@852
|
10 years |
mulligan |
foldl_strong outer definition
|
|
|
|
@851
|
10 years |
mulligan |
strong foldl added
|
|
|
|
@850
|
10 years |
sacerdot |
More informative foldl: foldll.
|
|
|
|
@849
|
10 years |
sacerdot |
…
|
|
|
|
@848
|
10 years |
sacerdot |
…
|
|
|
|
@847
|
10 years |
sacerdot |
Several bugs fixed in Matita.
|
|
|
|
@846
|
10 years |
mulligan |
changes
|
|
|
|
@845
|
10 years |
sacerdot |
Nightmare…
|
|
|
|
@844
|
10 years |
sacerdot |
Useless code removed.
|
|
|
|
@843
|
10 years |
sacerdot |
Function moved from Interpret to Status.
|
|
|
|
@842
|
10 years |
sacerdot |
Bug fixed.
|
|
|
|
@841
|
10 years |
sacerdot |
Minor changes.
|
|
|
|
@840
|
10 years |
sacerdot |
sigma defined
|
|
|
|
@839
|
10 years |
sacerdot |
More experiments.
|
|
|
|
@838
|
10 years |
sacerdot |
Restored.
|
|
|
|
@837
|
10 years |
mulligan |
changes complete
|
|
|
|
@836
|
10 years |
mulligan |
changes to assembly functions
|
|
|
|
@835
|
10 years |
sacerdot |
Old experiments removed.
|
|
|
|
@834
|
10 years |
sacerdot |
Russell at work.
|
|
|
|
@833
|
10 years |
sacerdot |
Bug fixed to make the file compile.
But the type of the assembly …
|
|
|
|
@832
|
10 years |
mulligan |
work from today
|
|
|
|
@831
|
10 years |
sacerdot |
Progress in proofs.
|
|
|
|
@829
|
10 years |
sacerdot |
…
|
|
|
|
@828
|
10 years |
sacerdot |
Proof statement.
|
|
|
|
@827
|
10 years |
sacerdot |
The preamble is now part of the PseudoStatus?.
|
|
|
|
@826
|
10 years |
mulligan |
start of proof
|
|
|
|
@825
|
10 years |
mulligan |
lots of refactoring, finally got something to prove
|
|
|
|
@824
|
10 years |
campbell |
Some work on showing that casts around integer operations can be removed.
|
|
|
|
@823
|
10 years |
mulligan |
added new file for proof of correctness of pseudo-assembly translation
|
|
|
|
@822
|
10 years |
mulligan |
removed all axioms
|
|
|
|
@821
|
10 years |
mulligan |
changes to introduce pseudostatus
|
|
|
|
@820
|
10 years |
mulligan |
changes to get the semantics of pseudoassembly working
|
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@799
|
10 years |
mulligan |
more changes.
|
|
|
|
@798
|
10 years |
campbell |
Fix usual matita tactic mistake.
|
|
|
|
@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.
|
|
|
|
@786
|
10 years |
campbell |
A version of the clight matita term printer for the current prototype.
|
|
|
|
@784
|
10 years |
mulligan |
Added missing tailcall simplification file.
|
|
|
|
@783
|
10 years |
mulligan |
rtl to ertl pass complete (modulo some straightforward axioms that …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@781
|
10 years |
campbell |
Implement labelling pass for Clight.
|
|
|
|
@780
|
10 years |
campbell |
Properly update set of registers that are used for pointers in Cminor …
|
|
|
|
@779
|
10 years |
campbell |
Add merging of tries and identifier sets (based on Dominic's earlier …
|
|
|
|
@778
|
10 years |
mulligan |
moved register set into correct place
|
|
|
|
@777
|
10 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@776
|
10 years |
campbell |
Fix up some minor null pointer issues in Clight.
Add corresponding …
|
|
|
|
@775
|
10 years |
campbell |
A few useful definitions for when RTLabs programs fail.
|
|
|
|
@774
|
10 years |
campbell |
Separate out the different forms of addition and subtraction in the …
|
|
|
|
@773
|
10 years |
campbell |
Report a couple of minor changes from the prototype compiler.
|
|
|
|
@772
|
10 years |
campbell |
Implement proper support for RTLabs addressing modes.
|
|
|
|
@771
|
10 years |
campbell |
Implement switch statements in Cminor -> RTLabs phase
|
|
|
|
@770
|
10 years |
campbell |
Clight and Cminor examples for switch statement.
|
|
|
|
@768
|
10 years |
campbell |
Make Cminor tests test translation to RTLabs.
|
|
|
|
@767
|
10 years |
campbell |
Use variable shadowing as a poor man's state monad in cminor to rtlabs …
|
|
|
|
@766
|
10 years |
campbell |
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …
|
|
|
|
@765
|
10 years |
campbell |
Remove superfluous register in RTLabs return statements.
Also fix up …
|
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
|
@763
|
10 years |
mulligan |
Changes to RTL-ERTL pass.
|
|
|
|
@762
|
10 years |
campbell |
Make naming of RTLabs files more uniform
|
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@760
|
10 years |
campbell |
Fix tailcall continuations in Cminor.
|
|
|
|
@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.
|
|
|
|
