Issues · pub / frama-c · GitLab

WP ignores some goals when 'initialized' is used in hypotheses

#776 · created Mar 04, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
WP-Plugin crashes due to an internal error

#701 · created Sep 12, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Feb 22, 2021
CVC4 results are not displayed in the GUI

#682 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
*i == *j cannot be proven from i == j

#631 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
*off == off_cpy cannot be proven just after the assignment *off = off_cpy

#628 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Range of remainder of two positive integers, wrong and missing assertions.

#627 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
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
deficient axioms

#617 · created Jun 29, 2015 by David Cok bug wp
- CLOSED
- 1
updated Feb 22, 2021
WP output of loop variant's goal doesn't have location of loop variant

#569 · created Dec 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Crash with \is_infinite

#550 · created Feb 24, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
Incorrect result with X modulo 1

#547 · created Jul 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
assumes clause and labels

#544 · created Dec 27, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021
memory leak (endless recursion?) caused by erroneous c program

#534 · created Nov 02, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
provide option "-wp-lemma"

#522 · created Jan 23, 2016 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021
Reals are bad encoded for coq

#504 · created Mar 03, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 0
updated Feb 22, 2021
coq fails to compile Cint because Zbits is not found

#501 · created Sep 02, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
missing lower bound of ACSL operator ".." not detected by Magnesium

#494 · created Jun 13, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 6
updated Feb 22, 2021
workaround for coq-8.5.1 issue?

#403 · created Jun 16, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 7
updated Feb 22, 2021
Switch statements seem to be unsound

#397 · created Aug 19, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Frama-C is unsound when employing both alt-ergo and cvc4

#394 · created Jun 30, 2016 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021

Prev
1
…
7
8
9
10
11
12
13
Next