--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis



>
>
> You are looking for the value analysis built-in Frama_C_interval_split,
> documented at
> http://blog.frama-c.com/index.php?post/2012/10/10/RERS-2012-competition-problems-1-9
> You will need to have the slevel option set high enough in conjunction
> with it for it to work properly.
>

I mean in general when you want the analyzer to does N separate analyses
with N different values of some variable n. That doesn't work for creating
buffers of size n, because there is no malloc, sorry.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150825/e91db6e5/attachment-0001.html>