Issues · pub / frama-c · GitLab

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
Error message when a solver is not installed

#1217 · created Nov 07, 2013 by Loïc Correnson enhancement wp
- CLOSED
- 3
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
Confusing bullets for unproven obligations under OSX

#1199 · created Jan 24, 2014 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
Qedlib.v definition of tactic "replace by" clashes with standard tactic "replace with"

#1195 · created Jan 22, 2014 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
Allow starting coq from Frama-C GUI also for proven obligations

#1197 · created Jan 21, 2014 by Jens Gerlach enhancement wp
- CLOSED
- 5
updated Feb 22, 2021
invalid loop invariant marked as valid (without pending hypothesis)

#1181 · created Jul 29, 2013 by Virgile Prevosto bug wp
- CLOSED
- 3
updated Feb 22, 2021
invalid statement contract ("assigns") verified with CVC4 under strange circumstances

#599 · created Apr 30, 2015 by Jochen Burghardt bug wp
- CLOSED
- 14
updated Feb 22, 2021
assertion not proved anymore by WP

#931 · created Oct 23, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
Warning for Axiom: From wp: Overloaded operator User defined axiom

#1319 · created Jul 28, 2011 by Patrick Baudin bug wp
- CLOSED
- 2
updated Feb 22, 2021
Errors in coq files generated by WP

#1231 · created Jan 16, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
WP: This term has type real but is expected to have type int

#1230 · created Jan 20, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
do ... while{ } loop and -wp-invariants option

#624 · created May 19, 2015 by Lionel Blatter bug wp
- CLOSED
- 1
updated Feb 22, 2021
Bug in let-elimination (due to <==> and assert false).

#1192 · created Dec 16, 2013 by Loïc Correnson bug wp
- CLOSED
- 3
updated Feb 22, 2021
WP - strcpy not proved

#1032 · created Feb 24, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
syntax error for alt-ergo with memset spec

#1020 · created Dec 16, 2013 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
frama-clang and WP: unverified precondition of member function

#826 · created May 25, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021
Crash when using wpo api get_result

#792 · created May 19, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
Make identifiers in Coq proofs more similar to those from C code

#779 · created Jan 23, 2014 by Jens Gerlach bug wp
- CLOSED
- 4
updated Feb 22, 2021
compatibility between \null in ACSL and NULL in C in wp

#777 · created Feb 17, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021

Prev
1
…
6
7
8
9
10
11
12
13
Next