--- layout: fc_discuss_archives title: Message 133 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assigns clause



Hello,

2013/9/25 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> We have tried to run the specification suggested, but it did not work, the
> GWhy GUI did not open. It showed the following message
> [kernel] user error: syntax error while parsing annotation
>

[kernel] indicates that the error lies in the kernel, i.e. Frama-C
itself can't parse the specification. requires inside behaviors are
supported since Frama-C Carbon IIRC. In any case, as mentioned by
Dillon, they are supported in Fluorine.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile