Issues · pub / frama-c · GitLab

Issue INSTALL guidance that alt-ergo has to be up-to-date (0.92 apparently)

#2197 · created Dec 16, 2010 by Holger Blasum bug wp
- CLOSED
- 3
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
Error: Unbound value Why3.Whyconf.load_default_config_if_needed 1 of 3 tasks completed

#2548 · created Mar 30, 2021 by Qix confirmed wp
- CLOSED
- 1
- 3
updated Apr 13, 2021
Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems 3 of 3 tasks completed

#41 · created Nov 01, 2020 by Jens Gerlach wp
- CLOSED
- 1
- 28
updated Apr 13, 2021
alt-ergo support in Frama-C 20 beta

#102 · created Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 0
updated Apr 14, 2021
Range verification in 2D-array fails

#1858 · created May 24, 2013 by Allan Blanchard bug wp
- CLOSED
- 2
updated Apr 14, 2021
do { ... } while (0) pattern causes wp to fail

#1816 · created Oct 15, 2012 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Apr 14, 2021
Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579

#582 · created Oct 27, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
WP crashes with \pointer_comparable

#527 · created Feb 03, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
Printing of function types causes a stack overflow

#1959 · created Oct 13, 2012 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 14, 2021
[wp] failure: not an integer (Blob)

#1925 · created Dec 15, 2012 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
Use of very large real constants cause failures in proof generation in WP

#507 · created Jun 14, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
Error when struct has no members

#612 · created Jul 15, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 14, 2021
unprovable PO in function manipulating structs - issue with Qed's simplifications

#1818 · created Nov 08, 2013 by Virgile Prevosto bug wp
- CLOSED
- 5
updated Apr 14, 2021
bound variable names in Coq file depend on unrelated function later in C source code

#601 · created Aug 31, 2015 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Apr 15, 2021
Prove of \false

#126 · created Feb 16, 2019 by Jens Gerlach bug wp
- CLOSED
- 6
updated Apr 15, 2021
Implicit casting from integer to real causes failure in WP proof generation

#413 · created Jul 29, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32

#579 · created Nov 30, 2015 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
suspicious axiomatization of included,zrange,zunion in .sx file

#2087 · created Dec 15, 2011 by Jochen Burghardt wp
- CLOSED
- 2
updated Apr 15, 2021
warn on stderr about current restrictions, and list them in WP manual

#2043 · created Nov 04, 2011 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021

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