Issues · pub / frama-c · GitLab

Unprovable inequality involving (unsigned) -1

#570 · created Jun 04, 2015 by mantis-gitlab-migration 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
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
Number of discharged Qed goals counted multiple times

#552 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 3
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
crash in presence of \result in assigns

#541 · created Jul 07, 2015 by David Cok critical 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
WP crashes with \pointer_comparable

#527 · created Feb 03, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
zombie processes (again)

#526 · created Feb 01, 2016 by Jens Gerlach bug confirmed wp
- CLOSED
- 5
updated Apr 15, 2021
provide option "-wp-lemma"

#522 · created Jan 23, 2016 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021
WP detect a non-natural loop on a do-while(0) loop

#518 · created Aug 19, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 15, 2021
Crash with large array initialisation

#514 · created Mar 18, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Apr 15, 2021
Make find(1) command POSIX-compliant

#513 · created Apr 09, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Aug 05, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 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
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

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