Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    Vc: handle missing "diverges" in Vc, not in Dexpr · 3e802ac9
    Andrei Paskevich authored
    On a missing "diverges", Vc emits a warning and adds
    a "false" sub-goal at the location of the non-terminating
    loop or function call. The explanation on this sub-goal is
    "termination", but should probably be "termination (failure)".
    
    The "diverges" clase propagates downwards: if it is put on
    the top-level function, there is no need to repeat it on local
    functions or abstract blocks.
    3e802ac9