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
[WP] Assertion failed in Instance tactic called from a custom strategy

#2600 · created Mar 15, 2022 by Lélio Brun wp
- 1
updated May 09, 2022
[WP] Out of memory crash

#2597 · created Mar 15, 2022 by Lélio Brun bug confirmed wp
- 2
updated Apr 20, 2022
[WP] Type mismatch with Real model

#2596 · created Mar 15, 2022 by Lélio Brun bug confirmed wp
- 1
updated Mar 15, 2022
[WP] Failure to verify range information after bitwise and on signed integers

#2589 · created Jan 03, 2022 by GuerricChupin wp
- CLOSED
- 4
updated Jan 11, 2022
[WP] Soundness issue when handling a pointer on a structure containing an array.

#2575 · created Sep 20, 2021 by AlexCid feedback-needed wp
- CLOSED
- 1
- 6
updated Oct 06, 2021
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
[Plug-in wp] 96-bits floats

#2560 · created Jun 08, 2021 by arun-babu feedback-needed kernel wp
- 1
updated Oct 06, 2021
Error: Unbound value Why3.Whyconf.load_default_config_if_needed 1 of 3 tasks completed

#2548 · created Mar 30, 2021 by Qix confirmed wp
- CLOSED
- 1
- 3
updated Apr 13, 2021
"Unknown Error" with Alt-Ergo 3 of 3 tasks completed

#2547 · created Mar 26, 2021 by Qix wp
- CLOSED
- 11
updated Jun 01, 2021
An option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflows 3 of 3 tasks completed

#54 · created Jan 29, 2021 by varosi eva wp
- 3
updated Mar 29, 2021
Why3 configuration for Frama-C

#47 · created Dec 11, 2020 by Allan Blanchard wp
- 0
updated Mar 31, 2021
Question: Dump why3 file generated by frama-c

#46 · created Dec 06, 2020 by Leo Viezens wp
- CLOSED
- 3
updated Aug 05, 2021
Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems 3 of 3 tasks completed

#41 · created Nov 01, 2020 by Jens Gerlach wp
- CLOSED
- 1
- 28
updated Apr 13, 2021
z3 ERROR: unknown parameter 'model_compress'

#55 · created Oct 15, 2020 by rwmjones bug wp
- CLOSED
- 2
updated Feb 22, 2021
Wanted features related to Why3-Coq

#30 · created Sep 28, 2020 by Allan Blanchard discussion enhancement wp
- 5
updated Oct 02, 2020
WP: Incorrect assigns global/static handling

#18 · created Jun 15, 2020 by Alex Coffin wp
- CLOSED
- 1
- 1
updated Feb 22, 2021

Prev
1
2
3
4
5
…
14
Next