--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2016 ---
Many Thanks for the quick replies. Wanted to know whether Jessie plug-in is able to handle trigonometric functions? If so, can I use Jessie with Coq? Thanks Prasuna 2016-07-11 15:30 GMT+05:30 <frama-c-discuss-request at lists.gforge.inria.fr>: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. JFLA 2017 : premier appel à communications (SIGNOLES Julien) > 2. A problem with math functions (Prasuna Saka) > 3. Re: A problem with math functions (Loïc Correnson) > 4. Re: A problem with math functions (Claude Marché) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 10 Jul 2016 18:19:51 +0000 > From: SIGNOLES Julien <julien.signoles at cea.fr> > To: "frama-c-discuss at lists.gforge.inria.fr" > <frama-c-discuss at lists.gforge.inria.fr> > Subject: [Frama-c-discuss] JFLA 2017 : premier appel à communications > Message-ID: > <D8D4FC26B114714EB1FAE173346799BB2C1B447F at EXDAG0-A1.intra.cea.fr> > Content-Type: text/plain; charset="iso-8859-1" > > [ This message is intentionally written in French. ] > > * Merci de faire circuler : premier appel à communications * > > JFLA'2017 (http://jfla.inria.fr/2017/) > > Journées Francophones des Langages Applicatifs > > dans les Pyrénées, du 4 au 7 janvier 2017 > > > Dates importantes > ----------------- > > 25 septembre 2016 : date limite de soumission des résumés > 09 octobre 2016 : date limite de soumission des articles > 18 novembre 2016 : notification aux auteurs > 27 novembre 2016 : remise des articles définitifs > 04 au 07 janvier 2017 : journées > > Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles > ont pour ambition de couvrir les domaines des langages applicatifs, de > la preuve formelle, de la vérification de programmes, et des objets > mathématiques qui sous-tendent ces outils. Ces domaines doivent être > pris au sens large : nous souhaitons promouvoir les ponts entre > les différentes thématiques. > > . Langages fonctionnels et applicatifs : sémantique, compilation, > optimisation, typage, mesures, extensions par d'autres paradigmes. > > . Assistants de preuve : implémentation, nouvelles tactiques, > développements présentant un intérêt technique ou méthodologique. > > . Logique, correspondance de Curry-Howard, réalisabilité, extraction > de programmes, modèles. > > . Spécification, prototypage, développements formels d'algorithmes. > > . Vérification de programmes ou de modèles, méthode déductive, > interprétation abstraite, raffinement. > > . Utilisation industrielle des langages fonctionnels et applicatifs, > ou des méthodes issues des preuves formelles, outils pour le web. > > Les articles soumis aux JFLA sont relus par au moins deux personnes > s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques > des relecteurs sont toujours bienveillantes et la plupart du temps > encourageantes et constructives, même en cas de rejet. > > Il n'y a donc pas de raison de ne pas soumettre aux JFLA ! > > Cours invités > ------------- > > . Guillaume Burel (ENSIIE) > sur "Dedukti, un vérificateur de preuve universel" (titre exact à > préciser) > > . Benjamin Canou (OCamlPro SAS) > sur "comment programmer en OCaml aujourd'hui" (titre exact à préciser) > > Exposés invités > ------------- > > . Stéphane Lescuyer et Florence Plateau (Prove and Run) > sur "langage, prouveur et autres outils dédiés à la preuve d'un > micro-noyau" > (titre exact à préciser) > > . second orateur invité à préciser > > Comité de programme > ------------------- > > Julien Signoles CEA LIST (président) > Sylvie Boldo Inria Saclay-Ãle de France, LRI (vice-présidente) > June Andronick Data61/CSIRO et UNSW > Anne-Gwenn Bosser ENIB, Lab-STICC > Thomas Gazagnaire Docker > Mohamed Iguernlala OCamlPro SAS > Frédéric Loulergue Université d'Orléans > Laurent Mounier Verimag, Université Grenoble Alpes > François Pottier Inria Paris > Sylvain Salvati Inria Bordeaux-Sud Ouest > Mihaela Sighireanu IRIF, Université Paris 7 > Francesco Zappa Nardeli Inria Paris > > Soumissions > ----------- > > Nous acceptons deux types de soumissions : > > . Article de recherche de quinze pages au plus, portant sur des > travaux originaux. Nous acceptons des travaux en cours, pour lesquels > l'aspect recherche n'est pas entièrement finalisé. > > . Article court de six pages au plus, pour décrire un prototype, > faire la démonstration d'un outil, rechercher de l'aide pour résoudre > un problème particulier, ou reparler d'un papier déjà publié. > > Dans tous les cas, la forme de l'article devra soignée. Les articles > sélectionnés seront publiés dans les actes de la conférence, et les > auteurs seront invités à faire une présentation lors des journées, > de vingt-cinq minutes pour les articles longs et de quinze minutes pour > les courts. > > L'article peut être rédigé en anglais, auquel cas la présentation devra > être effectuée en français. Néanmoins, dans le cas où il s'agit d'une > republication au format court d'un article déjà publié, la publication > doit être en français et la publication originale en anglais. > > Le style LaTeX est imposé : > > http://jfla.inria.fr/2017/actes.sty > > date limite de soumission des résumés : 25 septembre 2016 > date limite de soumission des articles : 09 octobre 2016 > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160710/f8012b98/attachment-0001.html > > > > ------------------------------ > > Message: 2 > Date: Mon, 11 Jul 2016 11:26:24 +0530 > From: Prasuna Saka <prasuna.drdo at gmail.com> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: [Frama-c-discuss] A problem with math functions > Message-ID: > < > CAA80GKO_sieHDpu3-1E_sTE1TgU0Lw+BwkVNLbia8t0+v_CCsQ at mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi, > > I am trying to solve a simple problem having math function "cos". In the > annotations, I have used the built-in function \cos. However, when run with > WP plug-in using the Frama-C Neon Version, following error is thrown : > > [wp} user error: Builtin \cos(real) not defined > [wp] failure: Logic \cos undefined. > > Please let em know the reason for the above errors. How do I make the > built-in function available at run-time. > > Thanks & Regards, > > Prasuna > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/d30e47da/attachment-0001.html > > > > ------------------------------ > > Message: 3 > Date: Mon, 11 Jul 2016 09:30:58 +0200 > From: Loïc Correnson <loic.correnson at cea.fr> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] A problem with math functions > Message-ID: <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F at cea.fr> > Content-Type: text/plain; charset=utf-8 > > > [wp} user error: Builtin \cos(real) not defined > > [wp] failure: Logic \cos undefined. > > We simply did not implement all built-ins in WP. > One reason is that many SMT solvers (if not all) lack interesting > properties about trigonometry. > > Workarounds: > - either use another name, like âcosâ, and declare it using standard ACSL > « logic real cos(real x); » within an axiomatic bloc, and add desired > axioms and lemmas ; > - or use a WP driver (WP manual § 2.4.10, p28) to bind `\cos` to some > symbol in your favorite SMT solver (or Coq or Why3) ; for instance, see > how we handle the â\maxâ function in '$(frama-c > -print-share-path)/wp/wp.driverâ > > In all cases, consider using -wp-model float > > L. > > > > > ------------------------------ > > Message: 4 > Date: Mon, 11 Jul 2016 10:36:47 +0200 > From: Claude Marché <Claude.Marche at inria.fr> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] A problem with math functions > Message-ID: <57835A9F.2080702 at inria.fr> > Content-Type: text/plain; charset=utf-8 > > > > Le 11/07/2016 09:30, Loïc Correnson a écrit : > > One reason is that many SMT solvers (if not all) lack interesting > properties about trigonometry. > > Yes, as far as I know, no SMT solver know about trigonometry. But there > are other provers available as Why3 back-end that do, and Why3 drivers > indeed know how to use them : MetiTarski, Coq, Isabelle/HOL > > For proving floating-point programs correct w.r.t a specification > involving real numbers, it is mandatory to use provers outside the SMT > world. > > See for examples http://toccata.lri.fr/gallery/fp.en.html > > > - Claude > > -- > Claude Marché | tel: +33 1 69 15 66 08 > INRIA Saclay - Ãle-de-France | > Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > ------------------------------ > > End of Frama-c-discuss Digest, Vol 97, Issue 4 > ********************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/deb68f9e/attachment-0001.html>