Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #113
Closed
Open
Issue created Jul 05, 2018 by mantis-gitlab-migration@mantis-gitlab-migration

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

Attachments

  • assigns.tar.gz
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking