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