--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Distiction between int a[] and int *a



Hi,

in the reply to my bug report http://bts.frama-c.com/view.php?id=537 I
learned that Boron introduced a distinction between 

int a[]

and

int *a.

What is the difference between the two and when does which form have to
be used?

I noticed that the Sorted predicate from the Jessie tutorial

/*@ predicate Sorted{L}(int a[], integer l, integer h) =
  @   \forall integer i; l <= i < h ==> a[i] <= a[i+1] ;
  @*/

causes Jessie to crash.
-- 
Regards,
Boris