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-06-17 21:34
Reporterjwaksbaum 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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
There are no notes attached to this issue.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker