search

alegnani / pancake-verifier

2 stars 0 forks source link

Function return statment #56

Open JunmingZhao42 opened 2 weeks ago

JunmingZhao42 commented 2 weeks ago

The recent change(s) seem to break the parsing of return statements, as:

This doesn't work:

fun net_require_signal(1 queue_ptr)
{
    var signalled = 0;
    !ld8 signalled, queue_ptr + 3 * @biw;
    return (!signalled);
}

thread 'main' panicked at pancake2viper/src/ir_to_viper/utils.rs:90:18:
internal error: entered unreachable code

This works fine:

fun net_require_signal(1 queue_ptr)
{
    var signalled = 0;
    !ld8 signalled, queue_ptr + 3 * @biw;
    var ret = !signalled;
    return ret;
}