Frama-C Bug Tracking System - Frama-C
View Issue Details
0002151Frama-CKernel > ACSL implementationpublic2015-07-30 15:072017-12-06 09:11
Jochen 
virgile 
normalcrashalways
closedduplicate 
Sodium-20150201xubuntu14.04
Frama-C Sodium 
Frama-C GIT, precise the release id 
0002151: predicate overloading causes crash when multiple files are given to wp
Running "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.
No tags attached.
duplicate of 0002322closed virgile repeated predicate definitions in separate file cause crash 
c 481a.c (96) 2015-07-30 15:07
https://bts.frama-c.com/file_download.php?file_id=1054&type=bug
c 481b.c (187) 2015-07-30 15:08
https://bts.frama-c.com/file_download.php?file_id=1055&type=bug
Issue History
2015-07-30 15:07JochenNew Issue
2015-07-30 15:07JochenFile Added: 481a.c
2015-07-30 15:08JochenFile Added: 481b.c
2015-08-04 09:41signolesAssigned To => correnson
2015-08-04 09:41signolesStatusnew => assigned
2015-08-04 09:41signolesCategoryKernel => Plug-in > wp
2015-08-17 11:31corrensonNote Added: 0006003
2015-08-17 11:31corrensonStatusassigned => acknowledged
2015-08-19 12:47corrensonNote Added: 0006010
2015-08-19 12:47corrensonAssigned Tocorrenson => virgile
2015-08-19 12:47corrensonStatusacknowledged => assigned
2015-08-19 12:48corrensonNote Added: 0006011
2017-08-02 11:10jensNote Added: 0006433
2017-08-25 10:48virgileNote Added: 0006449
2017-08-25 10:48virgileStatusassigned => closed
2017-08-25 10:48virgileResolutionopen => duplicate
2017-08-25 10:48virgileCategoryPlug-in > wp => Kernel > ACSL implementation
2017-08-25 10:48virgileFixed in Version => Frama-C GIT, precise the release id
2017-12-06 09:11signolesRelationship addedduplicate of 0002322

Notes
(0006003)
correnson   
2015-08-17 11:31   
Seems to be a problem about overloaded logic functions.
(0006010)
correnson   
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   
2015-08-19 12:48   
PS : overloading in WP is well supported.
(0006433)
jens   
2017-08-02 11:10   
probably related to https://bts.frama-c.com/view.php?id=2322
(0006449)
virgile   
2017-08-25 10:48   
As mentioned, this is the same issue as 2322