Issues · pub / frama-c · GitLab

Suggest to supply values of global consts to provers

#498 · created May 10, 2012 by Jochen Burghardt enhancement wp
- CLOSED
- 13
updated Feb 22, 2021
missing lower bound of ACSL operator ".." not detected by Magnesium

#494 · created Jun 13, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 6
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
Zombie processes

#491 · created Sep 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
alt-ergo: undefined symbol andb

#489 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 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
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
Logic with read clauses can have their values invalidated by writes to separated memory locations

#410 · created Aug 08, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Aug 05, 2021
Nested scopes may cause issues with the validity of created pointers

#409 · created Aug 17, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
error in Coq file generation

#405 · created Dec 03, 2016 by Alain Giorgetti bug wp
- CLOSED
- 1
updated Apr 15, 2021
workaround for coq-8.5.1 issue?

#403 · created Jun 16, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 7
updated Feb 22, 2021
"Builtin already registered" after Reparse

#398 · created Jul 30, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Feb 22, 2021
Switch statements seem to be unsound

#397 · created Aug 19, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Frama-C is unsound when employing both alt-ergo and cvc4

#394 · created Jun 30, 2016 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021
more prover processes run than expected

#388 · created Dec 15, 2016 by Jens Gerlach bug wp
- CLOSED
- 4
updated Apr 15, 2021
Why3 warning

#387 · created Dec 16, 2016 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
WP inserts unwanted new lines into Coq proofs

#385 · created Jan 02, 2017 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
coq 8.5: cannot find Memory.v

#384 · created Feb 11, 2016 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 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
Frama-C sleeps too much when discharging trivial goals

#369 · created Feb 13, 2017 by mantis-gitlab-migration enhancement wp
- CLOSED
- 1
updated Apr 15, 2021

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