Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002241Frama-CPlug-in > wppublic2016-07-29 14:112016-07-29 14:11
Assigned Tocorrenson 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002241: Implicit casting from integer to real causes failure in WP proof generation
DescriptionACSL defines the integer type as a subset of the real type. Therefore, it states, implicit casting from integers to reals is allowed, because one is the subset of another. However, when this is done in practice, the WP plugin will generate goals that provers cannot parse, giving a type error.
Steps To Reproduce== Input file (bug.c): /*@ axiomatic Bug { logic integer ibug; logic real rbug = ibug; } */ /*@ requires i == rbug; */ void foo(int i); void main() { foo(42); } == Command to reproduce frama-c -wp bug.c == Output [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing bug.c (with preprocessing) bug.c:13:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype [wp] warning: Missing RTE guards [wp] 1 goal scheduled /tmp/wp714796.dir/typed/A_Bug.ergo:7:[wp] user error: Alt-Ergo error: characters 1-34:typing error: real and int cannot be unified [wp] [Alt-Ergo] Goal typed_main_call_foo_pre : Failed characters 1-34:typing error: real and int cannot be unified [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (failed: 1)
Additional InformationThis is confirmed to occur with the alt-ergo and why3 provers. Tested on both Frama-C Sodium and Aluminum. Sodium produces slightly different errors than Aluminum, but both produce errors.
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (165 bytes) 2016-07-29 14:11 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-07-29 14:11 jrobbins New Issue
2016-07-29 14:11 jrobbins Status new => assigned
2016-07-29 14:11 jrobbins Assigned To => correnson
2016-07-29 14:11 jrobbins File Added: bug.c

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker