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 September 2013

• Main index
• Thread index for September 2013

---

• [Frama-c-discuss] wp vs. jessie?
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] installation on Ubuntu
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Proving a simple property on bitshift with WP
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] WP (v <= INT32_MIN) causing Inconsistent assumptions
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] installation on Ubuntu
  • From: jorge.adriano at gmail.com (Jorge Adriano Branco Aires)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] JFLA 2014 - Troisieme appel a Communication
  • From: Christine.Tasson at pps.univ-paris-diderot.fr (Christine Tasson)
• [Frama-c-discuss] Assignments proof
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Assignments proof
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Assignments proof
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Assignments proof
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] How to use the frama-c builtins programmatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] <CAA1cxuiRnanxWHJHhXFpRV9G3+pwnFbnNG9zQrCsx3PHQq+fdA@mail.gmail.com>
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] How to use the frama-c builtins programmatically? (David Yang)
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] How to reply a specific topic without opening a new topic.
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Assignments proof
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: moy at adacore.com (Yannick Moy)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Assignments proof
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Introductory slides on Frama-C
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] How would one annotate a function in an external header?
  • From: sstewartgallus00 at mylangara.bc.ca (Steven Stewart-Gallus)
• [Frama-c-discuss] How would one annotate a function in an external header?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] How would one annotate a function in an external header?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] How would one annotate a function in an external header?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Which version of Frama-C/Why to use PVS ? (Jessie or WP)
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] Which version of Frama-C/Why to use PVS ? (Jessie or WP)
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] How would one annotate a function in an external header?
  • From: sstewartgallus00 at mylangara.bc.ca (Steven Stewart-Gallus)
• [Frama-c-discuss] Which version of Frama-C/Why to use PVS ? (Jessie or WP)
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] WP: assigns needed to prove function contract?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] WP: assigns needed to prove function contract?
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] WP: assigns needed to prove function contract?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Proving a simple property on bitshift with WP
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Syntax of annotations in ghost code?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Proving a simple property on bitshift with WP
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] WP: assigns needed to prove function contract?
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Syntax of annotations in ghost code?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Proving a simple property on bitshift with WP
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Syntax of annotations in ghost code?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] List of pre-requsts for frama-c-Fluorine
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] List of pre-requests for frama-c-Fluorine
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] How to ignore Incompatible declarations without emitting errors?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to ignore Incompatible declarations without emitting errors?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without, emitting errors?" (David MENTRE)
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: abiao.yang at gmail.com (David)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to determine a function is non determine function or not programmatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to determine a function is non determine function or not programmatically?
  • From: anne.pacalet at free.fr (Anne Pacalet)
• [Frama-c-discuss] How to determine a function is non determine function or not programmatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] How to obtain a base variable's original variable?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] PVS TCC problem
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [Why3-club] PVS TCC problem
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] How to obtain a base variable's original variable?
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: richard.bonichon at gmail.com (Richard Bonichon)
• [Frama-c-discuss] Shouldn't Frama-C assume main's arguments are valid?
  • From: sstewartgallus00 at mylangara.bc.ca (Steven Stewart-Gallus)
• [Frama-c-discuss] Shouldn't Frama-C assume main's arguments are valid?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] How to obtain a base variable's original variable?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Whether could I know in advance it would have errors before adding a file (Kernel.Files.add)?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] nondeterminism
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] nondeterminism
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Whether could I know in advance it would have errors before adding a file (Kernel.Files.add)?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Whether could I know in advance it would have errors before adding a file (Kernel.Files.add)?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] [Why3-club] PVS TCC problem
  • From: Jean-Christophe.Filliatre at lri.fr (Jean-Christophe Filliatre)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Whether could I know in advance it would have errors before adding a file (Kernel.Files.add)?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Patch for ocaml 4.01.0
  • From: loganjerry at gmail.com (Jerry James)
• [Frama-c-discuss] Patch for ocaml 4.01.0
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] [Jessie] loop invariant
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Jessie3 detecting issue Z3,3.2
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] Jessie3 detecting issue Z3,3.2
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: anne.pacalet at free.fr (Anne Pacalet)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] E-ACSL v0.3
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] E-ACSL v0.3
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Assigns clause
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] RE : E-ACSL v0.3
  • From: julien.signoles at cea.fr (SIGNOLES Julien)
• [Frama-c-discuss] Assigns clause
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Assigns clause
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Assigns clause
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Assigns clause
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Assigns clause
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] JFLA 2014 - Denier appel et nouvelles dates de soumission
  • From: Christine.Tasson at pps.univ-paris-diderot.fr (Christine Tasson)
• [Frama-c-discuss] Gappa prover installation
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Gappa prover installation
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] Gappa prover installation
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Provers versions
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Provers versions
  • From: richard.bonichon at gmail.com (Richard Bonichon)
• [Frama-c-discuss] Provers versions
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: anne.pacalet at free.fr (Anne Pacalet)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: stephane.duprat at atos.net (DUPRAT Stephane)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Provers versions
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] New version of Jessie
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)

---

Mail converted by MHonArc