|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1672
|
9 years |
campbell |
Matita now generates a couple of inversion lemmas that were manually …
|
|
|
|
@1647
|
9 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
|
@1634
|
9 years |
campbell |
Update memory model examples syntax.
|
|
|
|
@1633
|
9 years |
campbell |
Update Cminor pretty printer and examples.
|
|
|
|
@1631
|
9 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1630
|
9 years |
campbell |
Remainder of freshness in Clight to Cminor pass.
|
|
|
|
@1629
|
9 years |
campbell |
Sort out most of the fresh names stuff in Clight to Cminor.
|
|
|
|
@1628
|
9 years |
campbell |
Show that the universe generated by Clight/fresh.ma is good.
|
|
|
|
@1627
|
9 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1618
|
9 years |
campbell |
Minor updates due to recent changes.
|
|
|
|
@1612
|
9 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
|
@1608
|
9 years |
sacerdot |
Porting to new library still in progress.
|
|
|
|
@1605
|
9 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
|
@1603
|
9 years |
sacerdot |
More proofs ported to new lib.
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1566
|
9 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
|
@1545
|
9 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1513
|
9 years |
campbell |
Fix up Clight examples.
|
|
|
|
@1510
|
9 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1489
|
9 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
|
@1410
|
9 years |
campbell |
Remove a few old workarounds.
|
|
|
|
@1401
|
9 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1351
|
9 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
|
@1350
|
9 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1344
|
9 years |
sacerdot |
Ported to new destruct.
|
|
|
|
@1342
|
9 years |
sacerdot |
The new auto is much more powerful.
|
|
|
|
@1336
|
9 years |
sacerdot |
Ported to new Matita destruct/inversion.
One lemma fails at qed. …
|
|
|
|
@1332
|
9 years |
campbell |
Summation example updated (needs computational K).
|
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1276
|
9 years |
campbell |
Support for replacing operations with runtime support functions in …
|
|
|
|
@1244
|
9 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
@1238
|
9 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
|
@1231
|
9 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1226
|
9 years |
campbell |
Adjust pretty printers for change in program records, try a test of each.
|
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1216
|
9 years |
campbell |
Update Clight semantics equivalence proof to match changes in …
|
|
|
|
@1207
|
9 years |
campbell |
Second part of fixing temporaries in Clight to Cminor stage.
|
|
|
|
@1206
|
9 years |
campbell |
First stage of fixing temporary generation in Clight/toCminor.ma.
|
|
|
|
@1198
|
10 years |
campbell |
Clight cast removal (NB: quite different from the prototype).
|
|
|
|
@1194
|
10 years |
campbell |
Remove old, commented out code.
|
|
|
|
@1157
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
|
@1147
|
10 years |
campbell |
Remove some obsolete commented out code, update a couple of comments.
|
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1078
|
10 years |
campbell |
Implement stack allocation for parameters whose address is taken.
|
|
|
|
@1058
|
10 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
|
@1056
|
10 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
|
@978
|
10 years |
campbell |
Update remaining Clight examples.
|
|
|
|
@965
|
10 years |
campbell |
Update some Clight examples.
|
|
|
|
@964
|
10 years |
campbell |
Rest of cast fix.
|
|
|
|
@962
|
10 years |
campbell |
Casts should use source type's signedness, not the target's.
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@891
|
10 years |
campbell |
Revise proofs affected by recent matita change.
|
|
|
|
@886
|
10 years |
campbell |
Put types into parameter and variable lists in Cminor.
Temporarily …
|
|
|
|
@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.
|
|
|
|
@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 …
|
