short int to float assertion not proved
ID0001653: This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001653 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| Reporter | dharma | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Ubuntu | OS | Linux | OS Version | 64 bit |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
Wonder why this assertion is not provable even though it is a valid one.
#include <limits.h>
/*@ requires x != 0; assigns \nothing; */ void assert(int x);
int main() { float f = SHRT_MAX; short int i = f; assert(i == SHRT_MAX); }
Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_short_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD float_to_short_int_max_2.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function main [wp] 3 goals scheduled [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (8ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown