UniAna.Unchanged
UniAna.Uniana
UniAna.cfg.CFGancestor
UniAna.cfg.CFGdef
- Definition of the reducible CFG
- Decidable properties on redCFG
- Definition of depth
- Some basic facts
- Generalizations of properties on CFGs for non-redCFG graphs
UniAna.cfg.CFGgeneral
UniAna.cfg.CFGinnermost
- Loop ordering
- Innermost loops and strit-innermost loops
- Lemmas about relative loop depth on exit edges
- Variant of get_innermost_loop that uses the root if there is no loop
UniAna.cfg.CFGloopcutting
UniAna.cfg.CFGloop
UniAna.cfg.CFGTac
UniAna.cfg.CncLoop
UniAna.cfg.ContractPath
UniAna.cfg.EEdge
UniAna.cfg.headexit
- Prerequisites
- redCFG Instance for the head_exit CFG
- The head exit property
- Properties of head exit CFGs