source: src/common @ 767

Name Size Rev Age Author Last Change
../
Registers.ma 481 bytes 757   10 years mulligan Lots more fixing to get both front and backends using same conventions …
Graphs.ma 305 bytes 746   10 years mulligan Changes to bitvectortrieset: equality on sets. Added new file for …
CostLabel.ma 336 bytes 757   10 years mulligan Lots more fixing to get both front and backends using same conventions …
Values.ma 34.5 KB 751   10 years campbell Initial version of the Cminor syntax and semantics.
SmallstepExec.ma 4.5 KB 751   10 years campbell Initial version of the Cminor syntax and semantics.
Smallstep.ma 27.7 KB 700   10 years campbell Get Clight semantics going again (except for problems CexecEquiv? that …
Mem.ma 114.1 KB 744   10 years campbell Evict Coq-style integers from common/Integers.ma. Make more bitvector …
Maps.ma 42.2 KB 747   10 years campbell Merge the two AST files together (although some definitions still need …
IOMonad.ma 8.3 KB 700   10 years campbell Get Clight semantics going again (except for problems CexecEquiv? that …
IO.ma 2.2 KB 731   10 years campbell Common definition for animation semantics, and factor out IO definitions.
Integers.ma 77.6 KB 747   10 years campbell Merge the two AST files together (although some definitions still need …
Identifiers.ma 2.7 KB 761   10 years campbell Enforce the use of declared identifiers/registers in Cminor/RTLabs.
Globalenvs.ma 51.3 KB 758   10 years campbell Implement replacement of global var initialisation data by code in Cminor.
FrontEndOps.ma 15.1 KB 744   10 years campbell Evict Coq-style integers from common/Integers.ma. Make more bitvector …
Floats.ma 2.6 KB 700   10 years campbell Get Clight semantics going again (except for problems CexecEquiv? that …
Events.ma 10.7 KB 720   10 years campbell Sort out cost labels.
Errors.ma 8.5 KB 764   10 years campbell Start Cminor to RTLabs phase. Includes some syntax for matching …
AST.ma 17.2 KB 764   10 years campbell Start Cminor to RTLabs phase. Includes some syntax for matching …
Animation.ma 2.5 KB 731   10 years campbell Common definition for animation semantics, and factor out IO definitions.
Note: See TracBrowser for help on using the repository browser.