Issues · pub / frama-c · GitLab

Information on C type of array is not present (in Coq)

#107 · created Nov 22, 2017 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"

#108 · created Dec 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
\false provable from recursive logic definition

#82 · created Dec 18, 2017 by Jochen Burghardt bug wp
- CLOSED
- 10
updated Feb 22, 2021
Coq translation of predicate name changes when additional files are processed by Frama-C

#111 · created Jan 04, 2018 by Jochen Burghardt bug wp
- CLOSED
- 5
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
alt-ergo goals generated directly / via why3 differ in provability

#112 · created Feb 01, 2018 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Feb 22, 2021
suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory

#77 · created Mar 22, 2018 by Jens Gerlach enhancement wp
- CLOSED
- 3
updated Feb 22, 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
`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
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
Auto-generated assigns clause for a void* argument crashes wp

#113 · created Jul 05, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 1
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
Failure to detect qed libraries when running wp

#75 · created Jul 17, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 18
updated Feb 22, 2021
dubious discharge of postcondition

#115 · created Jul 24, 2018 by Jens Gerlach bug wp
- CLOSED
- 8
updated Feb 22, 2021
conditional input annotations result in why3 type errors

#76 · created Aug 23, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
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
Newer releases of FramaC produce apparent WP plug-in bug

#114 · created Oct 01, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
Shape of VC depends on selection of properties

#125 · created Oct 08, 2018 by Jens Gerlach bug wp
- CLOSED
- 4
updated Sep 21, 2021
contracts about memory mapped I/O through volatile memory locations

#117 · created Oct 31, 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

Prev
1
…
7
8
9
10
11
12
13
Next