Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis

It doesn't seem that will work to verify all buffer
sizes (for example, l=0xffffffffffffffff on 64-bit memory spaces).

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/20150820/fa18ce2a/attachment.html>