--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Memory Problems with Lithium



Hi, 

I just wanted to add, that next to the bug with preservation of loop invariants, the handling of pointer dereferencing is very annoying.

I get the green bullets for this section only if I add

loop invariant \valid(it1)&&\valid(it2);

That seems very obsolete (at least for a user), i hope this wont be permanent

Cheers

Christoph





On Thu, Oct 30, 2008 at 9:01 AM, Christoph Weber <Christoph.Weber@first.fraunhofer.de> wrote:

  Hello again,

  Thank You and granulations for the latest release.

  But I have some problems to get started. Lets start with an example.
  Following Function in separate files:


  fill.h:

  /*@
  requires valid_range(first, last);
  requires \valid_range(first, 0, last-first -1);
  behavior is_not_empty:
  assumes not_empty_range(first, last);
  ensures \forall integer i;
  0 <= i < last-first ==> first[i] == value;
  */
  void fill (int* first, int* last, int value );

  fill.c:

  #include
  "fill.h" 
  void fill (int* first, int* last, int value ) 
  {
  int* it = first;
  /*@
  loop invariant first <= it <= last;
  loop invariant \forall integer k; 0 <= k < it - first ==> first[k] == value;
  */
  while (it != last)
  *it++ = value;
  }

  I call Jessie:
  frama-c -jessie-analysis -jessie-int-model exact -jessie-no-regions -jessie-gui fill.c

  Now the problems:
  -the loop invariant cannot be preserved, => am I missing an option or an annotation (it went fine on H and He)
  -the declared int* it causes problems in pointer dereferencing
  -Z3, CVC3, and Yices get stuck and wont abort, the timeout never worked on any release yet (on my pc)


  I hope for help

  Cheers


  _______________________________________________
  Frama-c-discuss mailing list
  Frama-c-discuss@lists.gforge.inria.fr
  http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss





-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081104/1ef41b69/attachment.htm