Issues · pub / frama-c · GitLab

obligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo nevertheless

#948 · created Nov 27, 2014 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 29, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
*off == off_cpy cannot be proven just after the assignment *off = off_cpy

#628 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
One \valid seems sufficient to write in a whole array.

#169 · created Feb 12, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Option -wp-qed-checks generates invalid At-Ergo files

#932 · created Dec 15, 2014 by David Mentré bug wp
- CLOSED
- 1
updated Feb 22, 2021
performance problem about number of fields in structure for struct equality properties

#1895 · created Jan 13, 2013 by Stephane Duprat bug wp
- CLOSED
- 3
updated Feb 22, 2021
Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579

#582 · created Oct 27, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 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
Post-state of statement spec

#1912 · created Mar 25, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 6
updated Aug 05, 2021
Printing of function types causes a stack overflow

#1959 · created Oct 13, 2012 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 14, 2021
Problems when using ptests.

#2105 · created Oct 12, 2011 by Patrick Baudin bug wp
- CLOSED
- 2
updated Feb 22, 2021
Problem when arguments are not used in predicates

#791 · created Apr 30, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Problem with _Bool(when casting to int or with ?:)

#1000 · created Jul 21, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
proc name in assigns clause causes crash

#1889 · created Nov 01, 2012 by Jochen Burghardt critical wp
- CLOSED
- 1
updated Feb 22, 2021
Proof obligations of lemma properties

#1972 · created Jul 28, 2011 by Patrick Baudin bug wp
- CLOSED
- 1
updated Feb 22, 2021
Property does not work anymore when changed to predicate

#1849 · created May 29, 2013 by Allan Blanchard bug wp
- CLOSED
- 2
updated Feb 22, 2021
Property reported as inconditionnally valid when its dependency graph shows some orange box

#1205 · created Jun 11, 2013 by Virgile Prevosto bug wp
- CLOSED
- 4
updated Feb 22, 2021
Prove of \false

#126 · created Feb 16, 2019 by Jens Gerlach bug wp
- CLOSED
- 6
updated Apr 15, 2021
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
provide option "-wp-lemma"

#522 · created Jan 23, 2016 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021

Prev
1
…
3
4
5
6
7
8
9
10
11
…
13
Next