Issues · pub / frama-c · GitLab

undefined (or built-in?) predicate "global" in proof obligation

#1880 · created Dec 01, 2011 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Feb 22, 2021
Wrong WP computation when calling a function with behaviors (assigns problem ?)

#1883 · created Oct 20, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
unproven property used in a behavior in Typed model

#1888 · created Nov 06, 2012 by Stephane Duprat bug wp
- CLOSED
- 1
updated Feb 22, 2021
proc name in assigns clause causes crash

#1889 · created Nov 01, 2012 by Jochen Burghardt critical wp
- CLOSED
- 1
updated Feb 22, 2021
performance problem about number of fields in structure for struct equality properties

#1895 · created Jan 13, 2013 by Stephane Duprat bug wp
- CLOSED
- 3
updated Feb 22, 2021
Support of \block_length

#1928 · created Jul 29, 2011 by Patrick Baudin bug wp
- CLOSED
- 1
updated Feb 22, 2021
ACSL builtins

#1929 · created May 10, 2011 by Loïc Correnson enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
addr_eq versus = and <> in generated axioms access_update, access_update_neq

#1948 · created Mar 12, 2012 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
Signal -7 and then crashed.

#1026 · created Jan 15, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
Crash on loop with global assigns and per-behavior assigns

#109 · created Oct 19, 2015 by Boris Yakobowski critical wp
- CLOSED
- 2
updated Feb 22, 2021
Proof obligations of lemma properties

#1972 · created Jul 28, 2011 by Patrick Baudin bug wp
- CLOSED
- 1
updated Feb 22, 2021
unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?

#1987 · created Nov 28, 2011 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
Information on C type of array is not present (in Coq)

#107 · created Nov 22, 2017 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
Bitwise Operators

#1999 · created Feb 29, 2012 by Loïc Correnson bug wp
- CLOSED
- 2
updated Feb 22, 2021
ACSL label LoopEntry not handled by WP

#1173 · created Jan 30, 2013 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Generate proof obligation for drivers when driver instantiate a logic acsl declaration

#1147 · created Mar 13, 2014 by Jens Gerlach enhancement wp
- 0
updated Feb 22, 2021
Upgrading WP causes crash in Jessie

#2018 · created Jul 02, 2012 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
WP 0.5 crashes with an Unbound label parameter 'Here'

#2039 · created Jan 11, 2012 by Mounir Assaf critical wp
- CLOSED
- 1
updated Feb 22, 2021
Requires of behaviors lost

#2075 · created Nov 30, 2011 by Boris Yakobowski bug wp
- CLOSED
- 3
updated Feb 22, 2021
Testing example which is OK for Jessie-plugin fails with wp-plugin.

#2081 · created Dec 16, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021

Prev
1
2
3
4
5
6
7
8
9
10
…
14
Next