

@3263

6 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3145

7 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3037

7 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@3004

7 years 
tranquil 
fixed a bug where when doing an asymetrical op, cast initialization …



@2946

7 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2931

7 years 
sacerdot 
Partial backtrack from Paolo's commit, that was partial.



@2925

7 years 
tranquil 
corrected bug in toggle_bool



@2918

7 years 
tranquil 
erased stupid accidental paste at the start of file (happened when …



@2917

7 years 
tranquil 
made it so that a 0 offset does not generate adding ops when accessing …



@2916

7 years 
tranquil 
corrected yet another endianness bug in load and store



@2915

7 years 
sacerdot 
Dead code removed.



@2912

7 years 
sacerdot 
Ouch, another bug in the very same function.
Fixed too, on an example …



@2911

7 years 
sacerdot 
Bug fixed in the translation of casts.



@2866

7 years 
tranquil 
corrected two bugs of the translation: constant translation used wrong …



@2823

7 years 
tranquil 
* corrected bug in ERTL semantics (both delframe and newframe did the …



@2808

7 years 
tranquil 
added local_stacksize to joint internal functions to accomodate for …



@2774

7 years 
sacerdot 
1. the compiler now outputs both the stack cost model and the max …



@2689

7 years 
tranquil 
* fixed passes up to linearisation



@2674

7 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2640

7 years 
tranquil 
updated RTL and RTLabs to RTL translation



@2601

7 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2505

7 years 
mckinna 
Cleaned up compiler.ma; some refactoring/additional code needed in …



@2493

7 years 
mckinna 
Change in cst_well_defd to fix previously broken defn of …



@2490

7 years 
tranquil 
switched back to Byte immediate (instead of beval ones)
propagated …



@2290

7 years 
campbell 
Remove jump tables from RTLabs > RTL.



@2286

7 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2176

7 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2103

7 years 
campbell 
Make transform_*program take a more general transformation to make …



@2032

7 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1995

7 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1601

8 years 
sacerdot 
Files ported to new version of the standard library.



@1529

8 years 
campbell 
Update RTLabs to RTL with unary operation types.



@1521

8 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1515

8 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1408

8 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1358

8 years 
mulligan 
got rtlabs to rtl compiling, foldi_strong needs examining



@1356

8 years 
mulligan 
deleted redundant directory. added outlines for both reports, and …



@1354

8 years 
sacerdot 
One axiom closed.



@1352

8 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1343

8 years 
mulligan 
fixed some bugs in the translation



@1331

8 years 
mulligan 
some changes, but i now have two contradictory proof obligations.



@1325

8 years 
mulligan 
finished implementing the translate constant function



@1315

8 years 
mulligan 
another move for the same reason. got rtlabs > rtl compiling again by …



@1314

8 years 
mulligan 
name changes so that bash tab completion actually works with some …


copied from src/RTLabs/RTLAbstoRTL.ma:



@1308

8 years 
mulligan 
changes to translate_cst
