Issues · pub / frama-c · GitLab

Translation of tsets

#1900 · opened Apr 15, 2013 by Julien Signoles enhancement wp
- CLOSED
- 6
updated Apr 15, 2021
WP-Plugin crashes due to an internal error when terms of sets during union have different types

#919 · opened Dec 22, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
quantifiers over logic types do not restrict to valid instances

#91 · opened Jan 30, 2020 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Apr 15, 2021
Eprover in Frama-C 20 beta

#103 · opened Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
statement contract apparently confuses parser

#324 · opened May 11, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
false postcondition shouldn't be verified in default memory-model setting

#333 · opened Jun 15, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 2021
naming the default behavior influences proven obligations

#336 · opened Jun 01, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · opened May 08, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
Some ACSL mathematical functions crash WP

#351 · opened May 10, 2017 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
axiom about bounds of lsl result needed in the long run

#352 · opened May 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4

#353 · opened Mar 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · opened Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
suggestion: translate axioms and implication premises in forward order to coq

#360 · opened Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
unable to use lemma separated_region

#620 · opened Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
Frama-C sleeps too much when discharging trivial goals

#369 · opened Feb 13, 2017 by mantis-gitlab-migration enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
WP inserts unwanted new lines into Coq proofs

#385 · opened Jan 02, 2017 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
Why3 warning

#387 · opened Dec 16, 2016 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
more prover processes run than expected

#388 · opened Dec 15, 2016 by Jens Gerlach bug wp
- CLOSED
- 4
updated Apr 15, 2021
error in Coq file generation

#405 · opened Dec 03, 2016 by Alain Giorgetti bug wp
- CLOSED
- 1
updated Apr 15, 2021
Nested scopes may cause issues with the validity of created pointers

#409 · opened Aug 17, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021

Prev
1
2
3
4
5
…
12
Next