|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2936
|
8 years |
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
|
|
@2907
|
8 years |
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
|
|
@2899
|
8 years |
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
|
@2841
|
8 years |
sacerdot |
The compiler now computes also the stack cost for every intermediate …
|
|
|
|
@2835
|
8 years |
sacerdot |
Included Uses.ma which is required by the untrusted code.
The …
|
|
|
|
@2828
|
8 years |
sacerdot |
1. New semantics.ma file that puts together all semantics.
It …
|
|
|
|
@2794
|
8 years |
mckinna |
Minor tweaks/tidying up
|
|
|
|
@2774
|
8 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
|
@2767
|
8 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|
|
@2763
|
8 years |
sacerdot |
All daemons in compiler.ma closed (i.e. proof obligations added
to the …
|
|
|
|
@2762
|
8 years |
sacerdot |
All repaired up to compiler.ma.
Note: one daemon is left for one …
|
|
|
|
@2754
|
8 years |
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
|
|
@2753
|
8 years |
mckinna |
Further tidying up thanks to Claudio's strong_decidable intervention; …
|
|
|
|
@2752
|
8 years |
mckinna |
Fixed TODO regarding length of list_instr
Added ASM/CodeMemory.ma to …
|
|
|
|
@2745
|
8 years |
sacerdot |
1. Complexity of policy computation lowered from O(n2) to O(n)
2. …
|
|
|
|
@2724
|
8 years |
campbell |
Add RTLabs cost labelling checks to compiler.ma.
|
|
|
|
@2709
|
8 years |
sacerdot |
LINToAsm repaired
|
|
|
|
@2705
|
8 years |
sacerdot |
More progress in ASM towards implementing the new pseudoinstructions.
|
|
|
|
@2702
|
8 years |
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
|
|
@2700
|
8 years |
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
|
|
@2697
|
8 years |
sacerdot |
Compiler fixed to include the ERTLptrToLTL pass.
|
|
|
|
@2693
|
8 years |
sacerdot |
1. Stuff moved to correct places.
2. ERTLptr pass added
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2581
|
8 years |
mckinna |
commented out back end entirely until knock-on effects of changes to …
|
|
|
|
@2512
|
8 years |
mckinna |
Simplified dependencies on ASM, to allow rollback to when …
|
|
|
|
@2508
|
8 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
|
@2505
|
8 years |
mckinna |
Cleaned up compiler.ma; some refactoring/additional code needed in …
|
|
|
|
@2497
|
8 years |
mckinna |
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
|
|
|
|
@2494
|
8 years |
mckinna |
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
|
|
|
|
@2492
|
8 years |
campbell |
Reduce axiomatisation in compiler.ma.
|
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
|
@2399
|
9 years |
campbell |
Fill in some details about the statement of correctness.
|
|
|
|
@2320
|
9 years |
campbell |
Update compiler and correctness with labelling changes.
|
|
|
|
@2319
|
9 years |
campbell |
Generate per-program cost labels rather than per-function ones, and …
|
|
|
|
@2291
|
9 years |
campbell |
Disable switch removal in compiler.ma for now.
|
|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2253
|
9 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
|
@2205
|
9 years |
campbell |
Get correctness.ma type checking again.
|
|
|
|
@2116
|
9 years |
sacerdot |
load_code_memory will be moved into Fetch.ma in the next commit.
This …
|
|
|
|
@2019
|
9 years |
campbell |
Split out special induction principle for Clight from soundness file. …
|
|
|
|
@2001
|
9 years |
campbell |
Get the compiler to output more.
|
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
|
@1991
|
9 years |
campbell |
Put the front end transformations together and make an example use it.
|
