/**
 * @name RangeSsa completeness test
 * @description RangeSsa completeness test. If there is a
 *    RangeSsaDefinition for a variable that reaches a use of that
 *    variable then there must be a RangeSsaDefinition for that use
 * @kind test
 */

import cpp
import semmle.code.cpp.rangeanalysis.RangeSSA

/* Count of number of uses of a LocalScopeVariable where no corresponding SSA definition exists,
   but at least one SSA definition for that variable can reach that use.
   Should always be zero *regardless* of the input */
select
count(LocalScopeVariable v, Expr use |
      exists(RangeSsaDefinition def, BasicBlock db, BasicBlock ub | 
          def.getAUse(v) = use and db.contains(def.getDefinition()) and ub.contains(use) |
          db.getASuccessor+() = ub
      )
      and not exists(RangeSsaDefinition def | def.getAUse(v) = use)
)