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<length;i++ )
        b[i]=a[i];

}
int main()
{

    int array_int[10]={1,2,3,4,5,6,7,8,9,0};
    int* first_int = &array_int[0];
    
    char array_char_to_int[50];
    copy(first_int, 10, array_char_to_int);
    
    //create pointers to the same array,
    //shift the second by one byte
    
    int* first_char_to_int = &array_char_to_int[0];
    int* first_char_to_int_shift = &array_char_to_int[1];
    
    //call copy to the same array
    //why error
    copy(first_char_to_int, 10, first_char_to_int_shift);
    

    return 0;
}

By the way, assigns b[0..length-1]; is never provable.

Cheers

Christoph
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