Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002229Frama-CPlug-in > wppublic2016-05-31 17:492016-05-31 17:49
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformUbuntuOSOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in Version 
Summary0002229: Validation fails when predicate is used with implicit type conversion.
DescriptionWhen there is an implicit type conversion on a parameter, and the value is checked by a predicate, validation fails when it should succeed.

In the example below, the functions foo and foo_pred have the same precondition, except foo_pred has the statement in a predicate. foo validates while foo_pred does not.

run2 validates the assertion, showing the precondition should be true, but foo_pred still fails.

run3 is similar to run2 except a ghost variable is used. This causes foo_pred to validate.
Steps To ReproduceFile foo.c (attached):
/*@
    predicate bar_req(int i) = ((unsigned char) i) == i;
*/

//@ requires ((unsigned char) i) == i;
void foo(int i) {
}

//@ requires bar_req(i);
void foo_pred(int i) {
}

void run(char c) {
    unsigned char uc = c;
    foo(uc); // Valid
    foo_pred(uc); // Fails
}

void run2(char c) {
    unsigned char uc = c;
    //@ assert ((unsigned char) ((int) uc)) == uc;
    foo_pred(uc); // Fails
}

void run3(char c) {
    unsigned char uc = c;
    //@ ghost int ic = uc;
    //@ assert ((unsigned char) ic) == uc;
    foo_pred(uc); // Valid
}


Run command:
frama-c foo.c -wp -wp-prover why3:alt-ergo -wp-model=typed+Cast

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing foo.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [alt-ergo] Goal typed_cast_run2_call_foo_pred_pre : Unknown (158ms)
[wp] [alt-ergo] Goal typed_cast_run_call_foo_pred_pre : Unknown (Qed:0.54ms) (157ms)
[wp] Proved goals: 4 / 6
     Qed: 3
     alt-ergo: 1 (10ms) (unknown: 2)
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (591 bytes) 2016-05-31 17:49 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-05-31 17:49 Ian New Issue
2016-05-31 17:49 Ian Status new => assigned
2016-05-31 17:49 Ian Assigned To => correnson
2016-05-31 17:49 Ian File Added: foo.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker