Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #306
Closed
Open
Issue created Jul 31, 2017 by Jochen Burghardt@burghardt

repeated predicate definitions in separate file cause crash

ID0002322: This issue was created automatically from Mantis Issue 2322. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002322 Frama-C Kernel public 2017-07-31 2017-12-06
Reporter Jochen Assigned To virgile Resolution fixed
Priority normal Severity crash Reproducibility always
Platform Phosphorus-20170501-beta1 OS xubuntu OS Version -
Product Version Frama-C 15-Phosphorus Target Version - Fixed in Version Frama-C 16-Sulfur

Description :

Running '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.

Attachments

  • part.c
  • whole.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking