--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ignoring status of type invariant



At Mon, 21 Apr 2014 18:52:00 +0200,
David MENTR? wrote:
> 
> Hello,
> 
> 2014-04-21 18:34, Marko Sch?tz Schmuck:
> > Why is the type invariant ignored?
> 
> Depending on plug-in, some ACSL features are not supported. Please refer 
> to the corresponding plug-in manual to see which ACSL features are 
> supported or not.

I was expecting POs to be generated in WP for the type invariant...

I checked the WP Manual but didn't find anything on type invariants.

Best regards,

Marko

> > What do I need to do so it is no longer ignored?
> 
> You cannot do much.
> 
> Sincerely yours,
> david
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140421/8a36e078/attachment.pgp>