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

• Main index
• Thread index for October 2013

---

• [Frama-c-discuss] New version of Jessie
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] Argumentos do main VS Ferramentas Estaticas
  • From: lucboluc at gmail.com (Lucas Barbosa)
• [Frama-c-discuss] Argumentos do main VS Ferramentas Estaticas
  • From: ismael.vb at gmail.com (Ismael Vilas Boas)
• [Frama-c-discuss] z3 failure
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] z3 failure
  • From: kornevgen at gmail.com (Eugene Kornykhin)
• [Frama-c-discuss] z3 failure
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Argumentos do main VS Ferramentas Estaticas
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] z3 failure
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: kornevgen at gmail.com (Eugene Kornykhin)
• [Frama-c-discuss] z3 failure
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] full IEEE754 model in Jessie
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] New version of Jessie
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
• [Frama-c-discuss] z3 failure
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] [Why3-club] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] [Why3-club] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Mac install
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] examples
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] Mac install
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] new GWhy - statistics
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] Mac install
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] euklid.c
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] Mac install
  • From: mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala)
• [Frama-c-discuss] Mac install
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] examples
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] examples
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] new GWhy - statistics
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] euklid.c
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Mac install
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] euklid.c
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] euklid.c
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] value analysis of function contain shift operations seems unable to stop
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Mac install
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
• [Frama-c-discuss] Mac install
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] euklid.c
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] value analysis of function contain shift operations seems unable to stop
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] value analysis of function contain shift operations seems unable to stop
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] about volatile variable in value analysis plugin and "Volatile" plugin
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [FEATURE REQUEST] Context insensitive for Value analysis plugin
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
• [Frama-c-discuss] Jessie plugin - more than 6,000 VCs generated
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] euklid.c
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: alle.iot at gmail.com (Alessio Iotti)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
• [Frama-c-discuss] examples
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] examples
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: nnarai at gmail.com (Nanci Naomi)
• [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: francois.bobot at cea.fr (François Bobot)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: moy at adacore.com (Yannick Moy)
• [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Array problem - Jessie plugin
  • From: luciana.burgareli at gmail.com (Luciana Burgareli)
• [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Array problem - Jessie plugin
  • From: kornevgen at gmail.com (Eugene Kornykhin)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: alle.iot at gmail.com (Alessio Iotti)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: alle.iot at gmail.com (Alessio Iotti)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Array problem - Jessie plugin
  • From: luciana.burgareli at gmail.com (Luciana Burgareli)
• [Frama-c-discuss] Problems with Nitrogen/Fluorine
  • From: alle.iot at gmail.com (Alessio Iotti)
• [Frama-c-discuss] how does Frama-C infer missing invariants?
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] Verification conditions left unproven by automatic prover
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] how does Frama-C infer missing invariants?
  • From: moy at adacore.com (Yannick Moy)
• [Frama-c-discuss] Array problem - Jessie plugin
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Verification conditions left unproven by automatic prover
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] how does Frama-C infer missing invariants?
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] How Jessie plug-in handles aliasing of pointers
  • From: moy at adacore.com (Yannick Moy)
• [Frama-c-discuss] Verification conditions left unproven by automatic prover
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] Frama-c - wp on Windows/Cygwin
  • From: dcok at grammatech.com (David Cok)
• [Frama-c-discuss] [FEATURE REQUEST] Context insensitive for Value analysis plugin
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
• [Frama-c-discuss] Problems with ensures
  • From: alle.iot at gmail.com (Alessio Iotti)
• [Frama-c-discuss] Problems with ensures
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Array problem - Jessie plugin
  • From: luciana.burgareli at gmail.com (Luciana Burgareli)
• [Frama-c-discuss] sums of arrays
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] label L required?
  • From: siegel at udel.edu (Stephen Siegel)
• [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: nnarai at gmail.com (Nanci Naomi)

---

Mail converted by MHonArc