Issues · pub / frama-c

New issue

unprovable po with -split

#2203 · created Dec 17, 2010 by Stephane Duprat bug wp
- CLOSED
- 2
updated Feb 22, 2021
Unexpected error (Stack overflow) during WP

#2205 · created Jan 10, 2011 by Benjamin Monate critical wp
- CLOSED
- 4
updated Feb 22, 2021
warning: Degenerated goal

#2206 · created Jan 07, 2011 by Stephane Duprat bug wp
- CLOSED
- 8
updated Feb 22, 2021
[wp] warning: Stronger goal store_AppelerVerifier_post_6 (1 warning)

#2209 · created Dec 21, 2010 by Stephane Duprat bug wp
- CLOSED
- 2
updated Feb 22, 2021
Unexpected error (Failure("int_of_string")).

#2210 · created Feb 02, 2011 by John Regher critical wp
- CLOSED
- 2
updated Feb 22, 2021
requires in beahviors do not behave as expected

#626 · created Jun 12, 2015 by David Cok bug wp
- CLOSED
- 2
updated Feb 22, 2021
Carbon beta coqide: need write rights to /usr/local/share/frama-c

#2227 · created Dec 15, 2010 by Holger Blasum bug wp
- CLOSED
- 2
updated Feb 22, 2021
for a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather than to 1 (as in C)

#677 · created Feb 19, 2015 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
cannot proof the rte assertion in the loop for

#2246 · created Feb 01, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Surprising goal generated with unsigned long long int

#2247 · created Jan 04, 2011 by Benjamin Monate bug wp
- CLOSED
- 1
updated Feb 22, 2021
Number of discharged Qed goals counted multiple times

#552 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
WP: Incorrect assigns global/static handling

#18 · created Jun 15, 2020 by Alex Coffin wp
- CLOSED
- 1
- 1
updated Feb 22, 2021
incomplete loading of saved state when using WP?

#124 · created Mar 09, 2017 by Jens Gerlach 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
[wp] unsoundness for base-offset

#16 · created Jun 12, 2020 by Loïc Correnson wp
- CLOSED (MOVED)
- 0
updated Feb 22, 2021
dubious discharge of postcondition

#115 · created Jul 24, 2018 by Jens Gerlach bug wp
- CLOSED
- 8
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
\false provable from recursive logic definition

#82 · created Dec 18, 2017 by Jochen Burghardt bug wp
- CLOSED
- 10
updated Feb 22, 2021
readability of coq(?) names

#104 · created Mar 31, 2015 by Jens Gerlach bug wp
- CLOSED
- 6
updated Feb 22, 2021
Newer releases of FramaC produce apparent WP plug-in bug

#241 · created Oct 01, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021