--- layout: fc_discuss_archives title: Message 42 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



"Usually, the advice if you want to verify your code for an arbitrary
length /n/ is to use a constant N in your code and then define a concrete
value for N on the command line before doing the analysis, using a shell
script to change N from 0 to the-biggest-value-you-want. Of course, you'll
need to get all analysis results and check you have no warning in each one
of them."

Hmm.. this is a useful technique, but I think frama's value analysis could
make it much more convenient by building in support in frama.  For
example, why not support a "forall N in 1..2048" type notation and then
repeat the analysis for each value, and then finally merge the results?
This would probably be a bit more efficient than using an external
driver to vary the parameters, provide better merging of results and
be more convenient to run.



On Wed, Aug 19, 2015 at 9:55 PM, David MENTRE <dmentre at linux-france.org>
wrote:

> Hello Tim,
>
> Le 20/08/2015 02:12, Tim Newsham a écrit :
>
>> I would like to prove that some code is safe for all buffers you can pass
>> in
>> as input. Is there a way to construct an arbitrary sized buffer (say
>> char*)
>> in frama such that all values are arbitrary ([--..--]) and so that the
>> properties \valid(p + (0..sz-1)) and \initialized(p + (0..sz-1)) hold?
>>
>
> Partially.
>
> For initialisation, you can use Frama_C_make_unknown() available in
> __fc_builtin.h, but you still need to give the size "l" and ensure the
> buffer is \valid.
>
> /*@ requires \valid(p + (0 .. l-1));
>     assigns p[0 .. l-1] \from Frama_C_entropy_source;
>     assigns Frama_C_entropy_source \from Frama_C_entropy_source;
>     ensures \initialized(p + (0 .. l-1));
> */
> void Frama_C_make_unknown(char *p, size_t l);
>
>
> You can use Frama_C_interval() to initialize "l" in a proper range,
> relying on a big enough buffer to ensure its \validity.
>
>  char a[255];
>  int n = Frama_C_interval(0, 255);
>  Frama_C_make_unknown(a, n);
>  do_my_code(a, n);
>
> I've done that once but I encountered issues afterwards (can't remember
> exactly why).
>
> Usually, the advice if you want to verify your code for an arbitrary
> length /n/ is to use a constant N in your code and then define a concrete
> value for N on the command line before doing the analysis, using a shell
> script to change N from 0 to the-biggest-value-you-want. Of course, you'll
> need to get all analysis results and check you have no warning in each one
> of them.
>
> Something like (not tested):
>
> int main(void)
> {
>  #include <__fc_builtin.h>
>
>  char a[N];
>  Frama_C_make_unknown(a, N);
>  do_my_code(a, N);
> }
>
> Then, in Bash:
>
>  for N in {1 .. 255}; do // or maybe "for N in 0 1 2 254 255; do"
>    frama-c -cpp-extra-args="-D=$N" -val file.c > result-$N.log
>  done
>
>
> Best regards,
> david
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss




-- 
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150825/b2fd1ead/attachment.html>