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}}
Updated date
Priority
Created date
Updated date
Milestone due date
Due date
Popularity
Label priority
Manual
Title
z3 ERROR: unknown parameter 'model_compress'
#55
· created
Oct 15, 2020
by
rwmjones
bug
wp
CLOSED
2
updated
Feb 22, 2021
error in generated proof obligation
#59
· created
Mar 10, 2020
by
Jens Gerlach
bug
wp
CLOSED
2
updated
Feb 22, 2021
Failure to detect qed libraries when running wp
#75
· created
Jul 17, 2018
by
mantis-gitlab-migration
critical
wp
CLOSED
18
updated
Feb 22, 2021
conditional input annotations result in why3 type errors
#76
· created
Aug 23, 2018
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Feb 22, 2021
suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
#77
· created
Mar 22, 2018
by
Jens Gerlach
enhancement
wp
CLOSED
3
updated
Feb 22, 2021
known, but inferrable, yet not inferred, property not given as precodition to provers
#80
· created
Oct 26, 2017
by
Jochen Burghardt
bug
wp
CLOSED
2
updated
Feb 22, 2021
WP warning not clear
#86
· created
Oct 22, 2019
by
Jens Gerlach
bug
wp
CLOSED
3
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
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 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
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
crash
#116
· created
Nov 13, 2018
by
mantis-gitlab-migration
critical
wp
CLOSED
6
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
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
number of generated files in Frama-C 18 vs 19. beta(2)
#151
· created
Jun 14, 2019
by
Jens Gerlach
bug
wp
CLOSED
7
updated
Feb 22, 2021
Ambiguous path error using why3
#159
· created
Jun 17, 2019
by
mantis-gitlab-migration
bug
wp
CLOSED
8
updated
Feb 22, 2021
Division by zero doesn't increase the number of VC in console output
#168
· created
Feb 17, 2019
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Feb 22, 2021
One \valid seems sufficient to write in a whole array.
#169
· created
Feb 12, 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
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
#224
· created
Jun 23, 2018
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Feb 22, 2021
Prev
1
2
3
4
5
…
13
Next