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 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