Issues · pub / frama-c · GitLab

suggest to report column number for warnings

#363 · created Jan 09, 2017 by Jochen Burghardt enhancement eva
- CLOSED
- 1
updated Feb 22, 2021
WP inserts unwanted new lines into Coq proofs

#385 · created Jan 02, 2017 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
Why3 warning

#387 · created Dec 16, 2016 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
more prover processes run than expected

#388 · created Dec 15, 2016 by Jens Gerlach bug wp
- CLOSED
- 4
updated Apr 15, 2021
error in Coq file generation

#405 · created Dec 03, 2016 by Alain Giorgetti bug wp
- CLOSED
- 1
updated Apr 15, 2021
suggest to provide and document a unique warning string to grep for in value-analysis output files

#297 · created Nov 28, 2016 by Jochen Burghardt eva
- CLOSED
- 4
updated Feb 22, 2021
Annotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.

#401 · created Nov 24, 2016 by mantis-gitlab-migration bug rte
- CLOSED
- 3
updated Feb 22, 2021
wrong example code in value analysis manual, p.35, for message " invalid LHS operand for left shift"

#391 · created Nov 21, 2016 by Jochen Burghardt documentation
- CLOSED
- 2
updated Feb 22, 2021
Ocaml 4.04.0 build error

#393 · created Nov 09, 2016 by mantis-gitlab-migration bug kernel
- CLOSED
- 2
updated Feb 22, 2021
File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h

#314 · created Oct 17, 2016 by Jochen Burghardt bug libc
- CLOSED
- 4
updated Apr 01, 2021
Failure to compile on windows using cygwin

#390 · created Oct 14, 2016 by mantis-gitlab-migration bug documentation
- CLOSED
- 3
updated Feb 22, 2021
GMP typing issue

#343 · created Oct 14, 2016 by Kostyantyn Vorobyov bug e-acsl
- CLOSED
- 0
updated Feb 22, 2021
Unterminated comment while generating division-by-zero assertion

#404 · created Oct 13, 2016 by Kostyantyn Vorobyov bug kernel
- CLOSED
- 5
updated Feb 22, 2021
__attribute__((aligned(0))) tacitly causes sizeof computation to fail

#402 · created Oct 13, 2016 by Jochen Burghardt kernel
- CLOSED
- 6
updated Feb 22, 2021
option "-print" prints array upper bound in type before parameter name, rather than after it

#392 · created Oct 06, 2016 by Jochen Burghardt kernel
- CLOSED
- 1
- 2
updated Apr 16, 2021
Compiling on Windows (cygwin) fails

#396 · created Oct 01, 2016 by mantis-gitlab-migration bug documentation
- CLOSED
- 7
updated Feb 22, 2021
Switch statements seem to be unsound

#397 · created Aug 19, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Nested scopes may cause issues with the validity of created pointers

#409 · created Aug 17, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Logic with read clauses can have their values invalidated by writes to separated memory locations

#410 · created Aug 08, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Aug 05, 2021
"Builtin already registered" after Reparse

#398 · created Jul 30, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Feb 22, 2021

Prev
1
…
7
8
9
10
11
12
13
14
15
…
64
Next