source: src/common @ 2435

Name Size Rev Age Author Last Change
../
Animation.ma 4.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
AssocList.ma 767 bytes 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
AST.ma 29.6 KB 2319   9 years campbell Generate per-program cost labels rather than per-function ones, and …
BackEndOps.ma 9.8 KB 2435   9 years tranquil new back end operations
ByteValues.ma 6.3 KB 2435   9 years tranquil new back end operations
CostLabel.ma 233 bytes 1268   10 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
Errors.ma 8.0 KB 1954   9 years campbell Initial state is in the labelling simulation (modulo global envs results).
Events.ma 10.8 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Executions.ma 8.7 KB 2338   9 years campbell Use much nicer definition for making several steps in the labelling …
Floats.ma 2.7 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
FrontEndMem.ma 2.0 KB 2429   9 years garnier Restrict semantics of pointer comparison to what CompCert? does - i.e. …
FrontEndOps.ma 22.5 KB 2432   9 years campbell Remove off-the-end pointers from front end ops.
FrontEndVal.ma 2.5 KB 2435   9 years tranquil new back end operations
GenMem.ma 7.3 KB 2332   9 years garnier Some progress on switch removal. Small fix in the definition of free, …
Globalenvs.ma 66.7 KB 2415   9 years campbell Add the ability to map blocks to symbols in preparation for stack space.
Graphs.ma 1.6 KB 1882   10 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Identifiers.ma 37.1 KB 2420   9 years campbell Tidy away generic results about folds on positive/identifier maps.
Integers.ma 77.6 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
IO.ma 2.6 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
IOMonad.ma 14.7 KB 2428   9 years campbell Tighten requirements on switch statements in Clight to only give …
LabelledObjects.ma 10.3 KB 2133   9 years boender - moved does_not_occur_occur_absurd
Order.ma 117 bytes 1049   10 years mulligan more stuff added
Pointers.ma 5.9 KB 2296   9 years campbell Tidy up some ill-placed definitions.
PositiveMap.ma 28.5 KB 2420   9 years campbell Tidy away generic results about folds on positive/identifier maps.
PreIdentifiers.ma 582 bytes 1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
Registers.ma 444 bytes 2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
Smallstep.ma 27.7 KB 1510   10 years sacerdot All files ported to new dependent inversion.
SmallstepExec.ma 9.6 KB 2338   9 years campbell Use much nicer definition for making several steps in the labelling …
StatusSimulation.ma 30.8 KB 2421   9 years tranquil added simulation of flat prefix, and comments to explain the code
StructuredTraces.ma 35.3 KB 2423   9 years tranquil as_classifier predicate → as_classify function as_call predicate from …
Values.ma 29.8 KB 2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
Note: See TracBrowser for help on using the repository browser.