- Sep 30, 2024
-
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
- Plugins fields in the AST are used to find the right extension - A plugin still cannot register twice an extension - If plugin is not given, can throw ambiguity error - Kernel extensions are an exception, a plugin cannot register an extension with the name name than the kernel
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
- Cil_types.acsl_extension - Logic_ptree.extension & global_extension
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
Thibault Martin authored
-
- Sep 27, 2024
-
-
Andre Maroneze authored
[Libc] add some POSIX and non-POSIX constants See merge request frama-c/frama-c!4792
-
Andre Maroneze authored
-
Andre Maroneze authored
Adds help to Eva message categories See merge request frama-c/frama-c!4798
-
-
-
-
Andre Maroneze authored
[kernel] Add optional description to keys See merge request frama-c/frama-c!4780
-
- Sep 26, 2024
-
-
Virgile Prevosto authored
[Libc] undefine 'index'/'rindex' if POSIX >= 200809 Closes #1422 See merge request frama-c/frama-c!4795
-
Andre Maroneze authored
-
-
-
-
-
-
-
Thibault Martin authored
[kernel] fix pretty printing of assigns-from clauses Closes #1398 See merge request frama-c/frama-c!4796
-
-
Andre Maroneze authored
[Eva] Offsetmap: removes some feedback messages about approximations. See merge request frama-c/frama-c!4777
-
David Bühler authored
-
David Bühler authored
In offsetmaps, removes a reference to change the feedback emitted when approximating the write of large memory locations. Instead, the main offsetmap functor takes an additional parameter about whether such messages should be emitted. Only the offsetmaps build by the Eva cvalue domain emits these messages, as write approximations may have a significant impact on the analysis precision. Offsetmaps used to represent memory zones or dependiencies do not emit these messages, which were most often insignificant and instable (as many plug-ins and Eva domains use memory zones in various ways).
-
Andre Maroneze authored
-
- Sep 25, 2024
-
-
Andre Maroneze authored
-
Virgile Prevosto authored
[Kernel] avoid stacktrace and show more precise plugin loading error message See merge request frama-c/frama-c!4754
-
Virgile Prevosto authored
[cabs2cil] Use CALL loc as vdecl for missing prototypes See merge request frama-c/frama-c!4791
-