Issues · pub / frama-c · GitLab

Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires

#357 · created Apr 23, 2014 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 2021
Axiomatic is recompiled when using severalprocesses

#356 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 1
updated Feb 22, 2021
Cast on funspec not considering typedef

#355 · created Oct 25, 2013 by Dillon Pariente bug kernel
- CLOSED
- 5
updated Feb 22, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4

#353 · created Mar 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
axiom about bounds of lsl result needed in the long run

#352 · created May 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
Some ACSL mathematical functions crash WP

#351 · created May 10, 2017 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · created May 08, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
sigsetjmp and siglongjmp in setjmp.h

#349 · created Jun 25, 2015 by mantis-gitlab-migration enhancement libc
- CLOSED
- 2
updated Feb 22, 2021
preprocessor fail: unterminated comment

#348 · created May 30, 2017 by mantis-gitlab-migration bug kernel
- 5
updated Feb 22, 2021
type of float parameter changed unexpectedly to double

#347 · created Feb 24, 2017 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
E-ACSL type system crash

#346 · created Feb 24, 2017 by Kostyantyn Vorobyov critical e-acsl
- CLOSED
- 0
updated Feb 22, 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
GMP typing issue

#343 · created Oct 14, 2016 by Kostyantyn Vorobyov bug e-acsl
- CLOSED
- 0
updated Feb 22, 2021
There is a typo in description of plug-in: "objuscator" instead of "obfuscator".

#342 · created Jan 12, 2017 by mantis-gitlab-migration obfuscator
- CLOSED
- 0
updated Feb 22, 2021
Operability depends on the order of options changes

#341 · created Feb 03, 2017 by mantis-gitlab-migration bug eva
- CLOSED
- 7
updated Feb 22, 2021
EVA analysis does not start with click on "Execution" button.

#340 · created Feb 10, 2017 by mantis-gitlab-migration enhancement eva
- CLOSED
- 3
updated Feb 22, 2021
Invalid results in presence of pseudo-recursive calls in inout and from

#339 · created Feb 20, 2011 by Boris Yakobowski bug inout
- CLOSED
- 5
updated Feb 22, 2021
Incorrectness when early exiting a block

#338 · created Apr 07, 2014 by Julien Signoles bug e-acsl
- CLOSED
- 0
updated Feb 22, 2021
suggest to check (loop) assigns clauses by data flow analysis

#337 · created Jun 01, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Aug 05, 2021

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