Frama-C Bug Tracking System - Frama-C
View Issue Details
0001389Frama-CPlug-in > wppublic2013-04-15 14:352013-04-16 17:07
signoles 
correnson 
normalfeatureN/A
assignedopen 
 
 
0001389: Translation of tsets
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);
No tags attached.
related to 0001428assigned correnson Range verification in 2D-array fails 
Issue History
2013-04-15 14:35signolesNew Issue
2013-04-15 14:35signolesStatusnew => assigned
2013-04-15 14:35signolesAssigned To => correnson
2013-04-16 17:07signolesSummaryTraduction of tsets => Translation of tsets
2013-05-24 14:14signolesRelationship addedrelated to 0001428

There are no notes attached to this issue.