Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001936Frama-CPlug-in > wppublic2014-10-12 04:082014-10-14 16:55
ReporterWolframKahl 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSGNU/LinuxOS Version3.14.14-gentoo
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001936: WP crashes on \floor builtin
DescriptionRunning frama-c-gui -wp floor.c produces the following in the pre-GUI-console: [kernel] preprocessing with "gcc -C -E -I. floor.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] user error: Builtin \floor(real) not defined [wp] failure: Logic '\floor' undefined and then crashes with a pop-up containing: Current source was: :0 The full backtrace is: Raised at file "hashtbl.ml", line 254, characters 18-27 Called from file "hashtbl.ml", line 262, characters 22-38 Plug-in wp aborted: internal error. Reverting to previous state. Look at the console for additional information (if any). 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 (I get this also with Fluorine.)
Steps To Reproduceframa-c -wp floor.c frama-c-gui -wp floor.c
Additional InformationBacktrace from the command-line: $ frama-c -wp floor.c [kernel] preprocessing with "gcc -C -E -I. floor.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] user error: Builtin \floor(real) not defined [wp] failure: Logic '\floor' undefined [kernel] Current source was: floor.c:7 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 748, characters 10-23 Called from file "src/wp/LogicSemantics.ml", line 518, characters 8-34 Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27 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 358, characters 20-35 Called from file "src/wp/LogicSemantics.ml", line 336, characters 31-50 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/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 456, characters 23-140 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 "list.ml", line 74, characters 24-34 Called from file "src/wp/calculus.ml", line 331, characters 22-64 Called from file "src/wp/calculus.ml", line 341, characters 23-45 Called from file "src/wp/calculus.ml", line 613, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 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/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 Filesc file icon floor.c [^] (228 bytes) 2014-10-12 04:08 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-10-12 04:08 WolframKahl New Issue
2014-10-12 04:08 WolframKahl Status new => assigned
2014-10-12 04:08 WolframKahl Assigned To => correnson
2014-10-12 04:08 WolframKahl File Added: floor.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker