Issues · pub / frama-c · GitLab

wrong proof obligation generated with axiomatic def and array quantification

#2375 · created Dec 15, 2009 by Jochen Burghardt bug jessie
- CLOSED
- 3
updated Apr 15, 2021
"why" reports "unbound label"

#2376 · created Dec 15, 2009 by Jochen Burghardt bug jessie
- CLOSED
- 3
updated Apr 15, 2021
Plugin jessie aborted because of an internal error.

#2269 · created Dec 16, 2009 by mantis-gitlab-migration critical jessie
- CLOSED
- 4
updated Apr 15, 2021
complete/disjoint behaviors shouldn't accept undefined behaviors

#2397 · created Dec 24, 2009 by mantis-gitlab-migration bug jessie
- CLOSED
- 2
updated Apr 15, 2021
Unicode minus sign (U+2212) not accepted by Jessie, yet used in documentation, causing mysterious failure

#1639 · created Jan 04, 2010 by mantis-gitlab-migration bug jessie
- CLOSED
- 2
updated Apr 15, 2021
bug with constants like 1E-6

#2374 · created Jan 07, 2010 by mantis-gitlab-migration bug jessie
- CLOSED
- 4
updated Apr 15, 2021
Decreases clause

#2329 · created Jan 13, 2010 by Dillon Pariente bug jessie
- CLOSED
- 1
updated Apr 15, 2021
pragma JessieIntegerModel

#2373 · created Jan 13, 2010 by Dillon Pariente bug jessie
- CLOSED
- 3
updated Apr 15, 2021
Global invariants are not verified

#2431 · created Jan 14, 2010 by Guillaume Melquiond bug jessie
- CLOSED
- 1
updated Apr 15, 2021
unsigned long long constant becomes signed

#2395 · created Jan 19, 2010 by mantis-gitlab-migration bug jessie
- CLOSED
- 2
updated Apr 15, 2021
Burstall-Bornat style on array init

#1541 · created Jan 20, 2010 by Dillon Pariente bug jessie
- CLOSED
- 3
updated Apr 15, 2021
\separated

#1962 · created Jan 21, 2010 by mantis-gitlab-migration critical jessie
- CLOSED
- 3
updated Apr 15, 2021
int32 and real can't be unified

#2384 · created Feb 01, 2010 by Sylvie Boldo bug jessie
- CLOSED
- 3
updated Apr 15, 2021
Why keywords as ACSL identifiers

#2383 · created Feb 03, 2010 by Julien Signoles enhancement jessie
- CLOSED
- 2
updated Apr 15, 2021
Statement contract and "hiding" of statement

#2382 · created Feb 06, 2010 by Dillon Pariente bug jessie
- CLOSED
- 3
updated Apr 15, 2021
Jessie translation unexpected failure

#1540 · created Feb 11, 2010 by David Delmas critical jessie
- CLOSED
- 2
updated Apr 15, 2021
assert false (* TODO *)

#1537 · created Feb 16, 2010 by Sylvie Boldo bug jessie
- CLOSED
- 4
updated Apr 15, 2021
Jessie translation unexpected failure

#2328 · created Feb 17, 2010 by Victoria Moya Lamiel critical jessie
- CLOSED
- 2
updated Apr 15, 2021
-2147483647<=0 unprovable by Simplify, except in switch

#2419 · created Feb 22, 2010 by Jochen Burghardt enhancement jessie
- CLOSED
- 2
updated Apr 15, 2021
local array decl with non-constant size causes Why error

#2423 · created Feb 22, 2010 by Jochen Burghardt bug jessie
- CLOSED
- 1
updated Apr 15, 2021

Prev
1
…
6
7
8
9
10
11
12
13
14
…
74
Next