|Anonymous | Login | Signup for a new account||2019-02-21 11:57 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002385||Frama-C||Plug-in > wp||public||2018-07-05 17:03||2018-07-06 09:38|
|Target Version||Fixed in Version|
|Summary||0002385: Auto-generated assigns clause for a void* argument crashes wp|
|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
|Steps To Reproduce||run `frama-c -wp test2.c` with those 3 provided files|
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
|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
|Tags||No tags attached.|
|Attached Files||assigns.tar.gz [^] (358 bytes) 2018-07-05 17:03|
The invalid « user » input is assigned because, actually, the function is missing any assigns clause.
The warning emitted by the kernel shall triggers some « user review » for verifying that the automatically generated assigns clause is actually meaningful in your context. So this is really some « user » issue.
Of course, we might rephrase the error message from WP by investigating whether the incorrect assign clause was generated or not. But this would be a large amount of work for little productivity gain : the origin of the error is still well identified in current messages. Moreover, the plug-in based architecture of Frama-C makes many of ACSL annotations generated by third-party plug-ins, which is typically the case for assign clauses (eg. we have a non-public « genassigns » plug-in for that) or imported from other kind of specifications (eg. from other specification languages that compiles to ACSL). So, it can be really
difficult to distinguish what was generated from user input than from other sources...
|2018-07-05 17:03||schollet||New Issue|
|2018-07-05 17:03||schollet||Status||new => assigned|
|2018-07-05 17:03||schollet||Assigned To||=> correnson|
|2018-07-05 17:03||schollet||File Added: assigns.tar.gz|
|2018-07-06 09:38||correnson||Note Added: 0006571|
|Copyright © 2000 - 2019 MantisBT Team|