- Oct 09, 2024
-
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
- Oct 08, 2024
-
-
Virgile Prevosto authored
-
Virgile Prevosto authored
Refine contracts inferred from GNU extended asm See merge request frama-c/frama-c!4738
-
- Oct 07, 2024
-
-
Allan Blanchard authored
Only keep static inline info in linker table when aggressive-merging is on See merge request frama-c/frama-c!4816
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Remi Lazarini authored
Feature/ivette/callgraph See merge request frama-c/frama-c!4678
-
-
Remi Lazarini authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
- Oct 04, 2024
-
-
David Bühler authored
[Eva] Improves the emission of integer overflow alarms on a/b and a%b See merge request frama-c/frama-c!4809
-
Allan Blanchard authored
[ci] Add Frama-Clang and Minimal to internal plugin tests See merge request frama-c/frama-c!4813
-
Andre Maroneze authored
[ivette] make sure to generate API before install Closes #1454 See merge request frama-c/frama-c!4810
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
Also documents that the behavior of a%b depends on the behavior of a/b.
-
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
Only emits overflow alarms on [a/b] when [a] may be equal to [min_int] AND [b] may be equal to [-1]. Also reduces the values of [a] and [b] when possible.
-
David Bühler authored
According to the C standard, section 6.5.5 §6: "If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a; otherwise, the behavior of both a/b and a%b is undefined."
-
Thibault Martin authored
-
Basile Desloges authored
[e-acsl] fix wrong equality notion used for terms See merge request frama-c/frama-c!4789
-
Andre Maroneze authored
Feature/tests/include deeper tests directories See merge request frama-c/frama-c!4812
-
Loïc Correnson authored
[Ivette] Fixes default view at first launch. Closes #1412 See merge request frama-c/frama-c!4814
-