Frama-C Bug Tracking System - Frama-C
View Issue Details
0002141Frama-CPlug-in > wppublic2015-07-01 19:222016-01-26 08:52
Ian 
correnson 
normalminoralways
closedfixed 
Ubuntu
Frama-C Sodium 
Frama-C Magnesium 
0002141: Incorrect result with X modulo 1
WP concludes that “n % 1 == n”, instead of “n % 1 == 0” where n are integers. This is only a problem with modulo 1, the correct answer is obtained for other integers, or if n is 0 (0 % 1 == 0). This can be shown with the following lemmas. /*@ lemma mod_one_error: \forall integer i; (i % 1) == i; */ > frama-c mod.c -wp -wp-prop=@lemma [kernel] preprocessing with "gcc -C -E -I. mod.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_lemma_mod_one_error : Valid [wp] Proved goals: 1 / 1 Qed: 1 /*@ lemma mod_one: \forall integer i; (i % 1) == 0; */ > frama-c mod.c -wp -wp-prop=@lemma [kernel] preprocessing with "gcc -C -E -I. mod.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal typed_lemma_mod_one : Unknown [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unknown: 1) I would have expected ‘mod_one_error’ not to validate, and ‘mod_one’ to validate. The goal generated for mod_one also illustrates the issue. lemma_mod_one.ergo: (* ---------------------------------------------------------- *) (* --- Lemma 'mod_one' --- *) (* ---------------------------------------------------------- *) (* --- Global Definitions --- *) goal lemma_mod_one: forall i : int. 0 = i This leads to vacuous truths when assuming the correct result. In the example below, wp believes ‘i' is 1, and our assumption leads to the contradictions 1 == 0. void f1() { int i = 1 % 1; //@ assert i == 0; //@ assert vacuous: \false; } > frama-c mod.c -wp [kernel] preprocessing with "gcc -C -E -I. mod.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Qed] Goal typed_f1_assert_vacuous : Valid [wp] [Alt-Ergo] Goal typed_f1_assert : Unknown [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unknown: 1) This behavior was observed in both Neon and Sodium.
No tags attached.
Issue History
2015-07-01 19:22IanNew Issue
2015-07-01 19:22IanStatusnew => assigned
2015-07-01 19:22IanAssigned To => correnson
2015-08-18 14:10corrensonNote Added: 0006005
2015-08-18 14:10corrensonStatusassigned => resolved
2015-08-18 14:10corrensonResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

Notes
(0006005)
correnson   
2015-08-18 14:10   
Already fixed in trunk. Thanks for the report.