Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002039Frama-CPlug-in > wppublic2014-12-22 22:152014-12-22 22:15
Reportergaggarwal 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002039: WP-Plugin crashes due to an internal error when terms of sets during union have different types
DescriptionIn case type of terms of tset1 and tset2 is different, then assigns \union(tset1, tset2) causes WP to crash. In the example in attached file, first set has terms of type int, and other set set has terms of type double. union is throwing following error: failure: c-object of logic type (ℝ)
Steps To ReproduceWhen attached file is called with the following command-line: frama-c -wp-fct copy -wp-print -wp-out temp -continue-annot-error array_assigns.c Frama-C produces below output: [kernel] preprocessing with "gcc -C -E -I. EditorTest/src/FVal_Infer/array_assigns.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards EditorTest/src/FVal_Infer/array_assigns.c:9:[wp] failure: c-object of logic type (ℝ) [kernel] Current source was: EditorTest/src/FVal_Infer/array_assigns.c:9 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/LogicSemantics.ml", line 802, characters 2-35 Called from file "list.ml", line 55, characters 20-23 Called from file "src/wp/LogicSemantics.ml", line 808, characters 27-51 Called from file "src/wp/cfgWP.ml", line 412, characters 6-147 Called from file "src/wp/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 468, characters 22-126 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 334, characters 27-62 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 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 599, characters 22-40 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 396, characters 20-39 Called from file "src/wp/calculus.ml", line 610, characters 10-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 304, characters 38-41 Called from file "map.ml", line 168, characters 20-25 Called from file "map.ml", line 168, characters 10-18 Called from file "map.ml", line 168, characters 10-18 Called from file "map.ml", line 168, 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 array_assigns.c [^] (194 bytes) 2014-12-22 22:15 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-12-22 22:15 gaggarwal New Issue
2014-12-22 22:15 gaggarwal Status new => assigned
2014-12-22 22:15 gaggarwal Assigned To => correnson
2014-12-22 22:15 gaggarwal File Added: array_assigns.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker