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



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