Unproven rte assertions for bit complement
ID0001769: This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.
|ID0001769||Frama-C||Plug-in > RTE||public||2014-05-01||2014-05-19|
|Reporter||jens||Assigned To||correnson||Resolution||no change required|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||-|
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 126.96.36.199 (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