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