Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001389Frama-CPlug-in > wppublic2013-04-15 14:352013-04-16 17:07
Reportersignoles 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
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 

-  Notes
There are no notes attached to this issue.

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker