Issues · pub / frama-c · GitLab

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
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
lemma tacitly omitted from prover assumptions

#367 · created Feb 27, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Aug 05, 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
Provide an option to run Coq from Frama-C

#359 · created Mar 12, 2014 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021
Axiomatic is recompiled when using severalprocesses

#356 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 1
updated Feb 22, 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
type of float parameter changed unexpectedly to double

#347 · created Feb 24, 2017 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
suggest to check (loop) assigns clauses by data flow analysis

#337 · created Jun 01, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Aug 05, 2021
naming the default behavior influences proven obligations

#336 · created Jun 01, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
poor errors message texts for Hoare memory model checks

#334 · created Jun 15, 2017 by Jochen Burghardt wp
- CLOSED
- 1
updated Sep 21, 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
Strange difference in generated Coq code between Chlorine and Sulfur

#262 · created May 09, 2018 by Jens Gerlach critical wp
- CLOSED
- 9
updated Feb 22, 2021
WP: internal error: only the kernel should set the status of property assumes

#261 · created Jul 04, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Invalid sizeof(struct) calculation in Sulfur

#259 · created Jan 19, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021

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