wrong example code in value analysis manual, p.35, for message " invalid LHS operand for left shift"
ID0002257: This issue was created automatically from Mantis Issue 2257. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002257 | Frama-C | Documentation > manuals | public | 2016-11-21 | 2016-12-08 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
p.35 (top) of the value analysis manual shows the code from the attached file "lshift_orig.c". However, "frama-c -val lshift_orig.c" does not emit the warning "invalid LHS operand for left shift. assert 0 <= x;" shown in the manual. In fact, x is only written, not read, by the code.
Probably, the code should be like that in file "lshift_new.c". Frama-C emits "lshift_new.c:3:[kernel] warning: invalid LHS operand for left shift. assert 0 ≤ c;" and "lshift_new.c:3:[kernel] warning: signed overflow. assert c<<1 ≤ 2147483647;" when run on that code.