Issues · pub / frama-c · GitLab

explain wp's syntactic restrictions on "inductive" definitions

#123 · created Dec 14, 2017 by Jochen Burghardt documentation
- CLOSED
- 1
updated Feb 22, 2021
malloc breaks reasoning about assigns

#122 · created Jun 17, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
floating-point support is somwhat incomplete

#121 · created Jul 02, 2019 by mantis-gitlab-migration critical wp
- CLOSED
- 4
updated Feb 22, 2021
Mk_addr not defined in Memory.v (coqwp via why3ide)

#118 · created Dec 07, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 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
crash

#116 · created Nov 13, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
dubious discharge of postcondition

#115 · created Jul 24, 2018 by Jens Gerlach bug wp
- CLOSED
- 8
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
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
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
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
Crash on loop with global assigns and per-behavior assigns

#109 · created Oct 19, 2015 by Boris Yakobowski critical wp
- CLOSED
- 2
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
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 unique term normalization for lemmas and goals

#106 · created Oct 09, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
suggest boolean expressions for "-wp-prop" arguments

#105 · created Feb 27, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 3
updated Feb 22, 2021
readability of coq(?) names

#104 · created Mar 31, 2015 by Jens Gerlach bug wp
- CLOSED
- 6
updated Feb 22, 2021
Eprover in Frama-C 20 beta

#103 · created Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
alt-ergo support in Frama-C 20 beta

#102 · created Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 0
updated Apr 14, 2021
quantifiers over logic types do not restrict to valid instances

#91 · created Jan 30, 2020 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Apr 15, 2021

Prev
1
…
57
58
59
60
61
62
63
64
Next