|
../
|
|
Clight
|
|
3021
|
8 years
|
campbell |
Replace clight_clock_after with a more sensible definition that uses …
|
|
Cminor
|
|
3007
|
8 years
|
campbell |
Sketch out how Cminor to RTLabs correctness would fit into the …
|
|
common
|
|
3007
|
8 years
|
campbell |
Sketch out how Cminor to RTLabs correctness would fit into the …
|
|
RTLabs
|
|
3022
|
8 years
|
campbell |
Make a couple of tests monadic for easier inversion.
|
|
ASM
|
|
3024
|
8 years
|
sacerdot |
Bug fixed: set_flags was ignoring the cy and ov flags.
|
|
ERTL
|
|
3018
|
8 years
|
sacerdot |
1) some files repaired
2) all stuff related to the aborted pass …
|
|
ERTLptr
|
|
3018
|
8 years
|
sacerdot |
1) some files repaired
2) all stuff related to the aborted pass …
|
|
LIN
|
|
3023
|
8 years
|
sacerdot |
Typo fixed. It made all GOTOs jump to random positions in the ASM code.
|
|
utilities
|
|
2949
|
8 years
|
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
joint
|
|
3014
|
8 years
|
tranquil |
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
|
|
LTL
|
|
2952
|
8 years
|
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
RTL
|
|
2975
|
8 years
|
tranquil |
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …
|
|
acc-matita-printers.patch
|
7.1 KB
|
1633
|
9 years
|
campbell |
Update Cminor pretty printer and examples.
|
|
compiler.ma
|
5.4 KB
|
3022
|
8 years
|
campbell |
Make a couple of tests monadic for easier inversion.
|
|
correctness.ma
|
7.3 KB
|
3022
|
8 years
|
campbell |
Make a couple of tests monadic for easier inversion.
|
|
Makefile
|
439 bytes
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
redundant_includes.txt
|
6.8 KB
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
BACKEND_BROKEN_FILES
|
713 bytes
|
2754
|
8 years
|
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
CHANGES
|
3.4 KB
|
1388
|
10 years
|
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
root
|
26 bytes
|
703
|
10 years
|
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
TODO
|
606 bytes
|
1457
|
9 years
|
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
semantics.ma
|
2.7 KB
|
3014
|
8 years
|
tranquil |
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
|
