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.

Old Frama-C mailing list archives for March 2009

• Main index
• Thread index for March 2009

---

• [Frama-c-discuss] Frama-C compilation: questions on APRON, test error and missing plugin?
  • From: dmentre at linux-france.org (David MENTRE)
• No subject
  • From: bogus@does.not.exist.com ()
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issue with non terminating function
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issue with non terminating function
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issue with non terminating function
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issue with non terminating function
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Issue with offset in static strings
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] RE : [Jessie] Issue with behavior in contracts
  • From: virgile.prevosto at cea.fr (PREVOSTO Virgile)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] extracting information from jessie-gui
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: nshmyrev at yandex.ru (Nickolay V. Shmyrev)
• [Frama-c-discuss] Issue with modulo over unsigned int
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Issue with behavior in contracts
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] an example involving floats
  • From: david.delmas at airbus.com (David DELMAS)
• [Frama-c-discuss] an example involving floats
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Jessie regions
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
• [Frama-c-discuss] Saving state of gWhy and reloading it later?
  • From: dmentre at linux-france.org (David MENTRE)
• No subject
  • From: bogus@does.not.exist.com ()
• [Frama-c-discuss] Jessie regions
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Jessie regions
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
• [Frama-c-discuss] Frama-c fails to open a C file
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Frama-c fails to open a C file
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Verifying recursive functions
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-c fails to open a C file
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Dead code that shouldn't be
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Dead code that shouldn't be
  • From: pascal.cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: julien.signoles at cea.fr (Julien SIGNOLES)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Semantics of Jessie icons?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: Anne.Pacalet at sophia.inria.fr (Anne.Pacalet at sophia.inria.fr)
• [Frama-c-discuss] How to prove "offset_min(char_xP_stdin_8_alloc_table, stdin) <= 0"?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Verifying recursive functions
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Verifying recursive functions
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Verifying recursive functions
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Verifying recursive functions
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Verifying recursive functions
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Global initialization of variables not taken into account?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Verifying recursive functions
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
• [Frama-c-discuss] Issue to prove a precondition for user call
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issue to prove a precondition for user call
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Jessie subprocess failed
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Jessie subprocess failed
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Jessie subprocess failed
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Jessie subprocess failed
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Jessie subprocess failed
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Verifying recursive functions
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Verifying recursive functions
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Verifying recursive functions
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Verifying recursive functions
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] Problem with simple search programm
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Setup of a Frama-C wiki?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Setup of a Frama-C wiki?
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Issue to express assigns on arrays
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparisonexample
  • From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
• [Frama-c-discuss] A toy electronic voting software checked with Frama-C
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Semantics of Jessie icons?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Semantics of Jessie icons?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Semantics of Jessie icons?
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] HELP FRAMA-C
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
• [Frama-c-discuss] Frama-C/Jessie: memory set problem
  • From: dillon.pariente at dassault-aviation.fr (Dillon Pariente)
• [Frama-c-discuss] Unable to prove assigns clause for array
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C/Jessie: memory set problem
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Installation problem
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Installation problem
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C: #define not taken into account into annotations
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Frama-C: #define not taken into account into annotations
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] Frama-C: #define not taken into account into annotations
  • From: david.delmas at airbus.com (David DELMAS)
• [Frama-c-discuss] Frama-C: #define not taken into account intoannotations
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)

---

Mail converted by MHonArc