Issues · pub / frama-c · GitLab

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
Implicit casting from integer to real causes failure in WP proof generation

#413 · created Jul 29, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
expression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in C

#399 · created Jul 28, 2016 by Jochen Burghardt ACSL enhancement kernel
- CLOSED
- 2
updated Feb 22, 2021
Ocamlfind cannod be found

#416 · created Jul 05, 2016 by mantis-gitlab-migration bug kernel
- CLOSED
- 5
updated Feb 22, 2021
Frama-C is unsound when employing both alt-ergo and cvc4

#394 · created Jun 30, 2016 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021
tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"

#138 · created Jun 27, 2016 by Jochen Burghardt documentation
- CLOSED
- 1
updated Feb 22, 2021
Creating a pointer to a local causes valid pointers above it to lose thier valid status

#425 · created Jun 21, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Functions that claim to return a struct but don't cause a crash

#344 · created Jun 21, 2016 by mantis-gitlab-migration critical kernel
- CLOSED
- 3
updated Feb 22, 2021
workaround for coq-8.5.1 issue?

#403 · created Jun 16, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 7
updated Feb 22, 2021
Use of very large real constants cause failures in proof generation in WP

#507 · created Jun 14, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
Incorrect code generation with gmp

#378 · created Jun 14, 2016 by Kostyantyn Vorobyov bug e-acsl
- CLOSED
- 1
updated Feb 22, 2021
missing lower bound of ACSL operator ".." not detected by Magnesium

#494 · created Jun 13, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 6
updated Feb 22, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
\valid(a + (0..9)) vs \valid(a[0..9])

#512 · created Apr 13, 2016 by David Cok ACSL bug kernel
- CLOSED
- 2
updated Feb 22, 2021
the documented grammar does not allow completeness clauses in statement contracts

#395 · created Apr 13, 2016 by David Cok ACSL bug
- CLOSED
- 4
updated Feb 22, 2021
Make find(1) command POSIX-compliant

#513 · created Apr 09, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Aug 05, 2021
Crash with large array initialisation

#514 · created Mar 18, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Apr 15, 2021

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