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

• Main index
• Thread index for December 2009

---

• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: benjamin.monate at cea.fr (Benjamin Monate)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] New Why Release on Mac OS Snow Leopard
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
• [Frama-c-discuss] RE : New Why Release on Mac OS Snow Leopard
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] RE : RE : New Why Release on Mac OS Snow Leopard
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] RE : RE : New Why Release on Mac OS Snow Leopard
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
• [Frama-c-discuss] RE : RE : New Why Release on Mac OS Snow Leopard
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] New Why 2.22 binaries for Mac OS Snow Leopard
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-c
  • From: carlitoon at gmail.com (Carlos Carloto)
• [Frama-c-discuss] Problem with bitwise xor
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] New Why 2.22 binaries for Mac OS Snow Leopard
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
• [Frama-c-discuss] Why/Jessie plugin version 2.22 is out
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Problem with memset
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] New Why 2.22 binaries for Mac OS Snow Leopard
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
• [Frama-c-discuss] New Why 2.22 binaries for Mac OS Snow Leopard
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] How to use ACSL in GUI and How to generate Coq code
  • From: jianzhou at seas.upenn.edu (Jianzhou Zhao)
• [Frama-c-discuss] How to use ACSL in GUI and How to generate Coqcode
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] How to use ACSL in GUI and How to generate Coqcode
  • From: jianzhou at seas.upenn.edu (Jianzhou Zhao)
• [Frama-c-discuss] Problem with memset
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] How to use ACSL in GUI and How to generateCoqcode
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Foudantions of Frama-C framework
  • From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
• [Frama-c-discuss] How to use ACSL in GUI and How to generateCoqcode
  • From: jianzhou at seas.upenn.edu (Jianzhou Zhao)
• [Frama-c-discuss] Problem with memset
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Foudantions of Frama-C framework
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Foudantions of Frama-C framework
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Different contracts in declaration and implementation
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] usage of Frama_C_memcpy
  • From: stephane.duprat at atosorigin.com (Stéphane Duprat)
• [Frama-c-discuss] Foudantions of Frama-C framework
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Problem with memset
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Problem with bitwise xor
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Lemma from ACSL doc doesn't verify
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] usage of Frama_C_memcpy
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C User Manual
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Problem with bitwise xor
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] usage of Frama_C_memcpy
  • From: stephane.duprat at atosorigin.com (Stephane DUPRAT)
• [Frama-c-discuss] Lemma from ACSL doc doesn't verify
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] usage of Frama_C_memcpy
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] usage of Frama_C_memcpy
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Problem with memset
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Lemma from ACSL doc doesn't verify
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Problem with bitwise xor
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Lemma from ACSL doc doesn't verify
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Problem with memset
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Lemma from ACSL doc doesn't verify
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Why/Jessie plugin version 2.23 is out
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Running ocaml on cygwin
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] how padding are introduced by Frama-C
  • From: stephane.duprat at atosorigin.com (Stéphane Duprat)
• [Frama-c-discuss] how padding are introduced by Frama-C
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] how padding are introduced by Frama-C
  • From: stephane.duprat at atosorigin.com (Stephane DUPRAT)
• [Frama-c-discuss] problem with verify a list
  • From: chengeng4001 at gmail.com (geng chen)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] unproven VC with newer why version
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] unproven VC with newer why version
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] unproven VC with newer why version
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] unproven VC with newer why version
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: dvidal at ekkyo.com (Damien Vidal)
• [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] unproven VC with newer why version
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Frama-C doesn't warn me about the illegal assignment of a variable
  • From: dvidal at ekkyo.com (Damien Vidal)
• [Frama-c-discuss] unproven VC with newer why version
  • From: dmentre at linux-france.org (David MENTRE)
• [Frama-c-discuss] unproven VC with newer why version
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Help with proving post-conditions
  • From: mtorl at hotmail.com (Murat Torlakcik)
• [Frama-c-discuss] unproven VC with newer why version
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Help with proving post-conditions
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Help with proving post-conditions
  • From: mtorl at hotmail.com (Murat)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Res: Foudantions of Frama-C framework
  • From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
• [Frama-c-discuss] History of the discussion list
  • From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
• [Frama-c-discuss] History of the discussion list
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Jessie global variables and functions
  • From: dak at adelard.com (Damien Karkinsky)
• [Frama-c-discuss] Jessie global variables and functions
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Res: Jessie global variables and functions
  • From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
• [Frama-c-discuss] Jessie global variables and functions
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] unproven VC with newer why version
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Res: Jessie global variables and functions
  • From: Claude.Marche at inria.fr (Claude Marche)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Discrepancy between Jessie gui and command line when using yices
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] problem with verify a list
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Help with proving post-conditions
  • From: mtorl at hotmail.com (Murat)
• [Frama-c-discuss] Help with proving post-conditions
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Help with proving post-conditions
  • From: mtorl at hotmail.com (Murat)
• [Frama-c-discuss] Help with proving post-conditions
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: dak at adelard.com (Damien Karkinsky)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] relationship of separated and restrict qualifier
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] relationship of separated and restrict qualifier
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
• [Frama-c-discuss] Jessie and -no-regions
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: dak at adelard.com (Damien Karkinsky)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] Proof conditions with simple pointer assignment
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
• [Frama-c-discuss] Problems with value analysis
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
• [Frama-c-discuss] arithmetic overflow unsigned int
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Problems with value analysis
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] problem with verify a list
  • From: chengeng4001 at gmail.com (geng chen)
• [Frama-c-discuss] problem with verify a list
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
• [Frama-c-discuss] Problems with value analysis
  • From: Julien.Signoles at cea.fr (Julien Signoles)
• [Frama-c-discuss] problem with verify a list
  • From: chengeng4001 at gmail.com (geng chen)
• [Frama-c-discuss] unproven VC with newer why version
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
• [Frama-c-discuss] Debugging huge theories
  • From: yegor.derevenets at gmail.com (Yegor Derevenets)
• [Frama-c-discuss] Debugging huge theories
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
• [Frama-c-discuss] Debugging huge theories
  • From: yegor.derevenets at gmail.com (Yegor Derevenets)
• [Frama-c-discuss] Loop Termination Challenge
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
• [Frama-c-discuss] Loop Termination Challenge
  • From: Jean-Christophe.Filliatre at lri.fr (Jean-Christophe.Filliatre at lri.fr)
• [Frama-c-discuss] Debugging huge theories
  • From: yegor.derevenets at gmail.com (Yegor Derevenets)

---

Mail converted by MHonArc