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

[Frama-c-discuss] jessie - struct as parameter to logic functions



Hello,

using the new Boron version of Frama-C I found a change to the Beryllium2
version I would like to ask about.
Below a simplified example.

typedef struct Test{
  int a;
} Test;

/*@ predicate test_a{L}(Test test) =
      (test.a == 0) || (test.a == 1);
 */

Trying to run Jessie on it returns:
failure: Jessie plugin does not support struct or union as parameter to
logic functions. Please use a pointer instead.

In Beryllium it was possible to have structs as a parameter in a predicate
like this.

Even though using pointers instead works, I wonder if there is a reason why
this has changed?

Kind Regards,
Kerstin