--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2010 ---
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