Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002144Frama-CPlug-in > wppublic2015-07-07 03:282016-01-26 09:00
Reporterdcok@grammatech.com 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSWindowsOS Version7
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002144: crash in presence of \result in assigns
DescriptionRunning frama-c -wp on the following program crashes:
/*@
requires \true;
assigns ((char*)\result)[..];
*/
void* f();

void m() {
    f();
}

With the following error output message:

[kernel] preprocessing with "gcc -C -E -I. -I../GTACSLSpecs/libc -IC:/cygwin/usr/local/share/frama-c/libc -D__FC_MACHDEP_X86_64 -dD C/Users/jrobbins/Desktop/speedy/trunk/annotations/SpecsTests/tests/TEST.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function m
[wp] failure: No function in frame 'Pre f'
[kernel] Current source was: C/Users/jrobbins/Desktop/speedy/trunk/annotations/SpecsTests/tests/TEST.c:8
         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/LogicSemantics.ml", line 221, characters 11-22
         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/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 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 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 713, characters 20-38
         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/LogicSemantics.ml", line 803, characters 2-15
         Called from file "list.ml", line 55, characters 20-23
         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/cfgWP.ml", line 972, characters 23-68
         Called from file "src/wp/cfgWP.ml", line 979, characters 19-52
         Called from file "src/wp/cfgWP.ml", line 1062, characters 15-67
         Called from file "src/wp/Warning.ml", line 155, characters 14-18
         Called from file "src/wp/cfgWP.ml", line 1099, characters 23-207
         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/calculus.ml", line 448, characters 14-224
         Called from file "src/wp/calculus.ml", line 595, characters 10-57
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 579, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 574, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 699, characters 40-59
         Called from file "set.ml", line 304, 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 "map.ml", line 168, characters 10-18
         Called from file "src/wp/calculus.ml", line 699, characters 4-64
         Called from file "src/wp/calculus.ml", line 745, characters 19-51
         Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
         Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
         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
(0006006)
correnson (manager)
2015-08-18 16:52

Presence of \result in assigns is not handled correctly.
(0006009)
correnson (manager)
2015-08-19 12:26

logic variable holding result was incorrectly generated twice.

- Issue History
Date Modified Username Field Change
2015-07-07 03:28 dcok@grammatech.com New Issue
2015-07-07 03:28 dcok@grammatech.com Status new => assigned
2015-07-07 03:28 dcok@grammatech.com Assigned To => correnson
2015-08-18 16:52 correnson Note Added: 0006006
2015-08-18 16:52 correnson Status assigned => acknowledged
2015-08-19 12:26 correnson Note Added: 0006009
2015-08-19 12:26 correnson Status acknowledged => resolved
2015-08-19 12:26 correnson Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-01-26 09:00 signoles Summary crash => crash in presence of \result in assigns


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker