Frama-C Bug Tracking System - Frama-C
View Issue Details
0002385Frama-CPlug-in > wppublic2018-07-05 17:032019-10-17 18:00
closedno change required 
0002385: Auto-generated assigns clause for a void* argument crashes wp
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
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
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
No tags attached.
gz assigns.tar.gz (358) 2018-07-05 17:03
Issue History
2018-07-05 17:03scholletNew Issue
2018-07-05 17:03scholletStatusnew => assigned
2018-07-05 17:03scholletAssigned To => correnson
2018-07-05 17:03scholletFile Added: assigns.tar.gz
2018-07-06 09:38corrensonNote Added: 0006571
2019-10-17 17:08corrensonStatusassigned => resolved
2019-10-17 17:08corrensonResolutionopen => no change required
2019-10-17 18:00signolesStatusresolved => closed

2018-07-06 09:38   
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...