module ConditionalSpec {  
    function f_ConditionalSpec() {
        var integer v_s0;
        var integer v_s1;
        var integer v_s2 := 1;
        var integer v_s3;
        var integer v_s4;
        var integer v_s5;
        
        //v_s2 is initialised upon declaration -> no warning
        if (v_s2 == 1) {
            //v_s3 is not initialised -> warning
            //v_s0 initialised within the conditional after this statement
            v_s0 := v_s3 + 1; 

            //v_s1 is not initialised -> warning
            //v_s2 is initialised -> no warning
            //v_s3 initialised within the conditional after this statement
            v_s3 := v_s2 + 1 + v_s1; 

            //v_s3 is initialised above -> no warning
            //v_s4 initialised within the conditional after this statement
            v_s4 := v_s3 + 1; 
        } else {
            //v_s2 is initialised -> no warning
            //v_s4 initialised within the else branch after this statement
            v_s4 := v_s2 + 1; 
        }

        //v_s3 is only initialised within one of the possible paths -> warning
        //v_s4 is initialised within both possible paths (within all branches of the conditional above) -> no warning
        v_s5 := v_s3 + v_s4; 
    }
      
}