Feature request: Saturating arithmatic

[danielsn]

It would be really useful to have saturating arithmetic primitives in CBMC

[martin-cs]

This should be reasonably do-able but it would be good to know a bit more about what you want. Are you using the internal back-end or an SMT solver? Do you want signed or unsigned? Do you have a particular implementation / system in mind? What about the edge cases involving the limit value(s); what is LIMIT * 0, what is LIMIT / 0 or 0 / LIMIT?

[peterschrammel]

@danielsn, can you give a code example of a use case?

[martin-cs]

Note that #5405 would give a relatively simple and probably pretty good route to implementing them.

[danielsn]

I'm trying to implement operations like these:
I'm trying to implement these:
https://doc.rust-lang.org/std/intrinsics/fn.saturating_add.html
https://doc.rust-lang.org/std/intrinsics/fn.saturating_sub.html
https://doc.rust-lang.org/std/primitive.u32.html#method.saturating_mul