Auto-generated assigns clause for a void* argument crashes wp
ID0002385: This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| Reporter | schollet | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
Additional Information :
The command run : frama-c -wp test2.c
Error log : [kernel] Parsing test2.c (with preprocessing) [kernel:annot:missing-spec] test2.c:7: Warning: Neither code nor specification for function foo, generating default assigns from the prototype [wp] Warning: Missing RTE guards [wp] test2.c:11: User Error: Invalid infinite range i_0+(0..) [kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui): /*@ assigns *((char *)thing + (0 ..)); assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..)); */
Removing the assigns clause for create stops WP from crashing
Steps To Reproduce :
run frama-c -wp test2.c with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause. Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file