Issues · pub / frama-c · GitLab

Known WP limitations on statement contract

#2569 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Aug 06, 2021
Known WP limitations on the reads clause 0 of 2 tasks completed

#2568 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Aug 05, 2021
Known WP limitations on `assigns` handling 0 of 2 tasks completed

#2567 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Nov 23, 2021
ghost integer ?

#2428 · created Feb 01, 2010 by Sylvie Boldo ACSL enhancement kernel
- 0
updated Feb 22, 2021
Better support of //@ style

#2427 · created May 11, 2009 by mantis-gitlab-migration ACSL enhancement kernel
- 2
updated Feb 22, 2021
no multiple assert-clauses accepted in /*@...*/-style comment

#2323 · created Oct 12, 2010 by Jochen Burghardt ACSL enhancement kernel
- 0
updated Feb 22, 2021
Any number of ";" should be allowed in specifications

#2240 · created Feb 10, 2011 by mantis-gitlab-migration ACSL enhancement kernel
- 0
updated Feb 22, 2021
Command.command_generic may raise Sys_error

#2237 · created Feb 21, 2011 by Julien Signoles enhancement kernel
- 0
updated Feb 22, 2021
Functional expression in assigns properties

#2171 · created Oct 06, 2011 by mantis-gitlab-migration ACSL enhancement kernel
- 0
updated Feb 22, 2021
suggest to provide FILE,LINE references for proof obligations in WP cmd-line output

#2098 · created Nov 04, 2011 by Jochen Burghardt enhancement wp
- 1
- 0
updated Aug 05, 2021
declaration of variable of type void accepted

#1829 · created Nov 28, 2013 by Jochen Burghardt enhancement kernel
- 0
updated Feb 22, 2021
r24600: confusing error message when t[] is used where t* is expected

#1828 · created Dec 03, 2013 by Pascal Cuoq ACSL enhancement kernel
- 0
updated Feb 22, 2021
suggest to insert implicit cast of logic function's expression to return type

#1827 · created Nov 28, 2013 by Jochen Burghardt enhancement kernel
- 0
updated Feb 22, 2021
Several [invariant] at a program point

#1753 · created Mar 08, 2011 by mantis-gitlab-migration ACSL enhancement kernel
- 4
updated Feb 22, 2021
Generate proof obligation for drivers when driver instantiate a logic acsl declaration

#1147 · created Mar 13, 2014 by Jens Gerlach enhancement wp
- 0
updated Feb 22, 2021
Extend smoke tests to incoherent specification of declared functions

#1028 · created Oct 28, 2013 by Dillon Pariente enhancement wp
- 7
updated Aug 05, 2021
Default @requires property for the [main] function

#1006 · created Feb 22, 2012 by mantis-gitlab-migration enhancement kernel
- 2
updated Feb 22, 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
- 1
updated Aug 05, 2021
different error messages for "0<x" and "0<x<9" when x is of class type

#872 · created Dec 01, 2014 by Jochen Burghardt confirmed enhancement frama-clang
- 1
updated Feb 22, 2021
suggest to suppress warning about passing void value via return statement

#868 · created Nov 27, 2014 by Jochen Burghardt confirmed enhancement frama-clang
- 1
updated Feb 22, 2021

Prev
1
2
3
Next