Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001804Frama-CPlug-in > wppublic2014-06-06 17:542014-06-06 17:54
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSUbuntuOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001804: WP crash when type casting in lemma
DescriptionWhen 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 ReproduceCreate 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 [^]
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-06-06 17:54 Ian New Issue
2014-06-06 17:54 Ian Status new => assigned
2014-06-06 17:54 Ian Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker