Issues · pub / frama-c · GitLab

WP - unsoundness with union

#2609 · created Apr 22, 2022 by Geoff Hulette confirmed enhancement wp
- 5
updated May 02, 2022
[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter

#2601 · created Mar 15, 2022 by Costava confirmed enhancement wp
- 2
updated Mar 16, 2022
Known WP limitations on statement contract

#2569 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Aug 06, 2021
Known WP limitations on the reads clause 0 of 2 tasks completed

#2568 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Aug 05, 2021
Known WP limitations on `assigns` handling 0 of 2 tasks completed

#2567 · created Aug 05, 2021 by Allan Blanchard enhancement wp
- 0
updated Nov 23, 2021
Default invariant should be inferred for loops

#2534 · created Apr 07, 2009 by Virgile Prevosto enhancement jessie
- CLOSED
- 3
updated Apr 15, 2021
Slicing leaves unreachable code

#2487 · created Jul 15, 2009 by mantis-gitlab-migration enhancement slicing
- CLOSED
- 4
updated Feb 22, 2021
Option -jessie-cpu-limit not taken into account in GUI

#2443 · created Apr 07, 2009 by Virgile Prevosto enhancement jessie
- CLOSED
- 2
updated Apr 15, 2021
ghost integer ?

#2428 · created Feb 01, 2010 by Sylvie Boldo ACSL enhancement kernel
- 0
updated Feb 22, 2021
Better support of //@ style

#2427 · created May 11, 2009 by mantis-gitlab-migration ACSL enhancement kernel
- 2
updated Feb 22, 2021
different translation of casted constants in program-code and in assertion

#2421 · created Mar 22, 2010 by Jochen Burghardt enhancement jessie
- CLOSED
- 1
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
assigns clauses are missing from the sliced program

#2390 · created Feb 04, 2010 by Pascal Cuoq enhancement slicing
- CLOSED
- 3
updated Feb 22, 2021
imprecision in widening/narrowing for char and short index

#2387 · created Feb 19, 2010 by Stephane Duprat enhancement eva
- CLOSED
- 1
updated Feb 22, 2021
Why keywords as ACSL identifiers

#2383 · created Feb 03, 2010 by Julien Signoles enhancement jessie
- CLOSED
- 2
updated Apr 15, 2021
Code containing consts should be verifiable

#2366 · created May 18, 2010 by mantis-gitlab-migration enhancement jessie
- CLOSED
- 1
updated Apr 15, 2021
Enhancement on assigns annotation and the name of proof obligation

#2356 · created Jul 17, 2010 by mantis-gitlab-migration enhancement jessie
- CLOSED
- 1
updated Apr 15, 2021
Suggest to close a section if each obligation is proven by *some* prover

#2346 · created Oct 12, 2010 by Jochen Burghardt enhancement gui
- CLOSED
- 1
updated Feb 22, 2021
Suggest to rename user identifiers to avoid name clashes in ..._why.sx files

#2338 · created Nov 29, 2010 by Jochen Burghardt enhancement jessie
- CLOSED
- 1
updated Apr 15, 2021
no multiple assert-clauses accepted in /*@...*/-style comment

#2323 · created Oct 12, 2010 by Jochen Burghardt ACSL enhancement kernel
- 0
updated Feb 22, 2021

Prev
1
2
3
4
5
…
10
Next