Issues · pub / frama-c · GitLab

Range of remainder of two positive integers, wrong and missing assertions.

#627 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
requires in beahviors do not behave as expected

#626 · created Jun 12, 2015 by David Cok bug wp
- CLOSED
- 2
updated Feb 22, 2021
validity of obligation from statement contract depends on whether the statement is enclosed in block {}

#625 · created Jun 01, 2015 by Jochen Burghardt bug wp
- CLOSED
- 3
updated Aug 05, 2021
do ... while{ } loop and -wp-invariants option

#624 · created May 19, 2015 by Lionel Blatter bug wp
- CLOSED
- 1
updated Feb 22, 2021
normalization of "assigns" in statement contract doens't cope with introduced auxiliary variables

#622 · created Apr 09, 2015 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Mar 30, 2021
unable to use lemma separated_region

#620 · created Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
Sessions and WP do not interact properly

#618 · created Jan 06, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
deficient axioms

#617 · created Jun 29, 2015 by David Cok bug wp
- CLOSED
- 1
updated Feb 22, 2021
Error when struct has no members

#612 · created Jul 15, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 14, 2021
bound variable names in Coq file depend on unrelated function later in C source code

#601 · created Aug 31, 2015 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Apr 15, 2021
invalid statement contract ("assigns") verified with CVC4 under strange circumstances

#599 · created Apr 30, 2015 by Jochen Burghardt bug wp
- CLOSED
- 14
updated Feb 22, 2021
Slow in proof obligation generation

#598 · created Sep 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
assertion failure using memset on a char

#595 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations

#593 · created Sep 21, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."

#592 · created Sep 21, 2015 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
Unable to prove things that are provable, gets confused

#584 · created Oct 18, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579

#582 · created Oct 27, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32

#579 · created Nov 30, 2015 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)

#578 · created Dec 03, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 2021
WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

#571 · created Jun 02, 2015 by Virgile Prevosto bug wp
- CLOSED
- 1
updated Feb 22, 2021

Prev
1
…
3
4
5
6
7
8
9
10
11
…
13
Next