source: CIVL/examples/languageFeatures/conditionalExpression.cvl@ 1258be5

/* Commandline execution:
 *              civl verify conditionalExpression.cvl
 * */
int n = 2;
$assume n > (5 > 7 ? 1 : 0);

int sum(int k){
        int sum = 0;
        for(int i = 1; i <= k; i++)
                sum += i;
        return sum;
}

void main(){
        int i = 1;
        
        // This would be 
        // Location Z:
        // when (n > 2) s = sum(5) goto ...
        // when (!(n > 2)) s = sum(8) goto ...
        int s = sum(n > 2 ? 5 : 8);

        //$when(n >= 2) $assert s == 9*8/2;
        $assert s == 9 * (n > 2 ? 5 : 8) / 2;

        // This should be translated into 
        // Location X: 
        // when(i>1) n = 1 goto ... 
        // when (!(i>1)) n = 2
        n = i > 1 ? 1 : 2;
        $assert n == 2;

        // This should be translated into
        // int v0;
        // if(n > 1) v0 = 1; else v0 = 2;
        // int v1;
        // if(i < 1) v1 = 1; else v1 = 2;
        // n = v0 + v1;
        n = (n > 1 ? 1 : 2) + (i < 1 ? 1 : 2);
        $assert n == 3;

        // conditional expression as the guard of a loop
        for(int j = 0; (j < 5 ? 1 : 0); j++){
                n = i * j;
        }
        $assert n == 4;

        // as the guard of when statement
        $when(n < 1 ? 0 : 1) n = 3;

        // as the guard of if statement
        if(n < 1 ? 0 : 1) n = 5;  
        $assert n == 5;
        
        // nested conditional expression
        s = (s < 30 ? 10 : (n < 40 ? 50 : 6));
        $assert s == 50;
}