--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2016 ---
Thanks Mr.Claude. Will try with Jessie. On Monday, July 11, 2016, <frama-c-discuss-request at lists.gforge.inria.fr> wrote: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr <javascript:;> > > 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 <javascript:;> > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr <javascript:;> > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Re: Frama-c-discuss Digest, Vol 97, Issue 4 (Prasuna Saka) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 11 Jul 2016 15:43:01 +0530 > From: Prasuna Saka <prasuna.drdo at gmail.com <javascript:;>> > To: frama-c-discuss at lists.gforge.inria.fr <javascript:;> > Subject: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 4 > Message-ID: > < > CAA80GKPysEEhSBTeXdKHER1nHgZz1Q0it_DpRcww8bMhWU+azQ at mail.gmail.com > <javascript:;>> > Content-Type: text/plain; charset="utf-8" > > 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 > <javascript:;>>: > > > Send Frama-c-discuss mailing list submissions to > > frama-c-discuss at lists.gforge.inria.fr <javascript:;> > > > > 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 <javascript:;> > > > > You can reach the person managing the list at > > frama-c-discuss-owner at lists.gforge.inria.fr <javascript:;> > > > > 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 <javascript:;>> > > To: "frama-c-discuss at lists.gforge.inria.fr <javascript:;>" > > <frama-c-discuss at lists.gforge.inria.fr <javascript:;>> > > Subject: [Frama-c-discuss] JFLA 2017 : premier appel à communications > > Message-ID: > > <D8D4FC26B114714EB1FAE173346799BB2C1B447F at EXDAG0-A1.intra.cea.fr > <javascript:;>> > > 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 <javascript:;>> > > To: frama-c-discuss at lists.gforge.inria.fr <javascript:;> > > Subject: [Frama-c-discuss] A problem with math functions > > Message-ID: > > < > > CAA80GKO_sieHDpu3-1E_sTE1TgU0Lw+BwkVNLbia8t0+v_CCsQ at mail.gmail.com > <javascript:;>> > > 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 <javascript:;>> > > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr > <javascript:;>> > > Subject: Re: [Frama-c-discuss] A problem with math functions > > Message-ID: <F3ED5FA7-7D8D-41B6-BCD2-A5D2F5A3982F at cea.fr <javascript:;>> > > 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 <javascript:;>> > > To: frama-c-discuss at lists.gforge.inria.fr <javascript:;> > > Subject: Re: [Frama-c-discuss] A problem with math functions > > Message-ID: <57835A9F.2080702 at inria.fr <javascript:;>> > > 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 <javascript:;> > > 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.html > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr <javascript:;> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > ------------------------------ > > End of Frama-c-discuss Digest, Vol 97, Issue 5 > ********************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160711/7b6e58e2/attachment-0001.html>