Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002141Frama-CPlug-in > wppublic2015-07-01 19:222016-01-26 08:52
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSUbuntuOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002141: Incorrect result with X modulo 1
DescriptionWP 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006005)
correnson (manager)
2015-08-18 14:10

Already fixed in trunk.
Thanks for the report.

- Issue History
Date Modified Username Field Change
2015-07-01 19:22 Ian New Issue
2015-07-01 19:22 Ian Status new => assigned
2015-07-01 19:22 Ian Assigned To => correnson
2015-08-18 14:10 correnson Note Added: 0006005
2015-08-18 14:10 correnson Status assigned => resolved
2015-08-18 14:10 correnson Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker