--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on February 2011 ---
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