Model integers as bounded - Githubissues

alegnani / pancake-verifier

1 stars 0 forks source link

Model integers as bounded #34

Open alegnani opened 1 week ago

alegnani commented 1 week ago

Pancake uses bounded integers of 64-bits (32-bit for 32-bit binaries). This is currently not modeled in Viper where they are instead unbounded.

[ ] Add support for unsigned logical operators: <+, <=+, >+, >=+
[ ] Add checks and constraints to integers in Viper