Goto outside of a block with assigns property
ID0000776: This issue was created automatically from Mantis Issue 776. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000776 | Frama-C | Kernel | public | 2011-04-04 | 2011-04-05 |
| Reporter | Anne | Assigned To | - | Resolution | duplicate |
| Priority | normal | Severity | crash | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
I not really sure of the title, but I get: $ frama-c toto.c [kernel] preprocessing with "gcc -C -E -I. toto.c" Erreur de segmentation
with the following file :
int X; void f (int c) { //@ assigns X; if (c) { X++; if (X > 0) goto L; X++; }
L: ; }