Issues · pub / frama-c · GitLab

A pointer can be reported as belonging to an adjacent memory blocks in the bittree memory model

#980 · created Jul 16, 2014 by Arvid Jakobsson bug e-acsl
- CLOSED
- 1
updated Feb 22, 2021
"[...]/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed." using full memory model, asserting validty of local var

#978 · created Mar 25, 2014 by Arvid Jakobsson bug e-acsl
- CLOSED
- 1
updated Feb 22, 2021
Global variables are not marked as initialized

#975 · created Jun 25, 2014 by Arvid Jakobsson bug e-acsl
- CLOSED
- 1
updated Feb 22, 2021
A valid pointer to an empty struct generate a failure

#972 · created Mar 14, 2014 by mantis-gitlab-migration bug e-acsl
- CLOSED
- 2
updated Feb 22, 2021
label argument of \at unrecognized

#964 · created Jun 16, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 2
updated Feb 22, 2021
Frama-clang has problems with "decreases" clauses

#962 · created Jun 20, 2014 by Jens Gerlach bug frama-clang
- CLOSED
- 2
updated Feb 22, 2021
Kernel error with _Static_assert in a struct

#949 · created Nov 20, 2014 by mantis-gitlab-migration bug kernel
- CLOSED
- 1
updated Feb 22, 2021
No access to inherited members of a struct in acsl clauses.

#941 · created Jul 23, 2014 by mantis-gitlab-migration bug frama-clang
- CLOSED
- 2
updated Feb 22, 2021
"catch(...)" causes crash

#940 · created Nov 13, 2014 by Jochen Burghardt critical frama-clang
- CLOSED
- 1
updated Feb 22, 2021
use of later-defined nested class type in method signature causes error

#939 · created Dec 11, 2014 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
Value analysis generates incorrect Imperative outputs for arrays

#918 · created Dec 12, 2014 by mantis-gitlab-migration enhancement eva
- CLOSED
- 3
updated Feb 22, 2021
ptest doesn't abort tests for which the command is incorrect

#909 · created Jan 22, 2015 by Valentin Perrelle bug compilation
- 0
updated Feb 22, 2021
"*" in quantifier in axiom causes SEGV

#905 · created Jan 29, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
"\at" doesn't accept predicate argument label

#904 · created Jan 26, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
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
logic function call in rhs of relation chain causes abort

#902 · created Jan 22, 2015 by Jochen Burghardt bug frama-clang
- CLOSED
- 1
updated Feb 22, 2021
name in contract should refer to logic function, if defined, even in presence of homonymous C++ method

#901 · created Jan 22, 2015 by Jochen Burghardt enhancement frama-clang
- CLOSED
- 1
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
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

Prev
1
…
57
58
59
60
61
62
63
64
65
…
74
Next