Frama-C Bug Tracking System - Frama-C
View Issue Details
0002455Frama-CPlug-in > wppublic2019-06-17 21:342019-10-17 17:57
jwaksbaum 
correnson 
normalminoralways
closedsuspended 
i386Darwin18.6.0
Frama-C 18-Argon 
 
0002455: malloc breaks reasoning about assigns
If 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.
# 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
No tags attached.
c example.c (799) 2019-06-17 21:34
https://bts.frama-c.com/file_download.php?file_id=1318&type=bug
Issue History
2019-06-17 21:34jwaksbaumNew Issue
2019-06-17 21:34jwaksbaumStatusnew => assigned
2019-06-17 21:34jwaksbaumAssigned To => correnson
2019-06-17 21:34jwaksbaumFile Added: example.c
2019-10-17 14:52corrensonNote Added: 0006889
2019-10-17 14:52corrensonNote Added: 0006890
2019-10-17 14:52corrensonStatusassigned => resolved
2019-10-17 14:52corrensonResolutionopen => suspended
2019-10-17 17:56signolesStatusresolved => closed

Notes
(0006889)
correnson   
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.
(0006890)
correnson   
2019-10-17 14:52   
On the roadmap.