--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2020 ---
Hello, You may have a look to previous related discussions about: * deprecated aspect of native coq prover Subjet: [Frama-c-discuss] Frama-C native:coq Date: Mon, 10 Feb 2020 13:04:18 +0000 From: Gerlach, Jens <jens.gerlach at fokus.fraunhofer.de> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> * how to perform coq proofs Subjet: [Frama-c-discuss] ACSL by Example (version 21.1.0) Date: Thu, 9 Jul 2020 17:45:53 +0000 From: Gerlach, Jens <jens.gerlach at fokus.fraunhofer.de> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> I hope that using the same method as the one used in ASCL by example will help you, Patrick. Le 16/08/2020 à 23:21, Matthias Güdemann a écrit : > Hello, > > I am looking at the WP plugin to prove lemmas for functions. In the > case that the automatic provers do not manage to prove a PO, how does > one proceed to get a script/.v file to be used in Coq to complete a > proof externally? > It seems that most what I found on this topic uses native Coq which is > deprecated now. > Maybe someone can point me to the current documentation for this. The > WP manual presents tip for proof scripts but that seems to be for the > interactive proof editor of the Frama-C GUI. > > Thank you for your help, > > Best regards > Matthias > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- Patrick Baudin, DILS/LSL, Bât. 862, Point Courrier n° 174 Institut CARNOT CEA LIST, CEA Saclay Nano-INNOV, 91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072 -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200817/259f3539/attachment.html>