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

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