|
../
|
|
ASM
|
|
2910
|
7 years
|
sacerdot |
Abstract statuses for ASM and OC completed.
A simple test program can …
|
|
Clight
|
|
2877
|
7 years
|
garnier |
Correction of a bug in my former bug correction.
|
|
Cminor
|
|
2936
|
7 years
|
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
common
|
|
2927
|
7 years
|
tranquil |
stupid bug in bool_of_beval
|
|
ERTL
|
|
2898
|
7 years
|
piccolo |
1) simplification of cond and seq case for StatusSimulationHelper? …
|
|
ERTLptr
|
|
2930
|
7 years
|
sacerdot |
More progress. Some useless parameters have been removed from the …
|
|
joint
|
|
2932
|
7 years
|
sacerdot |
Same comment as previous commit on this file: the previous commit was …
|
|
LIN
|
|
2837
|
7 years
|
tranquil |
* filled in evaluation of LTL/LIN's extended instrucitons
|
|
LTL
|
|
2858
|
7 years
|
sacerdot |
Trying to pretty print the code graph in visit order.
Slightly bugged …
|
|
RTL
|
|
2935
|
7 years
|
tranquil |
separation of RTL semantics in three different versions, and …
|
|
RTLabs
|
|
2936
|
7 years
|
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
utilities
|
|
2897
|
7 years
|
campbell |
Minor tidying.
|
|
acc-matita-printers.patch
|
7.1 KB
|
1633
|
8 years
|
campbell |
Update Cminor pretty printer and examples.
|
|
BACKEND_BROKEN_FILES
|
713 bytes
|
2754
|
7 years
|
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
CHANGES
|
3.4 KB
|
1388
|
8 years
|
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
compiler.ma
|
5.4 KB
|
2936
|
7 years
|
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
correctness.ma
|
7.6 KB
|
2928
|
7 years
|
tranquil |
some sketches about correctness proof
|
|
Makefile
|
439 bytes
|
2919
|
7 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
redundant_includes.txt
|
6.8 KB
|
2919
|
7 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
root
|
26 bytes
|
703
|
9 years
|
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
semantics.ma
|
2.8 KB
|
2905
|
7 years
|
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
TODO
|
606 bytes
|
1457
|
8 years
|
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
