|
|
|
@824
|
10 years |
campbell |
Some work on showing that casts around integer operations can be removed.
|
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@798
|
10 years |
campbell |
Fix usual matita tactic mistake.
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@786
|
10 years |
campbell |
A version of the clight matita term printer for the current prototype.
|
|
|
|
@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.
|
|
|
|
@747
|
10 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@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.
|
|
|
|
@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.
|
|
|
|
@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 …
|
|
|
|
@720
|
10 years |
campbell |
Sort out cost labels.
|
|
|
|
@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.
|
|
|
|
@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.
|
|
|
|
@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 …
|
|
|
|
@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…
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
copied from Deliverables/D3.1/C-semantics:
|
|
|
|
@693
|
10 years |
campbell |
Separate out whole program executions from the clight semantics and …
|
