Evaluation in the logic can cause crashes
ID0001000: This issue was created automatically from Mantis Issue 1000. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001000 | Frama-C | Plug-in > Eva | public | 2011-10-25 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | unable to reproduce |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Evaluation in the logic sometimes causes the warning "using size of void". Worse, this can lead to crashes, as e.g. do_cast raises assert false when it encounters something of type void.
It is not clear how one goes from something that has type void* to something that has type void, but this definitely happens.
Steps To Reproduce :
This example can be used to cause the apparition of the warning
frama-c -val -then -print
void main (int i) { int x=1; while(1) Frama_C_memcpy((void )&x, (void const)&x, i); }
The generated assertion cast the pointer to void*, then does arithmetic on it. This is incorrect.