Issues · pub / frama-c · GitLab

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
frama-c/wp generates invalid why3

#87 · created Aug 13, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
WP warning not clear

#86 · created Oct 22, 2019 by Jens Gerlach bug wp
- CLOSED
- 3
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
Error in coq code generated by wp

#81 · created Jun 12, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
known, but inferrable, yet not inferred, property not given as precodition to provers

#80 · created Oct 26, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Feb 22, 2021
ill-typed alt-ergo proof obligation

#78 · created Sep 25, 2013 by Virgile Prevosto 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
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
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
error in generated proof obligation

#59 · created Mar 10, 2020 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021

Prev
1
…
8
9
10
11
12
13
Next