

@160

10 years 
campbell 
Patch to acc to parse 8051 memory spaces and output matita terms.



@157

10 years 
campbell 
Make proposed memory spaces semantics more explicit.



@156

10 years 
campbell 
pdata support



@155

10 years 
campbell 
More sensible handling of integer types and pointer casts.



@154

10 years 
campbell 
Minor test case changes



@153

10 years 
campbell 
Use appropriate memory chunks for 8051 pointers.



@152

10 years 
campbell 
Force whd form for memory during execution



@149

10 years 
campbell 
Fill in a few details about 8051 extensions.



@127

10 years 
campbell 
Allow the storage of pointers in suitably large integers.



@126

10 years 
campbell 
Put in real pointer sizes.



@125

10 years 
campbell 
Unify memory space / pointer types.
Implement global variable …



@124

10 years 
campbell 
Initial work on Clight semantics with 8051 memory spaces.



@94

10 years 
sacerdot 
Minor comments.



@82

10 years 
campbell 
Start of document about impact of 8051 memory model on C.



@25

10 years 
campbell 
Simplify the IO monad a little.



@24

10 years 
campbell 
Separate out IOMonad from the rest of the executable semantics.
Start …



@20

10 years 
campbell 
Add resumption monad based version of the executable semantics with …



@17

10 years 
campbell 
Remainder of the statements for the executable semantics (except for …



@16

10 years 
campbell 
Add rest of the expressions to executable Clight semantics.



@15

10 years 
campbell 
Make some definitions more normalization friendly by a little 'nlet …



@14

10 years 
campbell 
Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.



@13

10 years 
campbell 
Minor syntactic changes.



@12

10 years 
campbell 
Make memory model tests more readable.
Update README.



@11

10 years 
campbell 
Fill in some axioms to aid executablity.
Implement global variable …



@10

10 years 
campbell 
Add binary arithmetic libraries, use for integers and identifiers (but …



@9

10 years 
campbell 
Enough of an executable semantics to execute a notquitetrivial …



@5

10 years 
campbell 
Add a few execution steps and calculation of the initial state to the …



@4

10 years 
campbell 
Some experimental work on executable Clight semantics.



@3

10 years 
campbell 
Import workinprogress port of the CompCert? C semantics to matita.
