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,261
All
1,470
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
suggest to report column number for warnings
#363
· created
Jan 09, 2017
by
Jochen Burghardt
enhancement
eva
CLOSED
1
updated
Feb 22, 2021
WP inserts unwanted new lines into Coq proofs
#385
· created
Jan 02, 2017
by
Jens Gerlach
bug
wp
CLOSED
1
updated
Apr 15, 2021
Why3 warning
#387
· created
Dec 16, 2016
by
Jens Gerlach
bug
wp
CLOSED
2
updated
Apr 15, 2021
more prover processes run than expected
#388
· created
Dec 15, 2016
by
Jens Gerlach
bug
wp
CLOSED
4
updated
Apr 15, 2021
error in Coq file generation
#405
· created
Dec 03, 2016
by
Alain Giorgetti
bug
wp
CLOSED
1
updated
Apr 15, 2021
suggest to provide and document a unique warning string to grep for in value-analysis output files
#297
· created
Nov 28, 2016
by
Jochen Burghardt
eva
CLOSED
4
updated
Feb 22, 2021
Annotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.
#401
· created
Nov 24, 2016
by
mantis-gitlab-migration
bug
rte
CLOSED
3
updated
Feb 22, 2021
wrong example code in value analysis manual, p.35, for message " invalid LHS operand for left shift"
#391
· created
Nov 21, 2016
by
Jochen Burghardt
documentation
CLOSED
2
updated
Feb 22, 2021
Ocaml 4.04.0 build error
#393
· created
Nov 09, 2016
by
mantis-gitlab-migration
bug
kernel
CLOSED
2
updated
Feb 22, 2021
File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
#314
· created
Oct 17, 2016
by
Jochen Burghardt
bug
libc
CLOSED
4
updated
Apr 01, 2021
Failure to compile on windows using cygwin
#390
· created
Oct 14, 2016
by
mantis-gitlab-migration
bug
documentation
CLOSED
3
updated
Feb 22, 2021
GMP typing issue
#343
· created
Oct 14, 2016
by
Kostyantyn Vorobyov
bug
e-acsl
CLOSED
0
updated
Feb 22, 2021
Unterminated comment while generating division-by-zero assertion
#404
· created
Oct 13, 2016
by
Kostyantyn Vorobyov
bug
kernel
CLOSED
5
updated
Feb 22, 2021
__attribute__((aligned(0))) tacitly causes sizeof computation to fail
#402
· created
Oct 13, 2016
by
Jochen Burghardt
kernel
CLOSED
6
updated
Feb 22, 2021
option "-print" prints array upper bound in type before parameter name, rather than after it
#392
· created
Oct 06, 2016
by
Jochen Burghardt
kernel
CLOSED
1
2
updated
Apr 16, 2021
Compiling on Windows (cygwin) fails
#396
· created
Oct 01, 2016
by
mantis-gitlab-migration
bug
documentation
CLOSED
7
updated
Feb 22, 2021
Switch statements seem to be unsound
#397
· created
Aug 19, 2016
by
mantis-gitlab-migration
bug
wp
CLOSED
3
updated
Feb 22, 2021
Nested scopes may cause issues with the validity of created pointers
#409
· created
Aug 17, 2016
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Apr 15, 2021
Logic with read clauses can have their values invalidated by writes to separated memory locations
#410
· created
Aug 08, 2016
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Aug 05, 2021
"Builtin already registered" after Reparse
#398
· created
Jul 30, 2016
by
mantis-gitlab-migration
critical
wp
CLOSED
2
updated
Feb 22, 2021
Prev
1
…
7
8
9
10
11
12
13
14
15
…
64
Next