Issues · pub / frama-c · GitLab

WP detect a non-natural loop on a do-while(0) loop

#518 · created Aug 19, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 15, 2021
Crash with large array initialisation

#514 · created Mar 18, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Apr 15, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 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
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
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
unable to use lemma separated_region

#620 · created Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
suggestion: translate axioms and implication premises in forward order to coq

#360 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4

#353 · created Mar 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
axiom about bounds of lsl result needed in the long run

#352 · created May 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
Some ACSL mathematical functions crash WP

#351 · created May 10, 2017 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · created May 08, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
naming the default behavior influences proven obligations

#336 · created Jun 01, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
false postcondition shouldn't be verified in default memory-model setting

#333 · created Jun 15, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 2021
statement contract apparently confuses parser

#324 · created May 11, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021

Prev
1
…
7
8
9
10
11
12
13
Next