Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] usage of why-dp
- Subject: [Frama-c-discuss] usage of why-dp
- From: stephane.duprat at atosorigin.com (Stéphane DUPRAT)
- Date: Tue, 12 May 2009 16:50:19 +0200
Hi, why-dp encapsulates calls of the solvers, but wich solver is called ? Does it depends on the suffix of the obligation file (ex: alt-ergo for .why file) ? I've seen the -smt-solver <solver> option, but what is "solver" : a command line or an id ? regards, St?phane -- ----------------------------------------------- Stephane DUPRAT Innovation et Bureau m?thode R?gion Midi-Pyr?n?es - Agence de Toulouse 6 Impasse Alice Guy B.P. 43045 31024 - Toulouse Cedex 03 T?l : 05 34 36 32 78 Fax : 05 34 36 31 00 mailto :stephane.duprat at atosorigin.com ======================================================================= Ce message electronique est confidentiel. Il peut contenir des informations protegees par le secret professionnel, le secret de fabrication ou autres regles legales. Si vous recevez ce message par erreur, il vous est interdit de le reproduire ou de le distribuer en tout ou en partie, ou de le divulguer de quelque maniere que ce soit a quelque personne que ce soit. Nous vous prions de bien vouloir en informer Atos Origin, par telephone ou par retour d'e-mail puis de detruire le message et toutes copies de votre systeme informatique. Le contenu de ce message ne reflete pas necessairement ni les opinions d'Atos Origin ni celle des membres de son groupe. Bien que l'emetteur de ce message ait fait tout son possible pour maintenir son systeme informatique sans virus, il ne peut garantir que cette transmission ne comporte aucun virus et il ne pourra etre tenu pour responsable de quelque dommage que ce soit resultant de la transmission d'un virus. ======================================================================= This electronic transmission is confidential. It may contain information that is covered by legal professional privilege, work product immunity or other legal rules. If you have received this transmission in error, you must not copy or distribute this message or any part of it or otherwise disclose its contents to anyone. Please notify Atos Origin Legal Services by telephone or return E-mail, and then delete this transmission and any copies of it from your computer system. The views expressed in this electronic transmission do not necessarily reflect those of Atos Origin SA or any member of its group. Although the sender endeavours to maintain a computer virus free network, the sender does not warrant that this transmission is virus free and will not be liable for any damages resulting from any virus transmitted. =======================================================================
- Follow-Ups:
- [Frama-c-discuss] usage of why-dp
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] usage of why-dp
- Prev by Date: [Frama-c-discuss] Jessie plug-in
- Next by Date: [Frama-c-discuss] usage of why-dp
- Previous by thread: [Frama-c-discuss] Loop invariants
- Next by thread: [Frama-c-discuss] usage of why-dp
- Index(es):