Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Issues
Open
21
Closed
247
All
268
New issue
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
Created date
Priority
Created date
Updated date
Milestone due date
Due date
Popularity
Label priority
Manual
Title
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
normalization of "assigns" in statement contract doens't cope with introduced auxiliary variables
#622
· created
Apr 09, 2015
by
Jochen Burghardt
bug
wp
CLOSED
4
updated
Mar 30, 2021
readability of coq(?) names
#104
· created
Mar 31, 2015
by
Jens Gerlach
bug
wp
CLOSED
6
updated
Feb 22, 2021
False valid with LONG_MIN
#802
· created
Mar 06, 2015
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
Able to assert a false statement
#803
· created
Mar 03, 2015
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Apr 15, 2021
Crash with \is_infinite
#550
· created
Feb 24, 2015
by
mantis-gitlab-migration
critical
wp
CLOSED
3
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
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
Frama-C does not work with versions of Why3 newer than 0.83
#711
· created
Jan 27, 2015
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Feb 22, 2021
Sessions and WP do not interact properly
#618
· created
Jan 06, 2015
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
unable to use lemma separated_region
#620
· created
Dec 28, 2014
by
Jens Gerlach
bug
wp
CLOSED
2
updated
Apr 15, 2021
assumes clause and labels
#544
· created
Dec 27, 2014
by
Jens Gerlach
bug
wp
CLOSED
2
updated
Feb 22, 2021
WP-Plugin crashes due to an internal error when terms of sets during union have different types
#919
· created
Dec 22, 2014
by
mantis-gitlab-migration
critical
wp
CLOSED
1
updated
Apr 15, 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
insufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operator
#878
· created
Dec 11, 2014
by
Jochen Burghardt
bug
confirmed
wp
CLOSED
3
updated
Apr 15, 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
suggest to provide a command-line option for checking if every loop or recursion has a termination measuring function attached
#951
· created
Nov 27, 2014
by
Jochen Burghardt
enhancement
kernel
wp
CLOSED
2
updated
Jan 10, 2022
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
assertion not proved anymore by WP
#931
· created
Oct 23, 2014
by
mantis-gitlab-migration
bug
wp
CLOSED
4
updated
Feb 22, 2021
WP crashes on \floor builtin
#959
· created
Oct 12, 2014
by
mantis-gitlab-migration
critical
wp
CLOSED
1
updated
Apr 15, 2021
Prev
1
…
3
4
5
6
7
8
9
10
11
…
13
Next