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 June 2009

• Main index
• Thread index for June 2009

---

• [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
  • From: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
• [Frama-c-discuss] Jessie sort specification
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Jessie sort specification
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• No subject
  • From: bogus@does.not.exist.com ()
• No subject
  • From: bogus@does.not.exist.com ()
• [Frama-c-discuss] Jessie sort specification
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Jessie sort specification
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] string functions and how to use jessie_prolog.h ?
  • From: Paolo.Argenton at elsagdatamat.com (Argenton Paolo)
• [Frama-c-discuss] Jessie sort specification
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Jessie sort specification
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: nicolas.stouls at insa-lyon.fr (Nicolas Stouls)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: nicolas.stouls at insa-lyon.fr (Nicolas Stouls)
• [Frama-c-discuss] Precondition for user call (newbye question)
  • From: bashir1961 at gmail.com (Paolo Bashir Argenton)
• [Frama-c-discuss] Precondition for user call (newbye question)
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Precondition for user call (newbye question)
  • From: bashir1961 at gmail.com (Paolo Bashir Argenton)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
• [Frama-c-discuss] Precondition for user call (newbye question)
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: nicolas.stouls at insa-lyon.fr (Nicolas Stouls)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Inductive definition of reachability in array-implemented list.
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
• [Frama-c-discuss] Array elements passed as reference
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Inductive definition of reachability in array-implemented list.
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] Inductive definition of reachability in array-implemented list.
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Inductive definition of reachability inarray-implemented list.
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Inductive definition of reachability inarray-implemented list.
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] [Jessie] pset_disjoint
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] pset_disjoint
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] [Jessie] pset_disjoint
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] [Jessie] pset_disjoint
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] [Jessie] pset_disjoint
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Semantics of \valid
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] A tentative FAQ...
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Semantics of \valid
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] A tentative FAQ...
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
• [Frama-c-discuss] integer overflow
  • From: regehr at cs.utah.edu (John Regehr)
• [Frama-c-discuss] integer overflow
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] integer overflow
  • From: regehr at cs.utah.edu (John Regehr)
• [Frama-c-discuss] integer overflow
  • From: regehr at cs.utah.edu (John Regehr)
• [Frama-c-discuss] Jessie different result with same prover on different OS
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] integer overflow
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] integer overflow
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] integer overflow
  • From: regehr at cs.utah.edu (John Regehr)
• [Frama-c-discuss] integer overflow
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Semantics of \valid
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Semantics of \valid
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Semantics of \valid
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C limit ?
  • From: Emilie.Timbou at continental-corporation.com (Emilie.Timbou at continental-corporation.com)
• [Frama-c-discuss] Frama-C limit ?
  • From: Emilie.Timbou at continental-corporation.com (Emilie.Timbou at continental-corporation.com)
• [Frama-c-discuss] Use of a deprecated function: Dynamic.Main.extend
  • From: stephane.duprat at atosorigin.com (Stéphane Duprat)
• [Frama-c-discuss] Use of a deprecated function: Dynamic.Main.extend
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Use of a deprecated function: Dynamic.Main.extend
  • From: stephane.duprat at atosorigin.com (Stephane DUPRAT)
• [Frama-c-discuss] [Fwd: Re: Use of a deprecated function: Dynamic.Main.extend]
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Jessie Plugin Tutorial
  • From: lc at adelard.com (Lukasz Cyra)
• [Frama-c-discuss] wp calculus
  • From: mauro at bglug.it (Mauro Baluda)
• [Frama-c-discuss] wp calculus
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] wp calculus
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] wp calculus
  • From: mbaluda at gmail.com (Mauro Baluda)
• [Frama-c-discuss] wp calculus
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] wp calculus
  • From: Anne.Pacalet at sophia.inria.fr (Anne.Pacalet at sophia.inria.fr)
• [Frama-c-discuss] wp calculus
  • From: mauro at bglug.it (Mauro Baluda)
• [Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)
  • From: dillon.pariente at dassault-aviation.fr (Dillon Pariente)
• [Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] (no subject)
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] (no subject)
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] (no subject)
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] (no subject)
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Frama-C Beryllium 20090601 Beta 1 release
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] (no subject)
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] (no subject)
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] (no subject)
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Cooperation with Splint
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Cooperation with Splint
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] (no subject)
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Cooperation with Splint
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] Cooperation with Splint
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Frama-C Beryllium 20090601 Beta 1 release
  • From: bashir1961 at gmail.com (Paolo Bashir Argenton)
• [Frama-c-discuss] Frama-C Beryllium 20090601 Beta 1 release
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] Frama-C Beryllium 20090601 Beta 1 release
  • From: bashir1961 at gmail.com (Paolo Bashir Argenton)
• [Frama-c-discuss] Frama-C Beryllium 20090601 Beta 1 release
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Help on handling unknown proof
  • From: tienhm at gmail.com (Tien Hoang Minh)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: ulissesaraujocosta at gmail.com (Ulisses Araújo Costa)
• [Frama-c-discuss] Beryllium beta1 / untyped_metrics plugin example
  • From: stephane.duprat at atosorigin.com (Stéphane Duprat)
• [Frama-c-discuss] Beryllium beta1 / untyped_metrics plugin example
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: ulissesaraujocosta at gmail.com (Ulisses Araújo Costa)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Beryllium beta1 / untyped_metrics plugin example
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: ulissesaraujocosta at gmail.com (Ulisses Araújo Costa)
• [Frama-c-discuss] Beryllium "complete behaviors"
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Beryllium beta1 / untyped_metrics plugin example
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Beryllium beta1 / untyped_metrics plugin example
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Patch for Frama-C-Beryllium-20090601-beta1
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Problem in example of ACSL Implementation
  • From: tienhm at gmail.com (Tien Hoang Minh)
• [Frama-c-discuss] wp calculus
  • From: mauro at bglug.it (Mauro Baluda)
• [Frama-c-discuss] Result icons in Jessie-GUI
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] wp calculus
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
• [Frama-c-discuss] Result icons in Jessie-GUI
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Selection Sort loop-invariant problem
  • From: ulissesaraujocosta at gmail.com (Ulisses Araújo Costa)
• [Frama-c-discuss] Result icons in Jessie-GUI
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)

---

Mail converted by MHonArc