|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002296||Frama-C||Plug-in > wp||public||2017-05-08 13:18||2017-05-08 13:18|
|Assigned To||correnson|| |
|Platform||Phosphorus-20170501-beta1||OS||xubuntu 16.04.1||OS Version|
|Product Version|| |
|Target Version||Fixed in Version|| |
|Summary||0002296: axiom about bounds of lsl result needed in the long run|
|Description||Running "frama-c -wp and.c" on the attached program fails to prove the assertion in line 5, although it should follow immediately from the assignment in line 4.|
Looking at the generated mlw file shows that "k=to_uint16(k)" can't be proven (variable name taken from c source). Apparently, the range boundaries of m from the contract in line 2 aren't propagated to m<<1.
In the long run, when bit operations will be handled in a satisfactory way, this issue should be resolved, too; the attached program can be used as a regeression test for it.
|Tags||No tags attached.|
|Attached Files|| and.c [^] (122 bytes) 2017-05-08 13:18 [Show Content]