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
209
Closed
1,269
All
1,478
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}}
Milestone due date
Priority
Created date
Updated date
Milestone due date
Due date
Popularity
Label priority
Manual
Title
explain wp's syntactic restrictions on "inductive" definitions
#123
· created
Dec 14, 2017
by
Jochen Burghardt
documentation
CLOSED
1
updated
Feb 22, 2021
malloc breaks reasoning about assigns
#122
· created
Jun 17, 2019
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
floating-point support is somwhat incomplete
#121
· created
Jul 02, 2019
by
mantis-gitlab-migration
critical
wp
CLOSED
4
updated
Feb 22, 2021
Mk_addr not defined in Memory.v (coqwp via why3ide)
#118
· created
Dec 07, 2018
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Feb 22, 2021
contracts about memory mapped I/O through volatile memory locations
#117
· created
Oct 31, 2018
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
crash
#116
· created
Nov 13, 2018
by
mantis-gitlab-migration
critical
wp
CLOSED
6
updated
Feb 22, 2021
dubious discharge of postcondition
#115
· created
Jul 24, 2018
by
Jens Gerlach
bug
wp
CLOSED
8
updated
Feb 22, 2021
Newer releases of FramaC produce apparent WP plug-in bug
#114
· created
Oct 01, 2018
by
mantis-gitlab-migration
bug
wp
CLOSED
4
updated
Feb 22, 2021
Auto-generated assigns clause for a void* argument crashes wp
#113
· created
Jul 05, 2018
by
mantis-gitlab-migration
critical
wp
CLOSED
1
updated
Feb 22, 2021
alt-ergo goals generated directly / via why3 differ in provability
#112
· created
Feb 01, 2018
by
Jochen Burghardt
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
Crash on loop with global assigns and per-behavior assigns
#109
· created
Oct 19, 2015
by
Boris Yakobowski
critical
wp
CLOSED
2
updated
Feb 22, 2021
suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
#108
· created
Dec 08, 2017
by
Jochen Burghardt
enhancement
wp
CLOSED
2
updated
Feb 22, 2021
Information on C type of array is not present (in Coq)
#107
· created
Nov 22, 2017
by
Jens Gerlach
bug
wp
CLOSED
3
updated
Feb 22, 2021
suggest unique term normalization for lemmas and goals
#106
· created
Oct 09, 2017
by
Jochen Burghardt
enhancement
wp
CLOSED
2
updated
Feb 22, 2021
suggest boolean expressions for "-wp-prop" arguments
#105
· created
Feb 27, 2017
by
Jochen Burghardt
enhancement
wp
CLOSED
3
updated
Feb 22, 2021
readability of coq(?) names
#104
· created
Mar 31, 2015
by
Jens Gerlach
bug
wp
CLOSED
6
updated
Feb 22, 2021
Eprover in Frama-C 20 beta
#103
· created
Nov 08, 2019
by
Jens Gerlach
bug
wp
CLOSED
1
updated
Apr 15, 2021
alt-ergo support in Frama-C 20 beta
#102
· created
Nov 08, 2019
by
Jens Gerlach
bug
wp
CLOSED
0
updated
Apr 14, 2021
quantifiers over logic types do not restrict to valid instances
#91
· created
Jan 30, 2020
by
mantis-gitlab-migration
bug
wp
CLOSED
3
updated
Apr 15, 2021
Prev
1
…
57
58
59
60
61
62
63
64
Next