

@60

9 years 
mulligan 
Finished implementing all jump instructions.



@59

9 years 
sacerdot 
Added a new appendix for assessment within the CerCo? project.



@58

9 years 
mulligan 
Bug fixed in CJNE instruction. More jump instructions implemented.



@57

9 years 
mulligan 
More instructions implemented. Started cleaning up code by moving …



@56

9 years 
sacerdot 
The technical annex of the contract.



@55

9 years 
mulligan 
CJNE instruction finished.



@54

9 years 
mulligan 
CLR instructions implemented.



@53

9 years 
mulligan 
All RR* and RL* instructions implemented.



@52

9 years 
mulligan 
RL, RR and SWAP implemented.



@51

9 years 
mulligan 
NOP and SETB implemented.



@50

9 years 
mulligan 
More missing cases added to the ASMInterpret functions. Pretty …



@49

9 years 
mulligan 
Fixed bug in ASMInterpret functions: CPL functions were not …



@48

9 years 
mulligan 
finished touching up report's English



@47

9 years 
mulligan 
Half of report's English fixed.



@46

9 years 
mulligan 
MOV done.



@45

9 years 
mulligan 
More pretty stuff added.



@44

9 years 
mulligan 
Added pretty printing functions for bits, bytes, words etc.



@43

9 years 
mulligan 
Address1 function completed.



@42

9 years 
mulligan 
Address1 function completed for instructions AM.



@41

9 years 
mulligan 
More added to address1 function. Weird type error?



@40

9 years 
amadio 
ercor



@39

9 years 
amadio 
deliverable D2.1



@38

9 years 
mulligan 
First draft Claudio's talk finished.



@37

9 years 
mulligan 
Slight change to presentation.



@36

9 years 
mulligan 
More on Claudio's presentation: upto interrupts and their handling.



@35

9 years 
mulligan 
`fetch' function complete.



@34

9 years 
mulligan 
Up to describing 8051 SFRs in presentation



@33

9 years 
mulligan 
Instructions MO added to `fetch' function. Presentation files for …



@32

9 years 
mulligan 
All MOV variations done.



@31

9 years 
mulligan 
Instructions JM complete.



@30

9 years 
mulligan 
Small bug fix in abstract syntax of ASM language (JB needs to carry a …



@29

9 years 
mulligan 
Commit while I check Siemen's data sheet. Instructions CJ added to …



@28

9 years 
sacerdot 
1) all the opcodes are there in ASM syntax
(but no labels, …



@27

9 years 
sacerdot 
The 8051 instruction set (syntax only).



@26

9 years 
sacerdot 
Executable semantics of 8051 assembly (in OCaml for now).



@25

9 years 
campbell 
Simplify the IO monad a little.



@24

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



@23

9 years 
sacerdot 
Spell checked.



@22

9 years 
sacerdot 
Proposed final version.



@21

9 years 
sacerdot 
First draft.



@20

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



@19

9 years 
sacerdot 
…



@18

9 years 
sacerdot 
logo moved



@17

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



@16

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



@15

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



@14

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



@13

9 years 
campbell 
Minor syntactic changes.



@12

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



@11

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



@10

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



@9

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



@8

9 years 
sacerdot 
Final version of D6.1.



@7

9 years 
sacerdot 
ispelled



@6

9 years 
sacerdot 
First deliverable (D6.1).



@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.



@2

10 years 
sacerdot 
First layout.



@1

10 years 
puech 
This is a test
