crash when unbound variable
ID0000190: This issue was created automatically from Mantis Issue 190. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000190 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-09-02 |
Reporter | lukaszc | Assigned To | patrick | Resolution | fixed |
Priority | normal | Severity | crash | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | - | Target Version | - | Fixed in Version | Frama-C Beryllium-20090901 |
Description :
"frama-c -slice-rd y -pp-annot test.c" results in a crash
test.c
int x(int y, int z) { /@ slice pragma expr y == 1; / //@ assert y == 1; //@ assert y + z == 3; return 2yz1(); }
int main() { x(1,2); return 0; }
int z1() { return 1; }