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.03Nov229Oct28272622211513765130Sep27232120148725Aug29Jul52130Jun2928251817161514434May26Apr222120161229Mar252219181098119Feb161585326Jan2117Nov16Jul9212Mar27Jan9Dec20Nov18146518Jul171615121110865439May29Apr1916115422Mar211816151413121126Feb25212019181413121123Nov22212016151413121110984324Oct198525Sep242114133Aug23Jul1312422Jun211512118131May3029201817161574318Apr76330Mar292814913Feb131Jan3018171621Dec1918141312628Nov1514913Oct121110653226Sep252322211527Jul2120181714131210876330Jun27262322212017Mayignore 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 freemore compact assign clauses for state variables, and remove useless memory pack predicates and assertionsremove tests with include directivesreintroduce existential for variables that may appear free when performing substitutionmore agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)fix test scriptfix bug in handling state variables in nested expressionsadd basic support to protect against some ACSL keywordsfix live variable calculation for spec: take variables occuring in clocks into accountprint (*mem) instead of *mem to avoid ambiguities with accessesfix handling of state variables in spec expressionsfix bug where singleton tuples were generatedtest everythingfix offline testsadd offline tests and fix a bug in generated spec where optimization was not performedfix tests procedureDocker filesa working version for automata with 'last' case of enums as default caseworking version for stateful contractsproper generation of stateful contractsproper handling of stateless nodes and automata