Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #116

Closed
Open
Created Nov 13, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

crash

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


Id Project Category View Due Date Updated
ID0002409 Frama-C Plug-in > wp public 2018-11-13 2019-10-17
Reporter hugo.gimbert Assigned To correnson Resolution won't fix
Priority normal Severity crash Reproducibility always
Platform macosx OS mojave OS Version 10.14.1
Product Version Frama-C 17-Chlorine Target Version - Fixed in Version -

Description :

frama-c -wp somme.c

with somme.c containing

/*@ logic integer f(integer k) = k;

lemma sumint: \forall int n; n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2; */

leads to crash

Trace below

Additional Information :

[kernel] Parsing somme.c (with preprocessing) [wp] Failure: Unbound logic variable 'f' [kernel] Current source was: somme.c:4 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16 Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38 Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32 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 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35 Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23 Called from file "list.ml", line 88, characters 20-23 Called from file "list.ml", line 88, characters 32-39 Called from file "list.ml", line 88, characters 32-39 Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32 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 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35 Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23 Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 931, 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 35-46 Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51 Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62 Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 931, 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 35-46 Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60 Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104 Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46 Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42 Called from file "map.ml", line 295, characters 20-25 Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59 Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48 Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47 Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45 Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36 Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202 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 19-28 Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36 Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023 Called from file "src/plugins/wp/register.ml", line 689, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48 Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 302, 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 791, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8

Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Chlorine-20180502. 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 hugo-9:TP3 gimbert$ cat somme.c /*@ logic integer f(integer k) = k;

lemma sumint: \forall int n; n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2; */

Attachments

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