Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002151Frama-CKernel > ACSL implementationpublic2015-07-30 15:072017-12-06 09:11
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionduplicate 
PlatformSodium-20150201OSxubuntu14.04OS Version
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C GIT, precise the release id 
Summary0002151: predicate overloading causes crash when multiple files are given to wp
DescriptionRunning "frama-c -wp 481a.c 481b.c" on the attached files causes a crash with following output:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 481a.c (with preprocessing)
[kernel] Parsing 481b.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[kernel] Current source was: 481b.c:9
         The full backtrace is:
         Raised at file "map.ml", line 117, characters 16-25
         Called from file "list.ml", line 55, characters 20-23
         Called from file "src/wp/LogicCompiler.ml", line 776, characters 17-61
         Called from file "src/wp/Warning.ml", line 139, characters 6-10
         Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
         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 462, 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 84, 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 724, 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 "src/wp/calculus.ml", line 724, characters 4-64
         Called from file "src/wp/calculus.ml", line 770, characters 19-51
         Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
         Called from file "src/wp/cfgWP.ml", line 1391, 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 15-40
         Called from file "src/wp/register.ml", line 574, characters 17-24
         Re-raised at file "src/wp/register.ml", line 578, characters 27-29
         Called from file "src/wp/register.ml", line 575, characters 17-24
         Re-raised at file "src/wp/register.ml", line 579, characters 30-32
         Called from file "src/wp/register.ml", line 575, characters 17-24
         Re-raised at file "src/wp/register.ml", line 579, characters 30-32
         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 763, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
         
         Unexpected error (Not_found).
         Please report as 'crash' at http://bts.frama-c.com/. [^]
         Your Frama-C version is Sodium-20150201.
TagsNo tags attached.
Attached Filesc file icon 481a.c [^] (96 bytes) 2015-07-30 15:07 [Show Content]
c file icon 481b.c [^] (187 bytes) 2015-07-30 15:08 [Show Content]

- Relationships
duplicate of 0002322closedvirgile repeated predicate definitions in separate file cause crash 

-  Notes
(0006003)
correnson (manager)
2015-08-17 11:31

Seems to be a problem about overloaded logic functions.
(0006010)
correnson (manager)
2015-08-19 12:47

This is probably a linker problem (merge-cil):

$ frama-c -check 481a.c 481b.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 481a.c (with preprocessing)
[kernel] Parsing 481b.c (with preprocessing)
481b.c:9:[kernel] failure: [AST Integrity Check] initial AST
                  Function eql expects 2 arguments but is used with 1
[removed stack trace]
(0006011)
correnson (manager)
2015-08-19 12:48

PS : overloading in WP is well supported.
(0006433)
jens (reporter)
2017-08-02 11:10

probably related to https://bts.frama-c.com/view.php?id=2322 [^]
(0006449)
virgile (developer)
2017-08-25 10:48

As mentioned, this is the same issue as 2322

- Issue History
Date Modified Username Field Change
2015-07-30 15:07 Jochen New Issue
2015-07-30 15:07 Jochen File Added: 481a.c
2015-07-30 15:08 Jochen File Added: 481b.c
2015-08-04 09:41 signoles Assigned To => correnson
2015-08-04 09:41 signoles Status new => assigned
2015-08-04 09:41 signoles Category Kernel => Plug-in > wp
2015-08-17 11:31 correnson Note Added: 0006003
2015-08-17 11:31 correnson Status assigned => acknowledged
2015-08-19 12:47 correnson Note Added: 0006010
2015-08-19 12:47 correnson Assigned To correnson => virgile
2015-08-19 12:47 correnson Status acknowledged => assigned
2015-08-19 12:48 correnson Note Added: 0006011
2017-08-02 11:10 jens Note Added: 0006433
2017-08-25 10:48 virgile Note Added: 0006449
2017-08-25 10:48 virgile Status assigned => closed
2017-08-25 10:48 virgile Resolution open => duplicate
2017-08-25 10:48 virgile Category Plug-in > wp => Kernel > ACSL implementation
2017-08-25 10:48 virgile Fixed in Version => Frama-C GIT, precise the release id
2017-12-06 09:11 signoles Relationship added duplicate of 0002322


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker