Issues · pub / frama-c · GitLab

typo in wp output: "interruped"-->"interrupted"

#753 · created Jul 14, 2014 by Jochen Burghardt wp
- CLOSED
- 2
updated Feb 22, 2021
unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?

#1987 · created Nov 28, 2011 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
Unable to prove things that are provable, gets confused

#584 · created Oct 18, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
unable to use lemma separated_region

#620 · created Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
undefined (or built-in?) predicate "global" in proof obligation

#1880 · created Dec 01, 2011 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Feb 22, 2021
Under windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishing

#492 · created Jun 11, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 0
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
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))

#499 · created Jan 22, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated May 18, 2021
Unexpected error (Stack overflow) during WP

#2205 · created Jan 10, 2011 by Benjamin Monate critical wp
- CLOSED
- 4
updated Feb 22, 2021
Unexpected label Old in pre : ignored annotation

#1350 · created Oct 05, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 12
updated Feb 22, 2021
"Unknown Error" with Alt-Ergo 3 of 3 tasks completed

#2547 · created Mar 26, 2021 by Qix wp
- CLOSED
- 11
updated Jun 01, 2021
Unprovable inequality involving (unsigned) -1

#570 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
unprovable PO in function manipulating structs - issue with Qed's simplifications

#1818 · created Nov 08, 2013 by Virgile Prevosto bug wp
- CLOSED
- 5
updated Apr 14, 2021
unprovable po with -split

#2203 · created Dec 17, 2010 by Stephane Duprat bug wp
- CLOSED
- 2
updated Feb 22, 2021
unproven property used in a behavior in Typed model

#1888 · created Nov 06, 2012 by Stephane Duprat bug wp
- CLOSED
- 1
updated Feb 22, 2021
Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas

#946 · created Dec 02, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Upgrading WP causes crash in Jessie

#2018 · created Jul 02, 2012 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
Use of very large real constants cause failures in proof generation in WP

#507 · created Jun 14, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
use of void* leads to type error in the PO generation

#554 · created Feb 16, 2015 by Virgile Prevosto bug wp
- CLOSED
- 2
updated Feb 22, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021

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