Issues · pub / frama-c · GitLab

ACSL comment rejected in function template

#896 · created Jan 12, 2015 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
bitwise negation of uint introduces "-1" in Alt-Ergo obligation

#865 · created Dec 08, 2014 by Jochen Burghardt ACSL confirmed
- 3
updated Feb 22, 2021
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
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
Can't use e-acsl on a dynamic library containing all the instrumentations

#179 · created Jan 22, 2019 by mantis-gitlab-migration confirmed critical e-acsl
- 2
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
CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)

#660 · created Oct 30, 2014 by Jochen Burghardt confirmed enhancement frama-clang
- 3
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
Declaration order of static class member

#851 · created Nov 02, 2014 by Jens Gerlach bug confirmed frama-clang
- 0
updated Feb 22, 2021
declarations of static variable of class type in function body causes crash

#640 · created Nov 27, 2014 by Jochen Burghardt confirmed critical frama-clang
- 1
updated Mar 29, 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
"do"-loop with body interspersed with "case" labels of surrounding "switch" not parsed

#866 · created Nov 27, 2014 by Jochen Burghardt confirmed enhancement frama-clang
- 0
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
enum types in contract cause syntax error

#859 · created Nov 24, 2014 by Jochen Burghardt bug confirmed frama-clang
- 0
updated Feb 22, 2021
error message "unknown identifier 'xxx'" causes Frama-C to forget previous more severe errors

#833 · created Dec 15, 2014 by Jochen Burghardt bug confirmed frama-clang
- 2
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
Frama-C-clang does not unfold typedef

#845 · created Jun 12, 2014 by Jens Gerlach bug confirmed kernel
- 2
updated Feb 22, 2021
Frama-Clang does allow access to private fields within annotations

#850 · created May 30, 2014 by Jens Gerlach confirmed enhancement kernel
- 2
updated Feb 22, 2021
how to specify equality of references, rather than of values, in contract?

#863 · created Nov 24, 2014 by Jochen Burghardt confirmed enhancement frama-clang
- 0
updated Feb 22, 2021
How to use the "Callers ..." context menu item

#290 · created May 27, 2013 by mantis-gitlab-migration confirmed enhancement gui
- 2
updated Feb 22, 2021

Prev
1
2
3
4
Next