|
|
|
@2395
|
8 years |
campbell |
Proper handling of comparison of pointers off-the-end of an object.
We …
|
|
|
|
@2393
|
8 years |
campbell |
A pointer comparison test case that illustrates a bug.
|
|
|
|
@2392
|
8 years |
campbell |
Labelling translations of && and || need a lot of cost labelling to …
|
|
|
|
@2391
|
8 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2389
|
8 years |
campbell |
Fix dowhile statements, and carefully arrange the translation so that …
|
|
|
|
@2388
|
8 years |
campbell |
Example of each type of control flow statement, plus minor fix to …
|
|
|
|
@2387
|
8 years |
garnier |
Revamped memory extensions, proved stuff on freeing blocks and on …
|
|
|
|
@2386
|
8 years |
garnier |
Implementation of constructive finite sets based on lists. Various …
|
|
|
|
@2385
|
8 years |
campbell |
Minor housekeeping.
|
|
|
|
@2384
|
8 years |
campbell |
Move Matita pretty printers into place.
|
|
|
|
@2353
|
8 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@2338
|
8 years |
campbell |
Use much nicer definition for making several steps in the labelling …
|
|
|
|
@2332
|
8 years |
garnier |
Some progress on switch removal. Small fix in the definition of free, …
|
|
|
|
@2328
|
8 years |
campbell |
Cut down the notion of a Clight labelled state to those where we pick …
|
|
|
|
@2326
|
8 years |
campbell |
More accurate notion of labelled states in Clight.
|
|
|
|
@2325
|
8 years |
campbell |
Fill out some Clight bits and pieces in correctness.ma.
|
|
|
|
@2319
|
8 years |
campbell |
Generate per-program cost labels rather than per-function ones, and …
|
|
|
|
@2312
|
8 years |
garnier |
Memory injections, to be revised
|
|
|
|
@2304
|
8 years |
garnier |
Strengthened proof of associativity of bitvector addition. Some more …
|
|
|
|
@2302
|
9 years |
garnier |
Finally proved associativity of addition on bitvectors. Rejoice.
|
|
|
|
@2298
|
9 years |
garnier |
WIP: converting switch removal from Z to bitvectors. Does not compile, …
|
|
|
|
@2271
|
9 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
|
@2263
|
9 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
|
@2255
|
9 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
|
@2253
|
9 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
|
@2252
|
9 years |
campbell |
Use the return statement invariant. Restructure the invariants for …
|
|
|
|
@2251
|
9 years |
campbell |
Add new invariant to Cminor that return typs should be respected.
|
|
|
|
@2250
|
9 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
|
@2249
|
9 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
|
@2234
|
9 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
|
@2232
|
9 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
|
@2231
|
9 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
|
@2227
|
9 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
|
@2219
|
9 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
|
@2203
|
9 years |
campbell |
A general result about simulations of executions.
|
|
|
|
@2202
|
9 years |
campbell |
Start defining equivalent executions.
|
|
|
|
@2201
|
9 years |
campbell |
Forgotten comment update.
|
|
|
|
@2184
|
9 years |
campbell |
Minor fix ups.
|
|
|
|
@2180
|
9 years |
campbell |
Fix off-by-one error in GenMem?.ma.
|
|
|
|
@2177
|
9 years |
campbell |
Tidy up multiplication.
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2145
|
9 years |
campbell |
Cost labelling doesn't affect interaction.
|
|
|
|
@2134
|
9 years |
campbell |
Split out behavioural equivalence spec for labelling.
|
|
|
|
@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
|
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.
|
|
|
|
