Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000031Frama-CPlug-in > jessiepublic2009-04-07 14:092009-06-17 13:30
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000031: Why- error :-jessie-no-regions and assigns does not work
Description[bug 7242 of old bts reported by Christoph Weber] Hello, for the following function I get the error: in memory set (mem-field(int_M),a_20), (mem-field(int_M),b_21) File "jc/jc_interp_misc.ml", line 707, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Asse rtion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs i nt_alignment.cloc int_alignment.jc ====== /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (b, 0, length-1); ensures \forall integer i; 0 <= i < length ==> b[i] == a[i]; */ void copy (int* a, int length, int* b) { int i=0; /*@ loop invariant 0 <= i <= length; loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k]; loop assigns b[0 .. i-1]; */ for(;i
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-07 14:09 virgile New Issue
2009-04-07 15:42 signoles Status new => acknowledged
2009-04-10 10:07 signoles Status acknowledged => assigned
2009-04-10 10:07 signoles Assigned To => cmarche
2009-06-17 13:30 signoles Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker