Issues · pub / frama-c · GitLab

WP - unsoundness with union

#2609 · created Apr 22, 2022 by Geoff Hulette confirmed enhancement wp
- 5
updated May 02, 2022
[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
- 2
updated Mar 16, 2022
[WP] Out of memory crash

#2597 · created Mar 15, 2022 by Lélio Brun bug confirmed wp
- 2
updated Apr 20, 2022
[WP] Type mismatch with Real model

#2596 · created Mar 15, 2022 by Lélio Brun bug confirmed wp
- 1
updated Mar 15, 2022
Build failure if only the eva plugin is selected: -rectypes is required

#2593 · created Jan 13, 2022 by fx-carton compilation confirmed
- 3
updated Jan 14, 2022
Non ghost lvalue when assigning array (frama-c 22)

#2580 · created Oct 20, 2021 by Raul Monti bug confirmed kernel
- 3
updated Oct 21, 2021
Parse error when using a wide string literal to initialize uint16 array

#2347 · created Sep 30, 2010 by mantis-gitlab-migration bug confirmed kernel
- 4
updated Feb 22, 2021
journalization of -print option

#1832 · created Jul 04, 2013 by Patrick Baudin bug confirmed kernel
- 1
updated Feb 22, 2021
exception identifier from catch() statement unknown in contracts, but not in code

#906 · created Feb 02, 2015 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
can't compare pointer and reference for equality in contract

#903 · created Jan 22, 2015 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
type def'd as template typename causes SEGV when used in logic functions

#900 · created Jan 22, 2015 by Jochen Burghardt confirmed critical frama-clang
- 1
updated Feb 22, 2021
catching a superclass causes crash

#898 · created Jan 15, 2015 by Jochen Burghardt confirmed critical frama-clang
- 0
updated Feb 22, 2021
recursive logic integer function definition causes error

#897 · created Jan 15, 2015 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
ACSL comment rejected in function template

#896 · created Jan 12, 2015 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
unprovable obligation generated for "ensures" in presence of exceptions

#895 · created Jan 08, 2015 by Jochen Burghardt bug confirmed frama-clang
- 1
updated Feb 22, 2021
throw without argument causes crash

#894 · created Jan 08, 2015 by Jochen Burghardt bug confirmed frama-clang
- 1
updated Feb 22, 2021
use of template class in default template argument in namespace causes crash

#889 · created Nov 17, 2014 by Jochen Burghardt confirmed critical frama-clang
- 3
updated Feb 22, 2021
use of initialized array causes crash

#887 · created Nov 24, 2014 by Jochen Burghardt confirmed critical frama-clang
- 2
updated Feb 22, 2021
constructor overloading resolution with templates causes dubious "contract merge" warning

#885 · created Jan 05, 2015 by Jochen Burghardt bug confirmed frama-clang
- 1
updated Feb 22, 2021
"ensures" clause of function template not supplied to Alt-Ergo

#883 · created Dec 15, 2014 by Jochen Burghardt bug confirmed frama-clang
- 3
updated Feb 22, 2021

Prev
1
2
3
4
Next