|
|
|
@46
|
11 years |
mulligan |
MOV done.
|
|
|
|
@45
|
11 years |
mulligan |
More pretty stuff added.
|
|
|
|
@44
|
11 years |
mulligan |
Added pretty printing functions for bits, bytes, words etc.
|
|
|
|
@43
|
11 years |
mulligan |
Address1 function completed.
|
|
|
|
@42
|
11 years |
mulligan |
Address1 function completed for instructions A--M.
|
|
|
|
@41
|
11 years |
mulligan |
More added to address1 function. Weird type error?
|
|
|
|
@40
|
11 years |
amadio |
er-cor
|
|
|
|
@39
|
11 years |
amadio |
deliverable D2.1
|
|
|
|
@38
|
11 years |
mulligan |
First draft Claudio's talk finished.
|
|
|
|
@37
|
11 years |
mulligan |
Slight change to presentation.
|
|
|
|
@36
|
11 years |
mulligan |
More on Claudio's presentation: upto interrupts and their handling.
|
|
|
|
@35
|
11 years |
mulligan |
`fetch' function complete.
|
|
|
|
@34
|
11 years |
mulligan |
Up to describing 8051 SFRs in presentation
|
|
|
|
@33
|
11 years |
mulligan |
Instructions M--O added to `fetch' function. Presentation files for …
|
|
|
|
@32
|
11 years |
mulligan |
All MOV variations done.
|
|
|
|
@31
|
11 years |
mulligan |
Instructions J--M complete.
|
|
|
|
@30
|
11 years |
mulligan |
Small bug fix in abstract syntax of ASM language (JB needs to carry a …
|
|
|
|
@29
|
11 years |
mulligan |
Commit while I check Siemen's data sheet. Instructions C--J added to …
|
|
|
|
@28
|
11 years |
sacerdot |
1) all the opcodes are there in ASM syntax
(but no labels, …
|
|
|
|
@27
|
11 years |
sacerdot |
The 8051 instruction set (syntax only).
|
|
|
|
@26
|
11 years |
sacerdot |
Executable semantics of 8051 assembly (in OCaml for now).
|
|
|
|
@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 …
|
|
|
|
@23
|
11 years |
sacerdot |
Spell checked.
|
|
|
|
@22
|
11 years |
sacerdot |
Proposed final version.
|
|
|
|
@21
|
11 years |
sacerdot |
First draft.
|
|
|
|
@20
|
11 years |
campbell |
Add resumption monad based version of the executable semantics with …
|
|
|
|
@19
|
11 years |
sacerdot |
…
|
|
|
|
@18
|
11 years |
sacerdot |
logo moved
|
|
|
|
@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 not-quite-trivial …
|
|
|
|
@8
|
11 years |
sacerdot |
Final version of D6.1.
|
|
|
|
@7
|
11 years |
sacerdot |
ispelled
|
|
|
|
@6
|
11 years |
sacerdot |
First deliverable (D6.1).
|
|
|
|
@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 work-in-progress port of the CompCert? C semantics to matita.
|
|
|
|
@2
|
11 years |
sacerdot |
First layout.
|
|
|
|
@1
|
11 years |
puech |
This is a test
|
