

@1661

8 years 
amadio 
rev



@1660

8 years 
ayache 
Deliverable: FramaC plugin (D5.15.3)



@1659

8 years 
amadio 



@1657

8 years 
amadio 
preliminary version of D5



@1635

8 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1590

8 years 
tranquil 
* got back to previous implementation of multiplication in RTLabs > …



@1589

8 years 
tranquil 
* turned to argumentless return statements for RTLabs and RTL (there …



@1585

8 years 
tranquil 
fighting with a bug of the translation from RTL to ERTL



@1584

8 years 
tranquil 
* new form of translation written in graphUtilites (mainly as a test …



@1580

8 years 
tranquil 
implemented constant propagation in LTL
cleaned up translations in …



@1572

8 years 
tranquil 
* corrected previous bug
* finished propagating immediates



@1569

8 years 
tranquil 
* added in repository some missing files…



@1568

8 years 
tranquil 
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …



@1546

8 years 
tranquil 
added an option to prevent reindexing transformations from taking …



@1543

8 years 
tranquil 
deletion of indexed labels branch



@1542

8 years 
tranquil 
merge of indexed labels branch



@1539

8 years 
tranquil 
branch up to date



@1525

8 years 
ayache 
D2.2: function pointers using JMP.



@1508

8 years 
tranquil 
branched a version of the plugin that is compatible with the indexed …



@1507

8 years 
tranquil 
* added an option to not use ternary expressions in costs, to …



@1505

8 years 
ayache 
D2.2: addendum on 16 and 32 bits integer and function pointers support.



@1504

8 years 
ayache 
8051 ocaml: bug fix in the labelling of dowhiles.



@1492

8 years 
ayache 
Comment in D2.2 > LINToASM about function pointers.



@1491

8 years 
ayache 
Function pointers good and working.



@1490

8 years 
ayache 
Function pointers fixed.



@1488

8 years 
ayache 
Function pointers in D2.2/8051. Bugged for now.



@1483

8 years 
tranquil 
* implemented a first draft of loop unrolling
* correced bugs in CostExpr?



@1477

8 years 
tranquil 
* corrected a bug
* implemented copy propagation
* enhanced constant …



@1473

8 years 
tranquil 
* implemented partial redundancy elimination
* added some tools for …



@1468

8 years 
tranquil 
* implemented constant propagation
* implementing partial redundancy …



@1462

8 years 
ayache 
Added D5.1: FramaC plugin and Lustre wrapper. D2.2 (8051) has been …



@1456

8 years 
mulligan 
changed type of pointer_of_label in report



@1455

8 years 
mulligan 
ratios changed



@1454

8 years 
mulligan 
removed mention of axiomatised code in LIN/semantics.ma



@1449

8 years 
mulligan 
finished d4.3



@1448

8 years 
mulligan 
finished columns in d4.2 report



@1447

8 years 
mulligan 
changes to columns in tables



@1446

8 years 
sacerdot 
…



@1445

8 years 
mulligan 
o'caml sizes done for first table



@1444

8 years 
tranquil 
* expression simplification finished



@1443

8 years 
mulligan 
sizes added



@1442

8 years 
mulligan 
changes fixing wrong deletion of conflicts



@1441

8 years 
mulligan 
small change



@1440

8 years 
mulligan 
ratios fixed



@1439

8 years 
sacerdot 
…



@1438

8 years 
mulligan 
changed claudio's english, added bib file



@1437

8 years 
sacerdot 
…



@1436

8 years 
sacerdot 
…



@1435

8 years 
sacerdot 
More on dependent types. One citation is missing.



@1434

8 years 
mulligan 
chages to typesetting and some wording changes



@1433

8 years 
tranquil 
* added infrastructure to add samelanguage transformations along the …



@1432

8 years 
mulligan 
finished d4.2 report



@1428

8 years 
mulligan 
finished d4.3 report



@1427

8 years 
mulligan 
more added to d4.3 report



@1422

8 years 
tranquil 
corrected a small bug



@1421

8 years 
tranquil 
first draft of peeling optimization:
* a framework for heuristics has …



@1420

8 years 
mulligan 
more changes



@1418

8 years 
mulligan 
correct ratios for semantics calculated



@1414

8 years 
mulligan 
more added



@1413

8 years 
mulligan 
a lot more added, including updated parameters based on csc's recent submit



@1409

8 years 
mulligan 
added more to appendix discussing code



@1407

8 years 
mulligan 
almost finished



@1406

8 years 
mulligan 
a little more



@1405

8 years 
mulligan 
yet more added. apparently there's more parameters than i ever …



@1403

8 years 
mulligan 
more added



@1402

8 years 
mulligan 
more added



@1400

8 years 
mulligan 
more added on parameters



@1399

8 years 
mulligan 
more work on parameters



@1398

8 years 
mulligan 
more work on parameters



@1397

8 years 
mulligan 
more changes, talking about parameters



@1394

8 years 
mulligan 
reconfiguring of tables, and recalculation of ratios



@1392

8 years 
tranquil 
fiddling with Cminor: elimination of loops, blocks and exits



@1391

8 years 
mulligan 
more added



@1375

8 years 
mulligan 
changes, fixing typos etc



@1374

8 years 
mulligan 
added note about cfgs



@1373

8 years 
mulligan 
changes to file based on claudio's suggestions



@1370

8 years 
campbell 
D3.3: Added a subsection on the SmallstepExec?.ma definitions, plus a …



@1366

8 years 
mulligan 
added connections with other languages to d4.3 report, also fixed …



@1365

8 years 
mulligan 
changed description of task in 4.2 report.
added outline and …



@1364

8 years 
mulligan 
finished the report on d4.2. starting d4.3 report



@1362

8 years 
mulligan 
d42 report almost complete



@1361

8 years 
mulligan 
more changes



@1360

8 years 
mulligan 
added more on use of dependent types, and also discussing the …



@1357

8 years 
tranquil 
* changed implementation of constant indexings with extensible arrays …



@1356

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



@1349

8 years 
tranquil 
* work on LIN completed
* small implementation of extensible arrays



@1346

8 years 
campbell 
Minor corrections and a paragraph of context in the abstract to …



@1345

8 years 
tranquil 
work on ERTL and LTL completed



@1340

8 years 
tranquil 
work on RTLabs and RTL completed



@1334

8 years 
tranquil 
work on Cminor completed



@1328

8 years 
tranquil 
* bug in ClightUtilities?.find_max_depth_lbld fixed
* singleentry loop …



@1319

8 years 
tranquil 
indexing branch is compiling again:
* clight interpreter updated
* …



@1317

8 years 
campbell 
Fix listings in D3.2/D3.3.



@1311

8 years 
campbell 
Merge trunk to invariants branch, sorting out the handling of …



@1310

8 years 
tranquil 
* finished changes on annotator
* implementing indexes in interpreter



@1305

8 years 
tranquil 
added indexes to loop constructors. Branch does not compile atm



@1297

8 years 
tranquil 
changed representation of indexings to a nameless one implemented with …



@1291

8 years 
tranquil 
Started branch of untrusted compiler with indexed labels
* added …



@1277

8 years 
campbell 
Runtime functions and conclusion for D3.2.



@1273

8 years 
campbell 
Remove generated file.


