Issues · pub / frama-c · GitLab

False valid with LONG_MIN

#802 · created Mar 06, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Crash when using wpo api get_result

#792 · created May 19, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
Problem when arguments are not used in predicates

#791 · created Apr 30, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Assert erroneously proved valid

#788 · created May 07, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
Frama-C/WP fails to discharge simple bit operation for small integer types

#787 · created Apr 11, 2014 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
Make identifiers in Coq proofs more similar to those from C code

#779 · created Jan 23, 2014 by Jens Gerlach bug wp
- CLOSED
- 4
updated Feb 22, 2021
compatibility between \null in ACSL and NULL in C in wp

#777 · created Feb 17, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
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
Status of POs: the word "interruped" should be "interrupted"

#765 · created Sep 26, 2014 by Richard Bonichon wp
- CLOSED
- 1
updated Feb 22, 2021
Frame Validity

#754 · created Jul 08, 2014 by Loïc Correnson bug wp
- CLOSED
- 2
updated Feb 22, 2021
typo in wp output: "interruped"-->"interrupted"

#753 · created Jul 14, 2014 by Jochen Burghardt wp
- CLOSED
- 2
updated Feb 22, 2021
Frama-C/WP "forgets" a proven assertion

#749 · created Apr 11, 2014 by Jens Gerlach bug wp
- CLOSED
- 5
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
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
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
WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

#635 · created Jun 01, 2015 by Virgile Prevosto bug wp
- CLOSED
- 1
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

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