Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002082Frama-CPlug-in > wppublic2015-02-24 20:242016-01-26 08:52
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSUbuntuOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002082: Crash with \is_infinite
DescriptionUsing the built-in \is_infinite causes wp to crash. This is used in the provided libc specifications (math.h), and a call to these functions will cause a crash.
Steps To ReproduceCreate program: #include /*@ ensures \true; */ void main() { double val = acos(1); } Run frama-c, where FRAMA_C_LIBC is .../frama-c-Neon-20140301/share/libc: frama-c -cpp-extra-args="-I${FRAMA_C_LIBC}" -wp is_infinte_test.c Get output: [wp] Running WP plugin... [wp] Collecting axiomatic usage is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acos, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosf, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosh, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshf, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshl, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosl, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asin, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinf, generating default assigns from the specification is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinl, generating default assigns from the specification [wp] warning: No definition for 'memchr' interpreted as reads nothing [wp] warning: No definition for 'memset' interpreted as reads nothing [wp] warning: No definition for 'strchr' interpreted as reads nothing [wp] warning: No definition for 'strcmp' interpreted as reads nothing [wp] warning: No definition for 'wcscmp' interpreted as reads nothing [wp] warning: No definition for 'wcslen' interpreted as reads nothing [wp] warning: No definition for 'wcsncmp' interpreted as reads nothing [wp] warning: Missing RTE guards [wp] user error: Builtin \is_infinite(float64) not defined [wp] failure: Logic '\is_infinite' undefined [kernel] Current source was: is_infinte_test.c:8 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "src/wp/LogicCompiler.ml", line 698, characters 20-51 Called from file "src/wp/LogicCompiler.ml", line 758, characters 10-23 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "list.ml", line 57, characters 20-23 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/cfgWP.ml", line 1069, characters 18-63 Called from file "src/wp/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 1099, characters 23-207 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/calculus.ml", line 448, characters 14-224 Called from file "src/wp/calculus.ml", line 595, characters 10-57 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 579, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 574, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 699, characters 40-59 Called from file "set.ml", line 288, characters 38-41 Called from file "map.ml", line 169, characters 20-25 Called from file "map.ml", line 169, characters 10-18 Called from file "map.ml", line 169, characters 10-18 Called from file "src/wp/calculus.ml", line 699, characters 4-64 Called from file "src/wp/calculus.ml", line 745, characters 19-51 Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837 Called from file "src/wp/Model.ml", line 111, characters 17-20 Re-raised at file "src/wp/Model.ml", line 116, characters 25-28 Called from file "src/wp/Model.ml", line 117, characters 19-36 Called from file "src/wp/register.ml", line 435, characters 17-42 Called from file "src/wp/register.ml", line 574, characters 17-24 Re-raised at file "src/wp/register.ml", line 578, characters 29-31 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8 Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Neon-20140301. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005967)
correnson (manager)
2015-06-29 17:24

Thanks. We should add this built-in.
(0005968)
correnson (manager)
2015-06-29 17:25

Missing built-in
(0006004)
correnson (manager)
2015-08-18 14:07

Fixed in trunk.

- Issue History
Date Modified Username Field Change
2015-02-24 20:24 Ian New Issue
2015-02-24 20:24 Ian Status new => assigned
2015-02-24 20:24 Ian Assigned To => correnson
2015-06-29 17:24 correnson Note Added: 0005967
2015-06-29 17:25 correnson Note Added: 0005968
2015-06-29 17:25 correnson Status assigned => acknowledged
2015-08-18 14:07 correnson Note Added: 0006004
2015-08-18 14:07 correnson Status acknowledged => resolved
2015-08-18 14:07 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker