Unproven rte assertions for bit complement
ID0001769: This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001769 | Frama-C | Plug-in > RTE | public | 2014-05-01 | 2014-05-19 |
| Reporter | jens | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
I am struggling with unproven run time assertions in a some piece of code that heavily relies on bit operations. In fact, I am not sure this an issue of the rte plug-in. It is probably related to https://bts.frama-c.com/view.php?id=1750 which I submitted to the WP section. However, I wonder if the rte plug-in could make the task of WP easier.
The attached file simply performs bitwise complement for various unsigned integer types. For unsigned char and unsigned short the rte plugin generates unsigned_downcast assertion that WP cannot discharge. I understand that the promotion of the variable "a" to int is covered by the C standard. On the other hand, the C standard says in 6.5.3.4 (4)
If the promoted type is an unsigned type, the expression ~E is equivalent to the maximum value
representable in that type minus E.So, no overflow will occur.
Steps To Reproduce :
I called the file with the following options
frama-c-gui.byte -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -pp-annot -no-unicode -wp -warn-signed-downcast -warn-signed-overflow -warn-unsigned-downcast -warn-unsigned-overflow -wp-rte complement.c