|
|
|
@100
|
10 years |
mulligan |
More added to ASMInterpret.
|
|
|
|
@99
|
10 years |
mulligan |
Final clean-up
|
|
|
|
@98
|
10 years |
mulligan |
preliminary pretty-printing function (no usable output)
|
|
|
|
@97
|
10 years |
mulligan |
Move to polymorphic variants everywhere (scary...)
|
|
|
|
@96
|
10 years |
mulligan |
Tidying up repository.
|
|
|
|
@95
|
10 years |
mulligan |
fixed typing errors in ASMInterpret up to execute1.
|
|
|
|
@94
|
10 years |
sacerdot |
Minor comments.
|
|
|
|
@93
|
10 years |
mulligan |
Fixed INC DPTR to assert false.
|
|
|
|
@92
|
10 years |
mulligan |
Fixed physical interface file. Refactoring ASMInterface.
|
|
|
|
@91
|
10 years |
mulligan |
Finished porting/fix type errors in physical.
|
|
|
|
@90
|
10 years |
mulligan |
Ported physical.ml to be compatible with new bitvector code, started …
|
|
|
|
@89
|
10 years |
mulligan |
Fixed a really annoying bug in vect_to_int and int_to_vect
|
|
|
|
@88
|
10 years |
mulligan |
int_of_vect implemented.
|
|
|
|
@87
|
10 years |
mulligan |
Moved tentative to bit_vectors. Added .mli file.
|
|
|
|
@86
|
10 years |
mulligan |
Adding bit vector file.
|
|
|
|
@85
|
10 years |
mulligan |
Deleted Pretty.ml, as `pretty' functions have now been merged into …
|
|
|
|
@84
|
10 years |
mulligan |
Lots of work on tidying up code.
|
|
|
|
@83
|
10 years |
mulligan |
Lots of work done on tidying up code.
|
|
|
|
@82
|
10 years |
campbell |
Start of document about impact of 8051 memory model on C.
|
|
|
|
@81
|
10 years |
mulligan |
INC DPTR partially implemented.
|
|
|
|
@80
|
10 years |
mulligan |
ANL, ORL and XRL instructions implemented.
|
|
|
|
@79
|
10 years |
mulligan |
One of the ANL instruction combinations implemented.
|
|
|
|
@78
|
10 years |
mulligan |
LCALL implemented.
|
|
|
|
@77
|
10 years |
mulligan |
ACALL implemented.
|
|
|
|
@76
|
10 years |
mulligan |
MOVC instruction implemented.
|
|
|
|
@75
|
10 years |
mulligan |
AJMP implemented.
|
|
|
|
@74
|
10 years |
mulligan |
RETI instruction implemented.
|
|
|
|
@73
|
10 years |
mulligan |
RET instruction implemented.
|
|
|
|
@72
|
10 years |
mulligan |
DA instruction implemented: pretty complex!
|
|
|
|
@71
|
10 years |
mulligan |
Two more jump instructions implemented.
|
|
|
|
@70
|
10 years |
mulligan |
XCHD implemented.
|
|
|
|
@69
|
10 years |
mulligan |
PUSH implemented.
|
|
|
|
@68
|
10 years |
mulligan |
POP implemented ... at last.
|
|
|
|
@67
|
10 years |
mulligan |
DJNZ instruction finished.
|
|
|
|
@66
|
10 years |
mulligan |
Bytes mostly finished.
|
|
|
|
@65
|
10 years |
mulligan |
Forgot to add new file for processor.
|
|
|
|
@64
|
10 years |
mulligan |
More work on bits, bytes and nibbles.
|
|
|
|
@63
|
10 years |
mulligan |
More work on bits, bytes, nibbles, and added modules for byte7s and
words.
|
|
|
|
@62
|
10 years |
mulligan |
Many additions to Bit, Nibble and Byte API, as well as more …
|
|
|
|
@61
|
10 years |
sacerdot |
Final version.
|
|
|
|
@60
|
10 years |
mulligan |
Finished implementing all jump instructions.
|
|
|
|
@59
|
10 years |
sacerdot |
Added a new appendix for assessment within the CerCo? project.
|
|
|
|
@58
|
10 years |
mulligan |
Bug fixed in CJNE instruction. More jump instructions implemented.
|
|
|
|
@57
|
10 years |
mulligan |
More instructions implemented. Started cleaning up code by moving …
|
|
|
|
@56
|
10 years |
sacerdot |
The technical annex of the contract.
|
|
|
|
@55
|
10 years |
mulligan |
CJNE instruction finished.
|
|
|
|
@54
|
10 years |
mulligan |
CLR instructions implemented.
|
|
|
|
@53
|
10 years |
mulligan |
All RR* and RL* instructions implemented.
|
|
|
|
@52
|
10 years |
mulligan |
RL, RR and SWAP implemented.
|
|
|
|
@51
|
10 years |
mulligan |
NOP and SETB implemented.
|
|
|
|
@50
|
10 years |
mulligan |
More missing cases added to the ASMInterpret functions. Pretty …
|
|
|
|
@49
|
10 years |
mulligan |
Fixed bug in ASMInterpret functions: CPL functions were not …
|
|
|
|
@48
|
10 years |
mulligan |
finished touching up report's English
|
|
|
|
@47
|
10 years |
mulligan |
Half of report's English fixed.
|
|
|
|
@46
|
10 years |
mulligan |
MOV done.
|
|
|
|
@45
|
10 years |
mulligan |
More pretty stuff added.
|
|
|
|
@44
|
10 years |
mulligan |
Added pretty printing functions for bits, bytes, words etc.
|
|
|
|
@43
|
10 years |
mulligan |
Address1 function completed.
|
|
|
|
@42
|
10 years |
mulligan |
Address1 function completed for instructions A--M.
|
|
|
|
@41
|
10 years |
mulligan |
More added to address1 function. Weird type error?
|
|
|
|
@40
|
10 years |
amadio |
er-cor
|
|
|
|
@39
|
10 years |
amadio |
deliverable D2.1
|
|
|
|
@38
|
10 years |
mulligan |
First draft Claudio's talk finished.
|
|
|
|
@37
|
10 years |
mulligan |
Slight change to presentation.
|
|
|
|
@36
|
10 years |
mulligan |
More on Claudio's presentation: upto interrupts and their handling.
|
|
|
|
@35
|
10 years |
mulligan |
`fetch' function complete.
|
|
|
|
@34
|
10 years |
mulligan |
Up to describing 8051 SFRs in presentation
|
|
|
|
@33
|
10 years |
mulligan |
Instructions M--O added to `fetch' function. Presentation files for …
|
|
|
|
@32
|
10 years |
mulligan |
All MOV variations done.
|
|
|
|
@31
|
10 years |
mulligan |
Instructions J--M complete.
|
|
|
|
@30
|
10 years |
mulligan |
Small bug fix in abstract syntax of ASM language (JB needs to carry a …
|
|
|
|
@29
|
10 years |
mulligan |
Commit while I check Siemen's data sheet. Instructions C--J added to …
|
|
|
|
@28
|
10 years |
sacerdot |
1) all the opcodes are there in ASM syntax
(but no labels, …
|
|
|
|
@27
|
10 years |
sacerdot |
The 8051 instruction set (syntax only).
|
|
|
|
@26
|
10 years |
sacerdot |
Executable semantics of 8051 assembly (in OCaml for now).
|
|
|
|
@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 …
|
|
|
|
@23
|
10 years |
sacerdot |
Spell checked.
|
|
|
|
@22
|
10 years |
sacerdot |
Proposed final version.
|
|
|
|
@21
|
10 years |
sacerdot |
First draft.
|
|
|
|
@20
|
10 years |
campbell |
Add resumption monad based version of the executable semantics with …
|
|
|
|
@19
|
10 years |
sacerdot |
…
|
|
|
|
@18
|
10 years |
sacerdot |
logo moved
|
|
|
|
@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 not-quite-trivial …
|
|
|
|
@8
|
10 years |
sacerdot |
Final version of D6.1.
|
|
|
|
@7
|
10 years |
sacerdot |
ispelled
|
|
|
|
@6
|
10 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 work-in-progress port of the CompCert? C semantics to matita.
|
|
|
|
@2
|
10 years |
sacerdot |
First layout.
|
|
|
|
@1
|
10 years |
puech |
This is a test
|
