Issues · pub / frama-c · GitLab

frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).

#263 · opened May 29, 2018 by mantis-gitlab-migration critical jessie
- CLOSED
- 1
updated Apr 20, 2021
Missing cast in code generated by RTE

#181 · opened Dec 17, 2018 by Julien Signoles bug confirmed rte
- CLOSED
- 1
updated Apr 20, 2021
E-ACSL crash with RTE generated assertion with booleans

#180 · opened Dec 03, 2018 by mantis-gitlab-migration confirmed critical e-acsl
- CLOSED
- 11
updated Apr 20, 2021
option "-print" prints array upper bound in type before parameter name, rather than after it

#392 · opened Oct 06, 2016 by Jochen Burghardt kernel
- CLOSED
- 1
- 2
updated Apr 16, 2021
Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")

#1867 · opened May 09, 2013 by mantis-gitlab-migration bug compilation
- CLOSED
- 2
updated Apr 15, 2021
Translation of tsets

#1900 · opened Apr 15, 2013 by Julien Signoles enhancement wp
- CLOSED
- 6
updated Apr 15, 2021
WP-Plugin crashes due to an internal error when terms of sets during union have different types

#919 · opened Dec 22, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")

#43 · opened Nov 06, 2020 by Jens Gerlach
- CLOSED
- 1
- 19
updated Apr 15, 2021
quantifiers over logic types do not restrict to valid instances

#91 · opened Jan 30, 2020 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Apr 15, 2021
Eprover in Frama-C 20 beta

#103 · opened Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
statement contract apparently confuses parser

#324 · opened May 11, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
false postcondition shouldn't be verified in default memory-model setting

#333 · opened Jun 15, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 2021
naming the default behavior influences proven obligations

#336 · opened Jun 01, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · opened May 08, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
Some ACSL mathematical functions crash WP

#351 · opened May 10, 2017 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
axiom about bounds of lsl result needed in the long run

#352 · opened May 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4

#353 · opened Mar 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · opened Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
Lithum- Z3 shell aborts with error message

#1496 · opened Apr 07, 2009 by Virgile Prevosto bug jessie
- CLOSED
- 1
updated Apr 15, 2021
Lithium: behavior, complete disjoint does not work

#1629 · opened Apr 07, 2009 by Virgile Prevosto bug jessie
- CLOSED
- 4
updated Apr 15, 2021

Prev
1
2
3
4
5
…
61
Next