Issues · pub / frama-c · GitLab

Plug-in inout fails to parse clause /*@ assigns s[..]; */

#1597 · created Apr 28, 2009 by David Delmas enhancement eva
- CLOSED
- 4
updated Feb 22, 2021
wrongly synthesized assert

#1584 · created Jul 16, 2009 by Fabrice Derepas bug eva
- CLOSED
- 4
updated Feb 22, 2021
int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero

#1554 · created May 04, 2009 by Pascal Cuoq bug eva
- CLOSED
- 1
updated Feb 22, 2021
if((int)(&a+2)) fails to warn about being unspecified

#1553 · created May 05, 2009 by Pascal Cuoq bug eva
- CLOSED
- 1
updated Feb 22, 2021
propagation of \result clauses

#1542 · created Jan 21, 2010 by Jean-François Lalande enhancement eva
- CLOSED
- 2
updated Feb 22, 2021
Incorrect 'assert false' in value analysis

#1536 · created Feb 01, 2010 by Boris Yakobowski critical eva
- CLOSED
- 0
updated Feb 22, 2021
malloc.h can't be preprocessed: __func__ is not a macro

#1526 · created Nov 03, 2009 by mantis-gitlab-migration bug eva
- CLOSED
- 3
updated Feb 22, 2021
non-constant size of 2-dim array leads to crash (some similarities to issue #852)

#1481 · created Jun 07, 2011 by mantis-gitlab-migration critical eva
- CLOSED
- 7
updated Feb 22, 2021
Double version of program considerably slower to analyze than float version (svn 19535)

#1444 · created Aug 03, 2012 by mantis-gitlab-migration bug eva
- CLOSED
- 23
updated Feb 22, 2021
FRAMA_C_MALLOC_INFINITE not used in stdlib.c

#1418 · created Jun 18, 2012 by mantis-gitlab-migration bug eva
- CLOSED
- 4
updated Feb 22, 2021
wrong origin displayed in the GUI

#1402 · created Sep 20, 2009 by Pascal Cuoq bug eva
- CLOSED
- 5
updated Feb 22, 2021
relation chains exploited incompletely

#1394 · created Jan 26, 2012 by Jochen Burghardt enhancement eva
- CLOSED
- 6
updated Feb 22, 2021
suggest to use "NULL" rather than "&NULL" for null pointer

#1389 · created Jan 19, 2012 by Jochen Burghardt eva
- CLOSED
- 3
updated Feb 22, 2021
Emitted assertion wrongly reduces to bottom (apparently) (csmith)

#1379 · created Nov 19, 2011 by Pascal Cuoq bug eva
- CLOSED
- 12
updated Feb 22, 2021
Bad AST generation ?

#1374 · created Apr 04, 2012 by mantis-gitlab-migration bug eva
- CLOSED
- 5
updated Feb 22, 2021
File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed

#1320 · created Jul 25, 2011 by Benjamin Monate critical eva
- CLOSED
- 2
updated Feb 22, 2021
Results differ between value analysis and GCC on bitfields

#1316 · created Jul 25, 2011 by Benjamin Monate bug eva
- CLOSED
- 2
updated Feb 22, 2021
Crash du builtin memcpy, par une exception non rattrapable

#1313 · created Jul 07, 2011 by Boris Yakobowski critical eva
- CLOSED
- 3
updated Feb 22, 2021
wrong interpretation when a bit-field receives the result of a function (csmith)

#1289 · created May 11, 2011 by Pascal Cuoq bug eva
- CLOSED
- 2
updated Feb 22, 2021
Serial conversions in function result (csmith)

#1275 · created Apr 17, 2011 by Pascal Cuoq bug eva
- CLOSED
- 2
updated Feb 22, 2021

Prev
1
2
3
4
5
6
7
Next