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
248
All
269
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
[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter
#2601
· created
Mar 15, 2022
by
Costava
confirmed
enhancement
wp
CLOSED
3
updated
May 30, 2022
[WP] Failure to verify range information after bitwise and on signed integers
#2589
· created
Jan 03, 2022
by
GuerricChupin
wp
CLOSED
4
updated
Jan 11, 2022
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
loop invariant as hypothesis
#1821
· created
Jan 20, 2014
by
mantis-gitlab-migration
bug
wp
CLOSED
1
3
updated
Jan 05, 2022
[WP] Soundness issue when handling a pointer on a structure containing an array.
#2575
· created
Sep 20, 2021
by
AlexCid
feedback-needed
wp
CLOSED
1
6
updated
Oct 06, 2021
Shape of VC depends on selection of properties
#125
· created
Oct 08, 2018
by
Jens Gerlach
bug
wp
CLOSED
4
updated
Sep 21, 2021
Develop strategies to efficiently run WP with different ATP and Coq
#1145
· created
Mar 14, 2014
by
Jens Gerlach
enhancement
wp
CLOSED
0
updated
Sep 21, 2021
poor errors message texts for Hoare memory model checks
#334
· created
Jun 15, 2017
by
Jochen Burghardt
wp
CLOSED
1
updated
Sep 21, 2021
Make find(1) command POSIX-compliant
#513
· created
Apr 09, 2016
by
mantis-gitlab-migration
bug
wp
CLOSED
1
updated
Aug 05, 2021
Question: Dump why3 file generated by frama-c
#46
· created
Dec 06, 2020
by
Leo Viezens
wp
CLOSED
3
updated
Aug 05, 2021
Post-state of statement spec
#1912
· created
Mar 25, 2011
by
mantis-gitlab-migration
bug
wp
CLOSED
6
updated
Aug 05, 2021
validity of obligation from statement contract depends on whether the statement is enclosed in block {}
#625
· created
Jun 01, 2015
by
Jochen Burghardt
bug
wp
CLOSED
3
updated
Aug 05, 2021
suggest to check (loop) assigns clauses by data flow analysis
#337
· created
Jun 01, 2017
by
Jochen Burghardt
enhancement
wp
CLOSED
1
updated
Aug 05, 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
Generate footprint from reads clauses of logic declarations
#1146
· created
Mar 13, 2014
by
Jens Gerlach
enhancement
wp
CLOSED
1
updated
Aug 05, 2021
lemma tacitly omitted from prover assumptions
#367
· created
Feb 27, 2017
by
Jochen Burghardt
bug
wp
CLOSED
2
updated
Aug 05, 2021
Assigns not respected in behaviors when using pointers to pointers
#1019
· created
Jun 16, 2014
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Aug 05, 2021
[wp] shall use per-behaviour assigns at call sites
#3
· created
May 07, 2020
by
Nikolai Kosmatov
enhancement
wp
CLOSED
6
updated
Aug 05, 2021
assigns clause appears unprovable
#1002
· created
Feb 01, 2014
by
Jens Gerlach
bug
wp
CLOSED
5
updated
Aug 05, 2021
assigns, loop assigns and loop invariant
#1018
· created
Jul 24, 2013
by
Virgile Prevosto
bug
wp
CLOSED
4
updated
Aug 05, 2021
Prev
1
2
3
4
5
…
13
Next