- Jun 19, 2020
-
-
Patrick Baudin authored
-
Basile Desloges authored
[eacsl] Add support for bitwise operators when using C integer types See merge request frama-c/frama-c!2635
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
[eacsl] Add support to create GMP rational from GMP integer Closes e-acsl#120 See merge request frama-c/frama-c!2700
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
[eacsl] Fix VLA memory tracking Closes e-acsl#119 See merge request frama-c/frama-c!2715
-
- Jun 18, 2020
-
-
Virgile Prevosto authored
[Eva] Eval_terms: fixes an error message. See merge request frama-c/frama-c!2696
-
Virgile Prevosto authored
[Analysis-scripts] fix issues with relative paths in JCDB See merge request frama-c/frama-c!2712
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
- Remove the renaming of Frama-C built-ins in the injector since the code printer is now responsible for it; - Explicitely add calls to `store_block` (resp. `delete_block`) when allocating (resp. deallocating) a VLA.
-
Basile Desloges authored
-
Basile Desloges authored
-
Basile Desloges authored
Remove unused labelled argument and simplify the function as a result.
-
Julien Signoles authored
[eacsl:codegen] Support of variadic functions in `Constructor.mk_lib_call` See merge request frama-c/frama-c!2706
-
Virgile Prevosto authored
fix handling of `loop assigns` by `Annotations.add_code_annot` Closes #883 See merge request frama-c/frama-c!2702
-
Basile Desloges authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
it seems like part of the issue lies in the fact that the cache might be looked at from different cwd. Anyways, proposing an absolute location can't hurt.
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
-
Virgile Prevosto authored
When loading some state, it may happen that some annotations are found to have been emitted by emitters that are no longer usable. This commit let the kernel adopt them, keeping them available as was the case before refactoring `Annotations.code_annot` to use `Annotations.code_annot_emitter`.
-
Virgile Prevosto authored
code duplication started to become a bit problematic
-
-
Virgile Prevosto authored
-
Virgile Prevosto authored
All loop assigns corresponding to a given set of behaviors are now merged together instead of being split into emitters. This is the same as what is done for statement contracts and will make it much easier for callers to identify appropriate loop assigns
-
Virgile Prevosto authored
-
- Jun 17, 2020
-
-
Loïc Correnson authored
[ivette] Property table: adds better tooltips to property and alarm kinds See merge request frama-c/frama-c!2717
-
Loïc Correnson authored
[Kernel] projectify option -add-symbolic-path See merge request frama-c/frama-c!2719
-