Issues · pub / frama-c · GitLab

ltl does not accept state charts with transitions invoking dynamic function pointers

#2033 · created Jun 01, 2012 by mantis-gitlab-migration bug wp
- CLOSED
- 5
updated Apr 15, 2021
WP doesn't warn about volatile variables

#1024 · created Jun 06, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Multiple branches to a label/loop entries crashes wp

#1960 · created Oct 13, 2012 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
Problem with _Bool(when casting to int or with ?:)

#1000 · created Jul 21, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
insufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operator

#878 · created Dec 11, 2014 by Jochen Burghardt bug confirmed wp
- CLOSED
- 3
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
applicability of Coq proof script depends on order of include files

#368 · created Feb 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
Creating a pointer to a local causes valid pointers above it to lose thier valid status

#425 · created Jun 21, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
translation to why3 of int* argument to logic function

#371 · created Feb 02, 2017 by Jochen Burghardt bug confirmed wp
- CLOSED
- 6
updated Apr 15, 2021
WP crashes on \floor builtin

#959 · created Oct 12, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas

#946 · created Dec 02, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C GUI discards candidate coq proof

#1240 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
assigns crash on incorrect locations

#1001 · created Jul 17, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
Able to assert a false statement

#803 · created Mar 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 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
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
zombie processes (again)

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

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