Issues · pub / frama-c · GitLab

for a pointer int *p, the expression "(p+1)-p" evaluates to 4 in ACSL rather than to 1 (as in C)

#677 · created Feb 19, 2015 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
Crash with \is_infinite

#550 · created Feb 24, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
Able to assert a false statement

#803 · created Mar 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
False valid with LONG_MIN

#802 · created Mar 06, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
readability of coq(?) names

#104 · created Mar 31, 2015 by Jens Gerlach bug wp
- CLOSED
- 6
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
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
do ... while{ } loop and -wp-invariants option

#624 · created May 19, 2015 by Lionel Blatter bug wp
- CLOSED
- 1
updated Feb 22, 2021
WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

#635 · created Jun 01, 2015 by Virgile Prevosto bug wp
- CLOSED
- 1
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
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
*i == *j cannot be proven from i == j

#631 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
*off == off_cpy cannot be proven just after the assignment *off = off_cpy

#628 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
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
Unprovable inequality involving (unsigned) -1

#570 · created Jun 04, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Under windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishing

#492 · created Jun 11, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 0
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
deficient axioms

#617 · created Jun 29, 2015 by David Cok bug wp
- CLOSED
- 1
updated Feb 22, 2021
Incorrect result with X modulo 1

#547 · created Jul 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
crash in presence of \result in assigns

#541 · created Jul 07, 2015 by David Cok critical wp
- CLOSED
- 2
updated Feb 22, 2021

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