Issues · pub / frama-c · GitLab

expression "&this->val" in logic function body causes framaCIRGen abort

#899 · created Jan 22, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
postcondition of destructor unconsidered

#651 · created Apr 09, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
syntax error in contract causes rest to be tacitly ignored

#652 · created Jun 27, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 2
updated Feb 22, 2021
using "delete" causes warning for "free"

#653 · created Oct 30, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
destructor call ignored by WP

#854 · created Nov 10, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
side effect of constructor call from global variable initialization ignored

#869 · created Dec 01, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 0
updated Feb 22, 2021
insufficient preconditions given to Alt-Ergo to prove obligation originating from virtual methods

#870 · created Nov 17, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 2
updated Feb 22, 2021
protected variable not visible in contract in subclass

#879 · created Dec 15, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 3
updated Feb 22, 2021
struct type inside 'extern "C"' causes crash, except as lhs of typedef

#891 · created Nov 13, 2014 by Jochen Burghardt confirmed critical frama-clang
- CLOSED
- 2
updated Mar 29, 2021
throw/catch of struct causes crash

#886 · created Nov 10, 2014 by Jochen Burghardt confirmed critical frama-clang
- CLOSED
- 2
updated Mar 29, 2021
namespace prefix in annotation causes segmentation fault

#862 · created Nov 24, 2014 by Jochen Burghardt confirmed critical frama-clang
- CLOSED
- 1
updated Mar 29, 2021
parsing of hex int constant swallows following semicolon

#858 · created Nov 24, 2014 by Jochen Burghardt bug confirmed frama-clang
- CLOSED
- 1
updated Mar 29, 2021
function called in initialization of a static/global variable

#808 · created Apr 01, 2014 by Franck Vedrine bug confirmed frama-clang
- CLOSED
- 1
updated Mar 29, 2021
class expression causes abort in presence of user-defined destructor

#659 · created Dec 01, 2014 by Jochen Burghardt bug confirmed frama-clang
- CLOSED
- 1
updated Mar 29, 2021
different signatures for "linked" in definition and use in generated Alt-Ergo mlw file

#644 · created May 04, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Mar 29, 2021
declaration of static class-type variable in function body causes crash

#639 · created Apr 27, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Mar 29, 2021
float constant in contract causes crash

#636 · created Nov 24, 2014 by Jochen Burghardt confirmed critical frama-clang
- CLOSED
- 2
updated Mar 29, 2021
no diagnostics on wrong keyword

#282 · created Jan 31, 2018 by Jens Gerlach bug frama-clang
- CLOSED
- 2
updated Mar 30, 2021
kernel warns about invalid implicit conversion

#279 · created Jan 31, 2018 by Jens Gerlach bug frama-clang
- CLOSED
- 3
updated Mar 30, 2021
predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang

#278 · created Feb 08, 2018 by Jochen Burghardt enhancement frama-clang
- CLOSED
- 1
updated Mar 30, 2021

Prev
1
2
3
4
Next