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
- Subject: [Frama-c-discuss] arbitrary buffers in analysis
- From: dmentre at linux-france.org (David MENTRE)
- Date: Thu, 20 Aug 2015 09:55:05 +0200
- In-reply-to: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com>
- References: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- References:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- Prev by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):