Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002354Frama-CPlug-in > RTEpublic2018-02-03 12:152018-11-30 10:07
Reporterxleroy 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in VersionFrama-C 18-Argon 
Summary0002354: RTE assertion for signed right shift is wrong
DescriptionConsider:

/*@ ensures \result == arg >> 2; */

int toto(int arg) { return arg >> 2; }

"frama-c -wp -wp-rte" fails to verify this rather tautological spec because the RTE pass inserts the assertion

  /*@ assert rte: shift: 0 ≤ arg; */

I think this is an incorrect reading of the ISO C 90 and C 99 specs: right-shift of a signed integer expression that has a negative value is implementation-defined, but is not an undefined behavior. (See ISO C 99 section 6.5.7 item 5.)

I would suggest that WP and RTE accept the spec above, so that I can actually reason about the right shift, probably by adding axioms specifying how right shifts of negative numbers work on the platforms I am (and everyone is) interested in.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006664)
signoles (manager)
2018-10-15 17:17

A new kernel option (-warn-right-shift-negative) has been introduced for controlling this behaviour. It is deactivated by default (while -warn-left-shift-negative is activated by default), hence no assertion is now emitted by default on your example.

This option is supported by plug-ins Eva and RTE. The assertions generated by RTE impact plug-ins E-ACSL and WP.

- Issue History
Date Modified Username Field Change
2018-02-03 12:15 xleroy New Issue
2018-02-03 12:15 xleroy Status new => assigned
2018-02-03 12:15 xleroy Assigned To => signoles
2018-10-15 17:17 signoles Note Added: 0006664
2018-10-15 17:17 signoles Status assigned => resolved
2018-10-15 17:17 signoles Resolution open => fixed
2018-11-30 10:07 signoles Fixed in Version => Frama-C 18-Argon
2018-11-30 10:07 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker