Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • master default protected
1 result
Created with Raphaël 2.2.09Dec29Nov17161096543229Oct28272622211513765130Sep27232120148725Aug29Jul52130Jun2928251817161514434May26Apr222120161229Mar252219181098119Feb161585326Jan2117Nov16Jul9212Mar27Jan9Dec20Nov18146518Jul171615121110865439May29Apr1916115422Mar211816151413121126Feb25212019181413121123Nov22212016151413121110984324Oct198525Sep242114133Aug23Jul1312422Jun211512118131May3029201817161574318Apr76330Mar292814913Feb131Jan3018171621Dec1918141312628Nov1514913Oct121110653226Sep252322211527Jul2120181714131210876330Jun27262322only requires seal package for lustrev[TODO] add some points from discussionsremove unused functionremove behavior-based contracts for clear_resetignore FIREFLY* testsindicate already failed testsindicate already verified testsread failed section in testsfix testsupdate docker with re library and tokeichange shell test by a magnificent OCaml testfix optimizationsdo not remove spec of removed assignments by optimunused vars have to be computed from both outputs AND state vars!do not run all proversadd timeout to testsremove testreplace ghost vars by universal vars in contractsfix testsignore some testsignore DRAGON* testsremove testmove asserts eqs at the end to respect dependenciesdo not eliminate vars in transitions defs but eliminate constantsadd integer casts in ACSLsince the df optim backward optim has been disabled, elimination is in a fixpoint now so elim chains are taken into accountadd ignored tests possibilityreplace the Reset: label by a ghost variableuse ghost variables instead of existential variables to avoid read / write capture problems with variable reusegenerate existential vars to handle reuse optimizationfix dependencies calculus not depending on instances in Machinefix spec optimization by variable reusefix errors in elimination optimization and dependencies calculus in Machine codedisable retro-elimination of dataflows after Machine optimdo not optimize too much the spec, as we want to keep the link with the dataflow nodenormalize existentials in ACSL (seems easier for solvers)remove unused variables after tag elimination in machine code (-O >= 3)remove debug linefix optimization for variable reuse that was not propagated in branchesstate variables ar not free