Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001032Frama-CPlug-in > jessiepublic2011-11-29 17:142011-11-29 17:14
Reporterjessie_user 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001032: assigns nothing is not possible to proof, if malloc is not in a same function
DescriptionThe assigns \nothing clausel is not provable with Jessie, if you use malloc in another function. And it is provable if it is in the same function.
Ex1:
/*@ assigns \nothing;*/ // assigns ok
int* assigns_tm(){
    int* a = malloc (sizeof(int)*10);
    a[0] = 42;
    return a;
}

Ex2:
/*@assigns \nothing;
ensures \valid_range (\result, 0, 10);*/
int* create_ints(){
    return malloc (sizeof(int)*10);
}
/*@ assigns \nothing; //Not possible to prove !
*/
int* assigns_t (){
    int* a = create_ints();
    a[0] = 42;
    return a;
}

Proof for Ex1 with coq is attached.

What possibilities do you have, if you want to prove this function? I know only 3:
1. rewrite my code
2. define yourself something like malloc
3. use \fresh (or \separated)

The best one is 3, but unfortunately Jessie does not implement \fresh and \separated.



TagsNo tags attached.
Attached Filesc file icon assigns_simpl1.c [^] (485 bytes) 2011-11-29 17:14 [Show Content]
? file icon proofs.v [^] (3,131 bytes) 2011-11-29 17:14

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-11-29 17:14 jessie_user New Issue
2011-11-29 17:14 jessie_user Status new => assigned
2011-11-29 17:14 jessie_user Assigned To => cmarche
2011-11-29 17:14 jessie_user File Added: assigns_simpl1.c
2011-11-29 17:14 jessie_user File Added: proofs.v


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker