Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:45 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002322Frama-CKernelpublic2017-07-31 13:142017-12-06 09:11
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformPhosphorus-20170501-beta1OSxubuntuOS Version
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in VersionFrama-C 16-Sulfur 
Summary0002322: repeated predicate definitions in separate file cause crash
DescriptionRunning 'frama-c -wp part.c whole.c' on the attached files causes the follwoing crash:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing part.c (with preprocessing)
[kernel] Parsing whole.c (with preprocessing)
[wp] warning: Missing RTE guards
[kernel] Current source was: whole.c:12
         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/plugins/wp/LogicCompiler.ml", line 772, characters 17-61
         Called from file "src/plugins/wp/Warning.ml", line 139, characters 6-10
         Called from file "src/plugins/wp/LogicSemantics.ml", line 853, characters 12-42
         Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
         Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 41-46
         Called from file "src/plugins/wp/Warning.ml", line 155, characters 14-18
         Called from file "src/plugins/wp/cfgWP.ml", line 461, characters 23-135
         Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
         Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
         Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
         Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
         Called from file "list.ml", line 84, characters 24-34
         Called from file "src/plugins/wp/calculus.ml", line 339, characters 22-62
         Called from file "src/plugins/wp/calculus.ml", line 343, characters 23-45
         Called from file "src/plugins/wp/calculus.ml", line 647, characters 20-43
         Called from file "src/plugins/wp/calculus.ml", line 606, characters 19-40
         Called from file "src/plugins/wp/calculus.ml", line 757, characters 40-59
         Called from file "set.ml", line 305, 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 "src/plugins/wp/calculus.ml", line 757, characters 4-64
         Called from file "src/plugins/wp/calculus.ml", line 793, characters 19-51
         Called from file "src/plugins/wp/cfgWP.ml", line 1468, characters 43-66
         Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48
         Called from file "src/plugins/wp/cfgWP.ml", line 1456, characters 14-957
         Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
         Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 25-28
         Called from file "src/plugins/wp/Model.ml", line 126, characters 19-36
         Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
         Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
         Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
         Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
         Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
         
         Unexpected error (Not_found).
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Phosphorus-20170501-beta1.


The problem disappears if:
* the source file order is exchanged on the command line,
* the overloaded predicate 'Bnd(integer n)' in while.c:5 is renamed e.g. to 'Bnd2',
* the trivial 'ensures' clause is removed in whole.c:10, or
* the 'requires' clause in whole.c:9 is changed to 'Bnd(1,(int)0)', i.e. 'Bnd' is inlined.
TagsNo tags attached.
Attached Files
  • c file icon part.c (97 bytes) 2017-07-31 13:14 - 
    /*@
	axiomatic ax { logic int Acc(int m); } 
	predicate Bnd(integer n,int m) = Acc(m)<=9; 
*/
    c file icon part.c (97 bytes) 2017-07-31 13:14 +
  • c file icon whole.c (199 bytes) 2017-07-31 13:14 - 
    /*@
	axiomatic ax { logic int Acc(int m); }
	predicate Bnd(integer n,int m) = Acc(m)<=9;
	predicate Bnd(integer n) = Bnd(n, (int) 0);
*/

/*@
	requires Bnd(1);
	ensures \true;
*/
void foo(void) {}
    c file icon whole.c (199 bytes) 2017-07-31 13:14 +

-Relationships
has duplicate 0002151closedvirgile predicate overloading causes crash when multiple files are given to wp 
+Relationships

-Notes

~0006430

Jochen (reporter)

2017-07-31 13:18

 Note that the contents of 'part.c' is a proper prefix of that of 'whole.c' (except for the closing '*/'). The crash problem also disappears when a definition disagrees between both files.

~0006431

jens (reporter)

2017-08-01 16:33

 I looked at another example and it really looks like Frama-C has a problem with overloaded predicates
when multiple files are processed.

~0006432

jens (reporter)

2017-08-02 09:55

 This might be related to https://bts.frama-c.com/view.php?id=2151

~0006448

virgile (developer)

2017-08-25 10:43

 Fixed in MR 1457 (now merged)
+Notes

-Issue History
Date Modified Username Field Change
2017-07-31 13:14 Jochen New Issue
2017-07-31 13:14 Jochen File Added: part.c
2017-07-31 13:14 Jochen File Added: whole.c
2017-07-31 13:18 Jochen Note Added: 0006430
2017-08-01 16:33 jens Note Added: 0006431
2017-08-02 09:55 jens Note Added: 0006432
2017-08-25 10:43 virgile Note Added: 0006448
2017-08-25 10:43 virgile Status new => resolved
2017-08-25 10:43 virgile Fixed in Version => Frama-C GIT, precise the release id
2017-08-25 10:43 virgile Resolution open => fixed
2017-08-25 10:43 virgile Assigned To => virgile
2017-12-06 09:09 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C 16-Sulfur
2017-12-06 09:10 signoles Status resolved => closed
2017-12-06 09:11 signoles Relationship added has duplicate 0002151
+Issue History