|
|
|
@2120
|
9 years |
campbell |
Fix victim of alloc unfolding.
|
|
|
|
@2118
|
9 years |
campbell |
Labelling preserves behaviour.
|
|
|
|
@2107
|
9 years |
campbell |
Memory initialisation and program transformations.
|
|
|
|
@2106
|
9 years |
campbell |
Fix up a couple of proofs broken by recent changes.
|
|
|
|
@2105
|
9 years |
campbell |
Show some results about globalenvs and program transformations.
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@2076
|
9 years |
garnier |
First steps towards a simulation proof for switch removal.
|
|
|
|
@2074
|
9 years |
garnier |
Prophylactic renaming of a relation
|
|
|
|
@2050
|
9 years |
campbell |
Limit some normalization that doesn't seem to like.
|
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@2030
|
9 years |
garnier |
Cast simplification was too conservative, now reasonably aggressive.
|
|
|
|
@2019
|
9 years |
campbell |
Split out special induction principle for Clight from soundness file. …
|
|
|
|
@2016
|
9 years |
garnier |
Slight change in simplification strategy to better match the semantics
|
|
|
|
@2011
|
9 years |
garnier |
Minor cleanup.
|
|
|
|
@2009
|
9 years |
garnier |
Proof of simulation completed for singe-step executions.
|
|
|
|
@2000
|
9 years |
campbell |
Fix g.e. glitch in label simulation.
|
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@1991
|
9 years |
campbell |
Put the front end transformations together and make an example use it.
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1986
|
9 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1974
|
9 years |
garnier |
Progress on the cast simplification proof.
|
|
|
|
@1970
|
9 years |
garnier |
Work-in-progress: correction proof for the cast removal on expressions.
|
|
|
|
@1954
|
9 years |
campbell |
Initial state is in the labelling simulation
(modulo global envs results).
|
|
|
|
@1930
|
9 years |
campbell |
Tidy up labelling simulation stuff a bit.
|
|
|
|
@1922
|
9 years |
campbell |
Main labelling simulation proof complete.
|
|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1915
|
9 years |
garnier |
Correction of a typo in switchRemoval.
|
|
|
|
@1914
|
9 years |
campbell |
Fix bug in Clight semantics that misses goto-labels inside a cost …
|
|
|
|
@1893
|
9 years |
campbell |
Show stronger result about labelling of expressions.
|
|
|
|
@1888
|
9 years |
campbell |
Show that labelling of expressions works ...
after fixing it to match …
|
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
|
@1875
|
9 years |
campbell |
Update brief memory model test.
|
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1873
|
9 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1871
|
9 years |
campbell |
Change Clight to Cminor compilation to use gotos rather than loops, …
|
|
|
|
@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
|
10 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1630
|
10 years |
campbell |
Remainder of freshness in Clight to Cminor pass.
|
|
|
|
@1629
|
10 years |
campbell |
Sort out most of the fresh names stuff in Clight to Cminor.
|
|
|
|
@1628
|
10 years |
campbell |
Show that the universe generated by Clight/fresh.ma is good.
|
|
|
|
@1627
|
10 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1626
|
10 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1618
|
10 years |
campbell |
Minor updates due to recent changes.
|
|
|
|
@1612
|
10 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
|
@1608
|
10 years |
sacerdot |
Porting to new library still in progress.
|
|
|
|
@1605
|
10 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
|
@1603
|
10 years |
sacerdot |
More proofs ported to new lib.
|
|
|
|
@1599
|
10 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1566
|
10 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
|
@1545
|
10 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1521
|
10 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1516
|
10 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
10 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1513
|
10 years |
campbell |
Fix up Clight examples.
|
|
|
|
@1510
|
10 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1489
|
10 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
|
@1410
|
10 years |
campbell |
Remove a few old workarounds.
|
|
|
|
@1401
|
10 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
|
@1369
|
10 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1352
|
10 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1351
|
10 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
|
@1350
|
10 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1344
|
10 years |
sacerdot |
Ported to new destruct.
|
|
|
|
@1342
|
10 years |
sacerdot |
The new auto is much more powerful.
|
|
|
|
@1336
|
10 years |
sacerdot |
Ported to new Matita destruct/inversion.
One lemma fails at qed. …
|
|
|
|
@1332
|
10 years |
campbell |
Summation example updated (needs computational K).
|
|
|
|
@1316
|
10 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1276
|
10 years |
campbell |
Support for replacing operations with runtime support functions in …
|
|
|
|
@1244
|
10 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
@1238
|
10 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
|
@1231
|
10 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1226
|
10 years |
campbell |
Adjust pretty printers for change in program records, try a test of each.
|
|
|
|
@1224
|
10 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1216
|
10 years |
campbell |
Update Clight semantics equivalence proof to match changes in …
|
|
|
|
@1207
|
10 years |
campbell |
Second part of fixing temporaries in Clight to Cminor stage.
|
|
|
|
@1206
|
10 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.
|
|
|
|
