|
|
@2992
|
8 years |
campbell |
Add "only one return" invariant to RTLabs functions.
|
|
|
@2971
|
8 years |
campbell |
Single RTLabs return statement.
|
|
|
@2936
|
8 years |
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
|
@2924
|
8 years |
campbell |
Make calls to a known identifier actually use a direct call.
|
|
|
@2809
|
8 years |
sacerdot |
…
|
|
|
@2793
|
8 years |
campbell |
Oops, gave fields wrong order during initialisation.
|
|
|
@2737
|
8 years |
garnier |
Commit of current proof state for Clight to Cminor translation.
|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2624
|
8 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2598
|
8 years |
garnier |
Tentative, partial draft for the definition of Clight-Cminor …
|
|
|
@2597
|
8 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
@2511
|
8 years |
campbell |
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …
|
|
|
@2496
|
8 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
@2489
|
8 years |
campbell |
Conjecture some Clight/Cminor? simulation results.
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
@2395
|
8 years |
campbell |
Proper handling of comparison of pointers off-the-end of an object.
We …
|
|
|
@2390
|
8 years |
campbell |
Tidy up a corner case when generating RTLabs so that we generate
less …
|
|
|
@2384
|
8 years |
campbell |
Move Matita pretty printers into place.
|
|
|
@2335
|
8 years |
campbell |
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …
|
|
|
@2319
|
9 years |
campbell |
Generate per-program cost labels rather than per-function ones, and …
|
|
|
@2292
|
9 years |
campbell |
More RTLabs invariants.
|
|
|
@2289
|
9 years |
campbell |
Update alias
|
|
|
@2287
|
9 years |
campbell |
RTLabs typing for loads and stores.
|
|
|
@2254
|
9 years |
campbell |
Fix up invariants in Cminor semantics.
|
|
|
@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.
|
|
|
@2249
|
9 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
@2232
|
9 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
@2178
|
9 years |
campbell |
Shift some notation into utilities.
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
@2033
|
9 years |
sacerdot |
Daemon reverted.
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
@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.
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
@1680
|
9 years |
campbell |
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …
|
|
|
@1655
|
9 years |
campbell |
Update Cminor and RTLabs semantics to use new monad definitions.
|
|
|
@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 …
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@1611
|
9 years |
sacerdot |
All of Cminor now compiles with the latest lib of Matita.
|
|
|
@1610
|
9 years |
sacerdot |
Ported to new lib.
|
|
|
@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.
|
|
|
@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 …
|
|
|
@1464
|
9 years |
campbell |
Use unification hints to simplify the graph monotonicity proofs.
|
|
|
@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.
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
@1238
|
9 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
@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 …
|
|
|
@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 …
|
|
|
@1072
|
10 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
@1070
|
10 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
@1056
|
10 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
@966
|
10 years |
campbell |
Update Cminor pretty printer and some examples.
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@898
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
@888
|
10 years |
campbell |
Use simplified conditionals in RTLabs, following the prototype.
|
|
|
@887
|
10 years |
campbell |
Start bringing RTLabs into line with the prototype compiler:
- a …
|
|
|
@886
|
10 years |
campbell |
Put types into parameter and variable lists in Cminor.
Temporarily …
|
|
|
@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.
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
@790
|
10 years |
campbell |
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …
|
|
|
@780
|
10 years |
campbell |
Properly update set of registers that are used for pointers in Cminor …
|
|
|
@776
|
10 years |
campbell |
Fix up some minor null pointer issues in Clight.
Add corresponding …
|
|
|
@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 …
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
@760
|
10 years |
campbell |
Fix tailcall continuations in Cminor.
|
|
|