Issues · pub / frama-c · GitLab

Error when struct has no members

#612 · created Jul 15, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 4
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
Zombie processes

#491 · created Sep 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
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
Slow in proof obligation generation

#598 · created Sep 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
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
suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations

#593 · created Sep 21, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."

#592 · created Sep 21, 2015 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
Unable to prove things that are provable, gets confused

#584 · created Oct 18, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
Crash on loop with global assigns and per-behavior assigns

#109 · created Oct 19, 2015 by Boris Yakobowski critical wp
- CLOSED
- 2
updated Feb 22, 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
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
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
Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)

#578 · created Dec 03, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 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
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))

#499 · created Jan 22, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated May 18, 2021
provide option "-wp-lemma"

#522 · created Jan 23, 2016 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021
zombie processes (again)

#526 · created Feb 01, 2016 by Jens Gerlach bug confirmed wp
- CLOSED
- 5
updated Apr 15, 2021
WP crashes with \pointer_comparable

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

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