Translation of tsets
ID0001389: This issue was created automatically from Mantis Issue 1389. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001389 | Frama-C | Plug-in > wp | public | 2013-04-15 | 2013-04-16 |
| Reporter | signoles | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Some tsets are not yet properly translated by Wp. Here is an example which expresses that the first n-th indexes of an array are equal to 0 (the ensures clause):
/@ requires n >= 0; @ requires \valid(t+(0..n-1)); @ ensures \result != 0 <==> t[0..n-1] == 0; @ assigns \nothing; @/ int all_zeros(int t[], int n);