search

zetzit / zz

🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

negative literals are unconstrained #112

Closed jacereda closed 3 years ago

jacereda commented 4 years ago

If I set temp below to 3 it works correctly, but passing negative values fails.

const i8 THRESHOLD = 10;

pub theory cold(i8 degrees) -> bool
(
    degrees < THRESHOLD
)

export fn main() -> int {
    i8 temp = -3;
    static_assert(cold(temp));
    return 0;
}
aep commented 4 years ago

Looks like a bug to me. Probably passing the wrong type for i8 to ssa.

jacereda commented 4 years ago

s/i8/int/g yields the same result.

aep commented 4 years ago

can reproduce. the ssa looks fine, except it lacks any literal value. negative integers are emitted as C literal.