- Feb 05, 2016
-
-
Julien Signoles authored
-
Julien Signoles authored
-
- Feb 03, 2016
-
-
Julien Signoles authored
-
- Jan 29, 2016
-
-
Julien Signoles authored
-
- Jan 27, 2016
-
-
Julien Signoles authored
-
- Jan 26, 2016
-
-
Julien Signoles authored
Bugfix for memory size computations/Embedded printf - Fixed a bug in computation of the heap size via updates of the `__memory_size` variable. - Added a test case for the above (e-acsl-runtime/memsize.c). - Added embedded printf to the C memory model. This removes functionality from stdio.h and assert.h headers. - Small updates and stylistic issues in the C code of the memory model. See merge request !21
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
Replaced system-wide assertions with custom assertions using embedded printf library
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
consistent with the rest of the C files
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
since the latter is faster
-
Kostyantyn Vorobyov authored
they are more generic and not exposed to the global scope
-
Kostyantyn Vorobyov authored
so they are restricted to e_acsl_mmodel.c compile unit
-
Kostyantyn Vorobyov authored
(__memory_size) is computed correctly
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
tracked heap memory to be computed incorrectly for the following cases: - realloc is supplied 0 - realloc fails
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
- Jan 20, 2016
-
-
Boris Yakobowski authored
-
- Jan 19, 2016
-
-
David Bühler authored
-
- Jan 18, 2016
-
-
Boris Yakobowski authored
-
- Jan 15, 2016
-
-
Julien Signoles authored
[Makefile] fix installation with non-standard prefix Create `BINDIR` directory if necessary before copying file into it. See merge request !23
-
Andre Maroneze authored
-
Boris Yakobowski authored
better handling of \valid on pointers to empty structs in Value
-
- Jan 14, 2016
-
-
Boris Yakobowski authored
Adapt to branch feature/boris/valid-function-predicate See merge request !20
-
Boris Yakobowski authored
-
- Jan 08, 2016
-
-
Julien Signoles authored
Feature/annotate assembly Branch compatible with Frama-C branch of the same name (MR 486). See merge request !22
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
- Jan 07, 2016
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-