Issues · pub / frama-c · GitLab

assertion failure using memset on a char

#595 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
alt-ergo: undefined symbol andb

#489 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Slow in proof obligation generation

#598 · created Sep 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 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
Zombie processes

#491 · created Sep 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 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
Error when struct has no members

#612 · created Jul 15, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 14, 2021
crash in presence of \result in assigns

#541 · created Jul 07, 2015 by David Cok critical wp
- CLOSED
- 2
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
deficient axioms

#617 · created Jun 29, 2015 by David Cok bug wp
- CLOSED
- 1
updated Feb 22, 2021
requires in beahviors do not behave as expected

#626 · created Jun 12, 2015 by David Cok bug wp
- CLOSED
- 2
updated Feb 22, 2021
Under windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishing

#492 · created Jun 11, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 0
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
Unprovable inequality involving (unsigned) -1

#570 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

#571 · created Jun 02, 2015 by Virgile Prevosto bug wp
- CLOSED
- 1
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
validity of obligation from statement contract depends on whether the statement is enclosed in block {}

#625 · created Jun 01, 2015 by Jochen Burghardt bug wp
- CLOSED
- 3
updated Aug 05, 2021
do ... while{ } loop and -wp-invariants option

#624 · created May 19, 2015 by Lionel Blatter bug wp
- CLOSED
- 1
updated Feb 22, 2021

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