Substraction results in unknown values
ID0002166: This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 | 2017-12-17 |
| Reporter | kroeckx | Assigned To | buhler | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
This line of code has: if (len + n >= 64) len -= n;
For callstack [SHA256_Update :: frama-test.c:19 <- main] Before this statement / after this statement: n ∈ [1..63]
and: For callstack [SHA256_Update :: frama-test.c:19 <- main] Before this statement: len ∈ [1..1024] After this statement: len ∈ -..-
I was expecting len after this to be: len ∈ [0..1023]
It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in: len ∈ [-62..1023]
Kurt