|
|
@2984
|
8 years |
tranquil |
better LINToASM initialization of globals (to be tested!)
|
|
|
@2978
|
8 years |
tranquil |
merged accidentally backtracked changes
|
|
|
@2976
|
8 years |
tranquil |
* a dangling trivial proof obligation is now closed
|
|
|
@2975
|
8 years |
tranquil |
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …
|
|
|
@2969
|
8 years |
sacerdot |
Dead axiom removed :-)
|
|
|
@2963
|
8 years |
sacerdot |
Bug fixed: the pre-main for the final code is now
COST k1
…
|
|
|
@2956
|
8 years |
tranquil |
fixed LTL/LIN semantics
|
|
|
@2952
|
8 years |
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
@2837
|
8 years |
tranquil |
* filled in evaluation of LTL/LIN's extended instrucitons
|
|
|
@2830
|
8 years |
sacerdot |
Added abstractions in front of cases daemon for code extraction.
|
|
|
@2783
|
8 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
@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 …
|
|
|
@2760
|
8 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
@2754
|
8 years |
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
|
@2708
|
8 years |
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2537
|
8 years |
tranquil |
rolled back changes on calls in joint. Now the save_frame parameter …
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
@2443
|
8 years |
tranquil |
changed joint's stack pointer and internal stack
|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
@2233
|
9 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
@2182
|
9 years |
tranquil |
updated linearisation pass
|
|
|
@2174
|
9 years |
tranquil |
* factored out script for (axiomatised) fixpoint computation
* ERTL → …
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
@1522
|
9 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
@1520
|
9 years |
campbell |
Generate cost labels with correct type.
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
@1415
|
9 years |
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
|
@1411
|
9 years |
sacerdot |
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
|
|
|
@1408
|
9 years |
sacerdot |
1. Added joint/BEGlobalenvs that is a modification of …
|
|
|
@1390
|
9 years |
sacerdot |
All fetch_result implementations have been factorized out, leaving …
|
|
|
@1386
|
9 years |
sacerdot |
Structure of semantic parameters simplified.
|
|
|
@1385
|
9 years |
sacerdot |
1. fetch_result and pop_frame now takes the genv in input
2. …
|
|
|
@1384
|
9 years |
sacerdot |
* fetch_ra taken out of pop_frame again since it is used uniformly and …
|
|
|
@1383
|
9 years |
sacerdot |
Potential bug fixed and bug found: the way pointers and labels are put …
|
|
|
@1382
|
9 years |
sacerdot |
- succ_pc generalized to return a res (necessary for LIN semantics)
- …
|
|
|
@1380
|
9 years |
sacerdot |
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
|
|
|
@1379
|
9 years |
sacerdot |
Invariant on LIN code removed. In Paris it was decided that a simpler …
|
|
|
@1378
|
9 years |
sacerdot |
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …
|
|
|
@1377
|
9 years |
sacerdot |
pop_frame now incorporates the fetch_result (that made sense only for …
|
|
|
@1372
|
9 years |
sacerdot |
save_frame now takes the stacksize to allow RTL to allocate the stack frame
|
|
|
@1371
|
9 years |
sacerdot |
save_frame changed to accept also the formal/actual argument pairs, …
|
|
|
@1359
|
9 years |
sacerdot |
1. more work on the RTL semantics
2. changes to joint/semantics to …
|
|
|
@1324
|
9 years |
sacerdot |
The semantics of extended statements must also consider the label …
|
|
|
@1312
|
9 years |
sacerdot |
Type of frame operations (pop_frame/save_frame) generalized to take in …
|
|
|
@1304
|
9 years |
sacerdot |
Work in progress.
|
|
|
@1282
|
9 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
@1281
|
9 years |
sacerdot |
Porting of all transformation to the joint syntax practically …
|
|
|
@1275
|
9 years |
sacerdot |
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …
|
|
|
@1270
|
9 years |
sacerdot |
Making RTL syntax an instance of Joint.
|
|
|
@1268
|
9 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
@1264
|
9 years |
sacerdot |
Almost ported to new Joint syntax.
|
|
|
@1250
|
9 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
@1246
|
9 years |
sacerdot |
Yet another change to Joint.ma to accomodate all passes.
The concrete …
|
|
|
@1245
|
9 years |
sacerdot |
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
|
|
|
@1236
|
9 years |
sacerdot |
LTLToLin.ma completed (up to a couple of daemons used to provide dead …
|
|
|
@1233
|
9 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
@1183
|
10 years |
mulligan |
removed parameterised label types in the three lowest level languages
|
|
|
@1179
|
10 years |
mulligan |
changes to ertl, ltl and lin to use new notion of joint params. ertl …
|
|
|
@1171
|
10 years |
mulligan |
changes made on claudio's request: changed order of nesting in the …
|
|
|
@1168
|
10 years |
sacerdot |
Joint statements parameterized over a record.
|
|
|
@1167
|
10 years |
mulligan |
…
|
|
|
@1166
|
10 years |
mulligan |
moved joint ltl lin files into their own directory. more changes to …
|
|
|
@1164
|
10 years |
mulligan |
ltl to lin working again, more changes to joint syntax
|
|
|
@1163
|
10 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
@1161
|
10 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
@1149
|
10 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
@1132
|
10 years |
mulligan |
reunified ltl and lin instruction type, removing lifting in ltl and …
|
|
|
@1112
|
10 years |
mulligan |
got lin > asm stuff working
|
|
|
@1110
|
10 years |
mulligan |
changes to get ltl to lin pass to work properly
|
|
|
@1108
|
10 years |
mulligan |
changes to get ertltoltli to compile
|
|
|
@1089
|
10 years |
mulligan |
more changes from earlier in the week
|
|
|
@1082
|
10 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
@734
|
10 years |
mulligan |
Fixed lin2asm.
|
|
|
@733
|
10 years |
mulligan |
Fixed partial commit.
|
|
|
@723
|
10 years |
mulligan |
Added dependent type internalising the invariant that LIN function …
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
@699
|
10 years |
mulligan |
More or less finished formalisation of LIN.
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
@696
|
10 years |
mulligan |
Added missing I8051 file and completed most of LIN formalisation.
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
|
copied from Deliverables/D4.2-4.3/LIN:
|
|
|
@491
|
10 years |
mulligan |
Initial commit of (part)-formalisation of LIN intermediate language.
|