

@177

11 years 
campbell 
Missing cost labels file.



@176

11 years 
campbell 
Remove old executable semantics without I/O.



@175

11 years 
campbell 
Add cost labels, with the semantics that the label is added to the …



@174

11 years 
campbell 
Add a form of nonterminating functional semantics.



@173

11 years 
campbell 
Minor changes for newer versions of matita.



@160

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



@157

11 years 
campbell 
Make proposed memory spaces semantics more explicit.



@156

11 years 
campbell 
pdata support



@155

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



@154

11 years 
campbell 
Minor test case changes



@153

11 years 
campbell 
Use appropriate memory chunks for 8051 pointers.



@152

11 years 
campbell 
Force whd form for memory during execution



@149

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



@127

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



@126

11 years 
campbell 
Put in real pointer sizes.



@125

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



@124

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



@94

11 years 
sacerdot 
Minor comments.



@82

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



@25

11 years 
campbell 
Simplify the IO monad a little.



@24

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



@20

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



@17

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



@16

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



@15

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



@14

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



@13

11 years 
campbell 
Minor syntactic changes.



@12

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



@11

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



@10

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



@9

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



@5

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



@4

11 years 
campbell 
Some experimental work on executable Clight semantics.



@3

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