You can't have this bug in WUFFS. The WUFFS compiler will point out that it can't see any reason to believe the expression won't overflow, and any possibility of overflow is illegal in WUFFS, so your program is invalid and won't compile. So you need to write code which can't overflow.
Of course WUFFS is deliberately constrained to a simple world and thus utterly unsuitable for writing an operating system kernel. However, the principles do apply, the authors of this code didn't want overflow to be possible, they just didn't have a way to express that to their compiler.
In Rust it is at least easier to express that you don't want overflow:
let x = size.checked_add(len).unwrap().checked_add(2).unwrap();
if (x > PAGE_SIZE) { ...
The above code will panic (regardless of build parameters) if adding size + len + 2 overflows. If you don't want a panic, you can write some unwrap_or_else() code to pick some preferred value when overflow occurs, or you can handle the None result (which is what checked_add gives you for overflow) explicitly.
However, perhaps it should be possible to express at compile time that you want an expression which can't overflow at runtime, as in WUFFS.
Of course WUFFS is deliberately constrained to a simple world and thus utterly unsuitable for writing an operating system kernel. However, the principles do apply, the authors of this code didn't want overflow to be possible, they just didn't have a way to express that to their compiler.
In Rust it is at least easier to express that you don't want overflow:
The above code will panic (regardless of build parameters) if adding size + len + 2 overflows. If you don't want a panic, you can write some unwrap_or_else() code to pick some preferred value when overflow occurs, or you can handle the None result (which is what checked_add gives you for overflow) explicitly.However, perhaps it should be possible to express at compile time that you want an expression which can't overflow at runtime, as in WUFFS.