Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001279Frama-CPlug-in > wppublic2012-10-13 03:352012-10-13 03:35
Reportersjw 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001279: Multiple branches to a label/loop entries crashes wp
DescriptionThe following code:

/*@ ensures \result == x; */
int test(int x)
{
 again:
    if (x > 10)
        goto again;

    if (x > 10)
        goto again;

    return x;
}

gives

$ ~/frama-c/bin/frama-c -wp doublegoto.c
[kernel] preprocessing with "gcc -C -E -I. doublegoto.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: CFG node <loop-1> has 2 successors instead of 1
...

This is caused by the use of a list for loop headers in cil2cfg.ml. The
attached patch fixes this by using a set of nodes.
TagsNo tags attached.
Attached Filesdiff file icon goto.diff [^] (2,356 bytes) 2012-10-13 03:35 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-10-13 03:35 sjw New Issue
2012-10-13 03:35 sjw Status new => assigned
2012-10-13 03:35 sjw Assigned To => correnson
2012-10-13 03:35 sjw File Added: goto.diff


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker