Issues · pub / frama-c · GitLab

invalid statement contract ("assigns") verified with CVC4 under strange circumstances

#599 · created Apr 30, 2015 by Jochen Burghardt bug wp
- CLOSED
- 14
updated Feb 22, 2021
normalization of "assigns" in statement contract doens't cope with introduced auxiliary variables

#622 · created Apr 09, 2015 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Mar 30, 2021
readability of coq(?) names

#104 · created Mar 31, 2015 by Jens Gerlach bug wp
- CLOSED
- 6
updated Feb 22, 2021
False valid with LONG_MIN

#802 · created Mar 06, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Able to assert a false statement

#803 · created Mar 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
Crash with \is_infinite

#550 · created Feb 24, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
for a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather than to 1 (as in C)

#677 · created Feb 19, 2015 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
use of void* leads to type error in the PO generation

#554 · created Feb 16, 2015 by Virgile Prevosto bug wp
- CLOSED
- 2
updated Feb 22, 2021
Frama-C does not work with versions of Why3 newer than 0.83

#711 · created Jan 27, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Sessions and WP do not interact properly

#618 · created Jan 06, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
unable to use lemma separated_region

#620 · created Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
assumes clause and labels

#544 · created Dec 27, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021
WP-Plugin crashes due to an internal error when terms of sets during union have different types

#919 · created Dec 22, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
Option -wp-qed-checks generates invalid At-Ergo files

#932 · created Dec 15, 2014 by David Mentré bug wp
- CLOSED
- 1
updated Feb 22, 2021
insufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operator

#878 · created Dec 11, 2014 by Jochen Burghardt bug confirmed wp
- CLOSED
- 3
updated Apr 15, 2021
Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas

#946 · created Dec 02, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
suggest to provide a command-line option for checking if every loop or recursion has a termination measuring function attached

#951 · created Nov 27, 2014 by Jochen Burghardt enhancement kernel wp
- CLOSED
- 2
updated Jan 10, 2022
obligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo nevertheless

#948 · created Nov 27, 2014 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 29, 2021
assertion not proved anymore by WP

#931 · created Oct 23, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
WP crashes on \floor builtin

#959 · created Oct 12, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021

Prev
1
…
3
4
5
6
7
8
9
10
11
…
13
Next