2021-01-26 06:45 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001389Frama-CPlug-in > wppublic2013-04-16 17:07
Reportersignoles 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0001389: Translation of tsets
DescriptionSome 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);
TagsNo tags attached.
Attached Files

-Relationships
related to 0001428assignedcorrenson Range verification in 2D-array fails 
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2013-04-15 14:35 signoles New Issue
2013-04-15 14:35 signoles Status new => assigned
2013-04-15 14:35 signoles Assigned To => correnson
2013-04-16 17:07 signoles Summary Traduction of tsets => Translation of tsets
2013-05-24 14:14 signoles Relationship added related to 0001428
+Issue History