2021-03-05 07:52 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002420Frama-CPlug-in > wppublic2018-12-28 00:582020-09-09 16:21
Reporterfrederic.loulergue@nau.edu 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusresolvedResolutionfixed 
PlatformMacOSmacOSOS VersionMojave 10.14.1
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002420: Wp crashes on a recursive function
Descriptionframa-c -wp tmp.c give the following trace. If the recursive call in e_get is removed, no crash.

[kernel] Parsing tmp.c (with preprocessing)
[wp] Running WP plugin...
[kernel] Current source was: tmp.c:14
  The full backtrace is:
  Raised by primitive operation at file "src/kernel_services/ast_data/statuses_by_call.ml", line 198, characters 11-65
  Called from file "list.ml", line 82, characters 20-23
  Called from file "src/kernel_services/ast_data/statuses_by_call.ml", line 231, characters 6-150
  Called from file "src/plugins/wp/cil2cfg.ml", line 859, characters 6-35
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
  Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
  Called from file "src/plugins/wp/cil2cfg.ml", line 1216, characters 13-47
  Called from file "src/plugins/wp/cil2cfg.ml", line 1248, characters 6-30
  Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
  Called from file "src/plugins/wp/cil2cfg.ml" (inlined), line 1288, characters 13-33
  Called from file "src/plugins/wp/wpAnnot.ml", line 1291, characters 12-26
  Called from file "src/plugins/wp/wpAnnot.ml", line 1307, characters 12-28
  Called from file "src/plugins/wp/wpAnnot.ml", line 1320, characters 16-68
  Called from file "src/plugins/wp/Generator.ml", line 109, characters 4-67
  Called from file "map.ml", line 291, characters 20-25
  Called from file "src/plugins/wp/Generator.ml", line 137, characters 4-39
  Called from file "src/plugins/wp/register.ml", line 686, characters 15-40
  Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17
  Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48
  Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
  Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
  Called from file "queue.ml", line 105, characters 6-15
  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
  
  Unexpected error (Stack overflow).
  Please report as 'crash' at http://bts.frama-c.com/.
  Your Frama-C version is 18.0 (Argon).
  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 Files
  • c file icon tmp.c (293 bytes) 2018-12-28 00:58 - 
    #define NULL 0

struct list {
  struct list *next;
  int value;
};

/*@ predicate valid_list{L}(struct list * l) =  \true; */

/*@ requires valid_list(l); */
struct list * e_get(struct list * l, int n){
  return
    ( l == NULL || n < 0 ) ? NULL : 
    ( n == 0 ? l : e_get(l->next, n-1) );
}
    c file icon tmp.c (293 bytes) 2018-12-28 00:58 +

-Relationships
+Relationships

-Notes

~0006979

AllanBlanchard (developer)

2020-09-09 16:21

 Fixed in the upcoming version of Frama-C.
+Notes

-Issue History
Date Modified Username Field Change
2018-12-28 00:58 frederic.loulergue@nau.edu New Issue
2018-12-28 00:58 frederic.loulergue@nau.edu Status new => assigned
2018-12-28 00:58 frederic.loulergue@nau.edu Assigned To => correnson
2018-12-28 00:58 frederic.loulergue@nau.edu File Added: tmp.c
2019-10-17 15:35 correnson Status assigned => acknowledged
2020-09-09 16:21 AllanBlanchard Note Added: 0006979
2020-09-09 16:21 AllanBlanchard Status acknowledged => resolved
2020-09-09 16:21 AllanBlanchard Resolution open => fixed
+Issue History