Issues · pub / frama-c · GitLab

statement contract apparently confuses parser

#324 · opened May 11, 2017 by Jochen Burghardt critical wp
- 2
updated Feb 22, 2021
Some ACSL mathematical functions crash WP

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

#352 · opened May 08, 2017 by Jochen Burghardt enhancement wp
- 0
updated Feb 22, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · opened May 08, 2017 by Jochen Burghardt critical wp
- 2
updated Feb 22, 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
- 0
updated Feb 22, 2021
suggestion: translate axioms and implication premises in forward order to coq

#360 · opened Mar 13, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · opened Mar 13, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
Why3ide cannot be opened in this version

#365 · opened Mar 01, 2017 by Pierre Yves Piriou enhancement wp
- 0
updated Feb 22, 2021
lemma tacitly omitted from prover assumptions

#367 · opened Feb 27, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
applicability of Coq proof script depends on order of include files

#368 · opened Feb 16, 2017 by Jochen Burghardt bug wp
- 0
updated Feb 22, 2021
Frama-C sleeps too much when discharging trivial goals

#369 · opened Feb 13, 2017 by mantis-gitlab-migration enhancement wp
- 0
updated Feb 22, 2021
problem with Qed's simplification power

#370 · opened Feb 06, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
Duplicates are created on the tab "Messages"

#318 · opened Feb 03, 2017 by mantis-gitlab-migration enhancement gui
- 3
updated Feb 22, 2021
translation to why3 of int* argument to logic function

#371 · opened Feb 02, 2017 by Jochen Burghardt bug confirmed wp
- 5
updated Feb 22, 2021
It is impossble to change log file without kinds of message changing.

#372 · opened Jan 19, 2017 by mantis-gitlab-migration confirmed enhancement kernel
- 1
updated Feb 22, 2021
WP appears to assume left-to-right evaluation order for int addition

#381 · opened Jan 16, 2017 by Jochen Burghardt bug kernel
- 2
updated Feb 22, 2021
label Pre in function contracts

#386 · opened Jan 02, 2017 by Jens Gerlach ACSL bug kernel
- 0
updated Feb 22, 2021
WP inserts unwanted new lines into Coq proofs

#385 · opened Jan 02, 2017 by Jens Gerlach bug wp
- 0
updated Feb 22, 2021
structure in logic not supported?

#383 · opened Dec 20, 2016 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 2021
Why3 warning

#387 · opened Dec 16, 2016 by Jens Gerlach bug wp
- 1
updated Feb 22, 2021

Prev
1
2
3
4
5
6
7
8
9
…
17
Next