Issues · pub / frama-c · GitLab

unprovable PO in function manipulating structs - issue with Qed's simplifications

#1818 · created Nov 08, 2013 by Virgile Prevosto bug wp
- CLOSED
- 5
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
Prove of \false

#126 · created Feb 16, 2019 by Jens Gerlach bug wp
- CLOSED
- 6
updated Apr 15, 2021
Implicit casting from integer to real causes failure in WP proof generation

#413 · created Jul 29, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 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
suspicious axiomatization of included,zrange,zunion in .sx file

#2087 · created Dec 15, 2011 by Jochen Burghardt wp
- CLOSED
- 2
updated Apr 15, 2021
warn on stderr about current restrictions, and list them in WP manual

#2043 · created Nov 04, 2011 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
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

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