Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002455Frama-CPlug-in > wppublic2019-06-17 21:342019-10-17 17:57
Assigned Tocorrenson 
Platformi386OSDarwinOS Version18.6.0
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002455: malloc breaks reasoning about assigns
DescriptionIf a function contains a call to malloc, WP fails to verify its assigns clause. This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
Steps To Reproduce# Verify a function with a call to malloc and assigns \nothing frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f # Verify a function with the same contract as malloc, which only calls malloc frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper
TagsNo tags attached.
Attached Filesc file icon example.c [^] (799 bytes) 2019-06-17 21:34 [Show Content]

- Relationships

-  Notes
correnson (manager)
2019-10-17 14:52

Allocation clauses are still not yet supported in WP, although it is implementable in the Typed memory model. This is on the roadmap, feel free to participate in if you want to help.
correnson (manager)
2019-10-17 14:52

On the roadmap.

- Issue History
Date Modified Username Field Change
2019-06-17 21:34 jwaksbaum New Issue
2019-06-17 21:34 jwaksbaum Status new => assigned
2019-06-17 21:34 jwaksbaum Assigned To => correnson
2019-06-17 21:34 jwaksbaum File Added: example.c
2019-10-17 14:52 correnson Note Added: 0006889
2019-10-17 14:52 correnson Note Added: 0006890
2019-10-17 14:52 correnson Status assigned => resolved
2019-10-17 14:52 correnson Resolution open => suspended
2019-10-17 17:56 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker