Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #1023

WP crash when type casting in lemma

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


Id Project Category View Due Date Updated
ID0001804 Frama-C Plug-in > wp public 2014-06-06 2014-06-06
Reporter Ian Assigned To correnson Resolution open
Priority normal Severity crash Reproducibility always
Platform - OS Ubuntu OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

When using Typed+cast, a cast in a lemma can cause wp to crash. In the below example, removing the lemma will cause the assert to validate.

Steps To Reproduce :

Create file ptr_cast.c : /*@ lemma valid_pointers: \forall int **ptr; sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr); */

void f(int **ptr){ //@ assert sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr); }

Run : frama-c -cpp-command 'gcc -C -E' -pp-annot -wp -wp-model Typed+cast ptr_cast.c

Receive output : [kernel] preprocessing with "gcc -C -E -dD ptr_cast.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage ptr_cast.c:4:[wp] warning: Cast with incompatible pointers types (source: int**) (target: sint32*) [wp] failure: Context 'Warning' non-initialized. [kernel] Current source was: ptr_cast.c:7 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "src/wp/Warning.ml", line 117, characters 10-31 Called from file "src/wp/MemTyped.ml", line 799, characters 3-111 Called from file "src/wp/MemVar.ml", line 374, characters 23-51 Called from file "src/wp/Cvalues.ml", line 433, characters 30-42 Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27 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/LogicCompiler.ml", line 358, characters 20-35 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 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/LogicCompiler.ml", line 357, characters 28-51 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 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/LogicCompiler.ml", line 357, characters 28-51 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 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/Lang.ml", line 869, characters 33-38 Re-raised at file "src/wp/Lang.ml", line 870, characters 40-43 Called from file "src/wp/LogicSemantics.ml", line 684, characters 11-54 Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37 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/LogicCompiler.ml", line 326, characters 14-25 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 "src/wp/LogicCompiler.ml", line 401, characters 24-83 Called from file "src/wp/LogicCompiler.ml", line 673, characters 6-97 Called from file "src/wp/LogicCompiler.ml", line 690, characters 19-41 Called from file "src/wp/cfgWP.ml", line 1294, characters 31-42 Called from file "map.ml", line 169, characters 20-25 Called from file "src/wp/cfgWP.ml", line 1369, characters 14-54 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 17-42 Called from file "src/wp/register.ml", line 574, characters 17-24 Re-raised at file "src/wp/register.ml", line 578, characters 29-31 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 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 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8

     Plug-in wp aborted: internal error.
     Please report as 'crash' at http://bts.frama-c.com/.
     Your Frama-C version is Neon-20140301.
     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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking