int to double - assert not verified

ID0001651: This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001651	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 :

For this below program, the assert should be valid I think but the WP is not proving it.

#include <limits.h>

/*@ requires x != 0; assigns \nothing; */ void assert(int x);

int main() { double f = INT_MAX; int i = f; assert(i == INT_MAX); return 0; }

Additional Information :

The regular C assert was able to prove when I run the a.out after compiling the wrong (commenting the ACSL's assert).

Steps To Reproduce :

[formal_verification]$ frama-c -wp -wp-rte double_to_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD double_to_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 (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)