Issues · pub / frama-c · GitLab

access to static struct fields unsupported in annotation

#638 · created May 07, 2015 by Jochen Burghardt bug 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
ACSL typing fails when performing unification of type variables

#590 · created Sep 24, 2015 by Patrick Baudin ACSL bug kernel
- 0
updated Mar 29, 2021
Alt-Ergo reports about " bool and int cannot be unified"

#280 · created Feb 05, 2018 by Jens Gerlach bug frama-clang
- 1
updated Feb 22, 2021
ambiguity with consecutive comparison and ternary expressions

#575 · created Dec 05, 2015 by David Cok ACSL bug kernel
- 1
updated Feb 22, 2021
An option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflows 3 of 3 tasks completed

#54 · created Jan 29, 2021 by varosi eva wp
- 3
updated Mar 29, 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
"assigns" in statement contract causes abort or crash

#273 · created Feb 12, 2018 by Jochen Burghardt critical frama-clang
- 0
updated Feb 22, 2021
axiom "addr_le_def" given to Alt-Ergo considered too weak

#907 · created Jan 12, 2015 by Jochen Burghardt bug wp
- 7
updated Aug 05, 2021
Better support of //@ style

#2427 · created May 11, 2009 by mantis-gitlab-migration ACSL enhancement kernel
- 2
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 due to mangled variable assignment in Makefile

#158 · created Jun 20, 2019 by mantis-gitlab-migration bug compilation
- 1
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
__builtin_alloca

#2045 · created Jun 08, 2012 by mantis-gitlab-migration bug kernel
- 1
updated Feb 22, 2021
C++11 delegating constructor not supported

#287 · created Jan 19, 2018 by Jens Gerlach bug frama-clang
- 0
updated Feb 22, 2021
cabs2cil fails with statements in expression in a question

#57 · created Jun 10, 2020 by mantis-gitlab-migration bug kernel
- 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
can't handle lemma with 3 labels

#277 · created Feb 08, 2018 by Jochen Burghardt bug frama-clang
- 2
updated Feb 22, 2021
can't prove (trivial) validity of memory access of "p->a"

#642 · created May 04, 2015 by Jochen Burghardt bug 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

Prev
1
2
3
4
5
…
11
Next