Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2535

Closed
Open
Created Apr 07, 2009 by Virgile Prevosto@virgileOwner

Why- error :-jessie-no-regions and assigns does not work

ID0000031: This issue was created automatically from Mantis Issue 31. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000031 Frama-C Plug-in > jessie public 2009-04-07 2009-06-17
Reporter virgile Assigned To cmarche Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Lithium-20081201 Target Version - Fixed in Version -

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking