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 January 2014

• Main index
• Thread index for January 2014

---

• [Frama-c-discuss] How to modify the value state of a statement for re-running the value analysis
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could it possible to change the if statement state then re-do value analysis programmatically?
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
• [Frama-c-discuss] How to modify the value state of a statement for re-running the value analysis
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] How to modify the value state of a statement for re-running the value analysis
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could I get the statement that caused the dead code programatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could I get the statement that caused the dead code programatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] Could it possible to change the if statement state then re-do value analysis programmatically?
  • From: matthieu.lemerre at cea.fr (Matthieu Lemerre)
• [Frama-c-discuss] Could it possible to change the if statement state then re-do value analysis programmatically?
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
• [Frama-c-discuss] how to operate on the type of Locations.Zone.map_t ?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] How to get the defined locations or varinfos of a corresponding statement by using the value state programatically?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] How to discard a visiting glob?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] RE : How to discard a visiting glob?
  • From: julien.signoles at cea.fr (SIGNOLES Julien)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] RE : How to discard a visiting glob?
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] RE : RE : How to discard a visiting glob?
  • From: julien.signoles at cea.fr (SIGNOLES Julien)
• [Frama-c-discuss] some questions about the "-lib-entry -main " option while value analysis a partial application
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: kahl at cas.mcmaster.ca (Wolfram Kahl)
• [Frama-c-discuss] some questions about the "-lib-entry -main " option while value analysis a partial application
  • From: dmentre at linux-france.org (David MENTRÉ)
• [Frama-c-discuss] some questions about the "-lib-entry -main " option while value analysis a partial application
  • From: abiao.yang at gmail.com (David Yang)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: dmentre at linux-france.org (David MENTRÉ)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: kahl at cas.mcmaster.ca (Wolfram Kahl)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: matthieu.lemerre at cea.fr (Matthieu Lemerre)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
• [Frama-c-discuss] Frama-c: WP issues
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Can i specify/proove a function to be "just called"?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] MThread
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] MThread
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-c: WP issues
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Proving Memory Safety of String Algorithms without Providing Loop Invariants
  • From: giesl at informatik.rwth-aachen.de (Juergen Giesl)
• [Frama-c-discuss] Proving Memory Safety of String Algorithms without Providing Loop Invariants
  • From: loganjerry at gmail.com (Jerry James)
• [Frama-c-discuss] Proving Memory Safety of String Algorithms without Providing Loop Invariants
  • From: giesl at informatik.rwth-aachen.de (Juergen Giesl)
• [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-c: WP issues
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: der.herr at hofr.at (Nicholas Mc Guire)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: der.herr at hofr.at (Nicholas Mc Guire)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: nicky.williams at cea.fr (Nicky Williams)
• [Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-C: Detecting unreachable code?
  • From: nicky.williams at cea.fr (Nicky Williams)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: der.herr at hofr.at (Nicholas Mc Guire)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: nicky.williams at cea.fr (Nicky Williams)
• [Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-C: Detecting unreachable code?
  • From: nicky.williams at cea.fr (Nicky Williams)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
• [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] problem with matrix pointer
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] WP - How to represent duplicate assumes?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] WP - How to represent duplicate assumes?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Value Analysis: signed_overflow in addition to division_by_zero warning
  • From: marcel.gehrke at tu-harburg.de (Marcel Gehrke)
• [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] Value Analysis: signed_overflow in addition to division_by_zero warning
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
• [Frama-c-discuss] Array size in Frama-C
  • From: phunghuuphu at gmail.com (Phu H. Phung)
• [Frama-c-discuss] Value Analysis: signed_overflow in addition to division_by_zero warning
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] two-dimensional array requires clause
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] A significant case study using Frama-C
  • From: Claude.Marche at inria.fr (Claude Marché)
• [Frama-c-discuss] two-dimensional array requires clause
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] two-dimensional array requires clause
  • From: dragan.stosic at gmail.com (Dragan)
• [Frama-c-discuss] two-dimensional array requires clause
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] Frama-C: Detecting unreachable code?
  • From: boris at yakobowski.org (Boris Yakobowski)
• [Frama-c-discuss] A significant case study using Frama-C
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] assigns \from supported in WP?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] WP: Max_List syntax error
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
• [Frama-c-discuss] assigns \from supported in WP?
  • From: loic.correnson at cea.fr (Loïc Correnson)
• [Frama-c-discuss] Frama-C and Keil C51
  • From: ajf at inti.gob.ar (Alejandro J. Formichelli)

---

Mail converted by MHonArc