--- layout: fc_discuss_archives title: Message 103 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/Jessie: memory set problem



I had a similar problem with this code:


#pragma JessieIntegerModel(exact)

//@  assigns *q;
void Copy(int *p, int *q)
{
  *q = *p;
}


void foo(int a[]) {
  Copy(&a[0], &a[1]);
}


File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed
Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v       -locs tst4.cloc tst4.jc