Issues · pub / frama-c · GitLab

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
-wp-out missing output for Why3 provers in Frama-C 20 beta

#101 · created Nov 08, 2019 by Jens Gerlach bug wp
- 0
updated Aug 05, 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
munmap() breaks WP analysis

#70 · created Feb 10, 2020 by mantis-gitlab-migration bug wp
- 0
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
Wp crashes on a recursive function

#58 · created Dec 28, 2018 by Frédéric Loulergue critical wp
- CLOSED
- 1
updated Feb 22, 2021
z3 ERROR: unknown parameter 'model_compress'

#55 · created Oct 15, 2020 by rwmjones bug wp
- CLOSED
- 2
updated Feb 22, 2021
An option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflows 3 of 3 tasks completed

#54 · created Jan 29, 2021 by varosi eva wp
- 3
updated Mar 29, 2021

Prev
1
…
9
10
11
12
13
14
Next