--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on August 2015 ---
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