--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C Carbon and spec_requires.



Hello Kalyan,

Le mer. 16 f?vr. 2011 10:49:48 CET,
Kalyan <kalyan.krishnamani at inria.fr> a ?crit :

> ... (Kernel_function.get_spec kf).spec_requires
> 
> /which no longer seems to work with the Carbon version as I do not see
> spec_requires. May I know the alternative?
> 

Requires are now part of behaviors (field b_requires of the behavior
record type), as in ACSL manual . Clauses that are part of a simple
contract (i.e. not in a named behavior) are in fact placed in a special
behavior. You can retrieve the requires corresponding to this specific
behavior with the function Cil.find_default_requires (and the whole
default behavior with Cil.find_default_behavior).

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98