2021-01-25 14:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002385Frama-CPlug-in > wppublic2019-10-17 18:00
Assigned Tocorrenson 
StatusclosedResolutionno change required 
Product Version 
Target VersionFixed in Version 
Summary0002385: Auto-generated assigns clause for a void* argument crashes wp
DescriptionWhen 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 Reproducerun `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 InformationThe 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
TagsNo tags attached.
Attached Files




correnson (manager)

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...

-Issue History
Date Modified Username Field Change
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
2019-10-17 17:08 correnson Status assigned => resolved
2019-10-17 17:08 correnson Resolution open => no change required
2019-10-17 18:00 signoles Status resolved => closed
+Issue History