Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002385Frama-CPlug-in > wppublic2018-07-05 17:032018-07-06 09:38
Reporterschollet 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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

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
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 Filesgz file icon assigns.tar.gz [^] (358 bytes) 2018-07-05 17:03

- Relationships

-  Notes
(0006571)
correnson (manager)
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...

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker