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}}
Title
Priority
Created date
Updated date
Milestone due date
Due date
Popularity
Label priority
Manual
Title
`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
suggest boolean expressions for "-wp-prop" arguments
#105
· created
Feb 27, 2017
by
Jochen Burghardt
enhancement
wp
CLOSED
3
updated
Feb 22, 2021
suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations
#593
· created
Sep 21, 2015
by
Jochen Burghardt
enhancement
wp
CLOSED
1
updated
Apr 15, 2021
suggestion: translate axioms and implication premises in forward order to coq
#360
· created
Mar 13, 2017
by
Jochen Burghardt
bug
wp
CLOSED
2
updated
Apr 15, 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
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
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
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
Suggest to supply values of global consts to provers
#498
· created
May 10, 2012
by
Jochen Burghardt
enhancement
wp
CLOSED
13
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
Support of \block_length
#1928
· created
Jul 29, 2011
by
Patrick Baudin
bug
wp
CLOSED
1
updated
Feb 22, 2021
Surprising goal generated with unsigned long long int
#2247
· created
Jan 04, 2011
by
Benjamin Monate
bug
wp
CLOSED
1
updated
Feb 22, 2021
suspicious axiomatization of included,zrange,zunion in .sx file
#2087
· created
Dec 15, 2011
by
Jochen Burghardt
wp
CLOSED
2
updated
Apr 15, 2021
Switch statements seem to be unsound
#397
· created
Aug 19, 2016
by
mantis-gitlab-migration
bug
wp
CLOSED
3
updated
Feb 22, 2021
syntax error for alt-ergo with memset spec
#1020
· created
Dec 16, 2013
by
mantis-gitlab-migration
bug
wp
CLOSED
4
updated
Feb 22, 2021
Testing example which is OK for Jessie-plugin fails with wp-plugin.
#2081
· created
Dec 16, 2011
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
time too long even with -wp-timeout 1
#1875
· created
Apr 13, 2011
by
Patrick Baudin
bug
wp
CLOSED
4
updated
Feb 22, 2021
Translation of tsets
#1900
· created
Apr 15, 2013
by
Julien Signoles
enhancement
wp
CLOSED
6
updated
Apr 15, 2021
translation to why3 of int* argument to logic function
#371
· created
Feb 02, 2017
by
Jochen Burghardt
bug
confirmed
wp
CLOSED
6
updated
Apr 15, 2021
type of float parameter changed unexpectedly to double
#347
· created
Feb 24, 2017
by
mantis-gitlab-migration
bug
wp
CLOSED
2
updated
Feb 22, 2021
Prev
1
…
5
6
7
8
9
10
11
12
13
Next