assigns nothing is not possible to proof, if malloc is not in a same function
ID0001032:
**This issue was created automatically from Mantis Issue 1032. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001032 | Frama-C | Plug-in > jessie | public | 2011-11-29 | 2011-11-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jessie_user | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The 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.
## Attachments
- [assigns_simpl1.c](/uploads/9df893964885643167b882651e866919/assigns_simpl1.c)
- [proofs.v](/uploads/9cf2ae078572f0ebd45b721b7a695936/proofs.v)
issue