Issues · pub / frama-c · GitLab

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
WP is not able to validate a statically declared structure followed by a memset

#246 · created Jul 11, 2018 by Patricia Mouy bug wp
- CLOSED
- 3
updated Feb 22, 2021
Newer releases of FramaC produce apparent WP plug-in bug

#241 · created Oct 01, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Some issues related to Frama-C 18.0 (beta) "Argon"

#225 · created Nov 03, 2018 by Jens Gerlach bug wp
- CLOSED
- 1
updated Feb 22, 2021
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.

#224 · created Jun 23, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021

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