alegnani / pancake-verifier

2 stars 0 forks source link

Nested while loop continue and break labels #28

Closed JunmingZhao42 closed 1 month ago

JunmingZhao42 commented 1 month ago

Currently it seems that the continue and break label of while loops are having duplicate naming issue. For example:

fun double_while() {
    var i = 0;
    var j = 0;
    while (i < 10) {
        while (j < 10) {
            j = j + 1;
            if (j == 5) {
                break;
            }
        }
        i = i + 1;
        if (i == 5) {
            break;
        }
    }
    return 0;
}

The above function has double label break_label_0 and label continue_label_0 in Viper.