--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on July 2010 ---
I have a small (20 lines) program mostly performing simple array updates that for function safety has 7102 proof obligations. Is this sort of thing common? Alt-Ergo seems discharge them albeit slowly (that is it worked on about 200 of them overnight and I killed it this morning). I give the main data structure and the code below. It's produced by a code generator so it is convoluted. I'm mostly wondering if this sort proof obligation explosion is common. ---------- -- struct { /* copilotState */ struct { /* t1 */ bool prophVal__y[3]; int32_t prophVal__x[4]; bool outputVal__z; bool outputVal__y; int32_t outputVal__x; } t1; } copilotState = { /* copilotState */ { /* t1 */ /* prophVal__y */ { true , false , false }, /* prophVal__x */ { 0L , 1L , 2L , 0L }, /* outputVal__z */ false, /* outputVal__y */ false, /* outputVal__x */ 0L } }; /*@ requires \valid_range(copilotState.t1.prophVal__x,0,3); @ requires \valid_range(copilotState.t1.prophVal__y,0,2); */ static void __r1() { bool __0 = true; uint64_t __1 = 0ULL; bool __2 = copilotState.t1.prophVal__y[__1]; uint64_t __3 = 1ULL; int32_t __4 = copilotState.t1.prophVal__x[__3]; int32_t __5 = copilotState.t1.prophVal__x[__1]; bool __6 = __4 < __5; bool __7 = __2 && __6; bool __8 = ! __7; bool __9 = ! __2; bool __10 = ! __6; bool __11 = __9 && __10; bool __12 = ! __11; bool __13 = __8 && __12; bool __14 = ! __13; uint64_t __15 = 2ULL; if (__0) { } copilotState.t1.prophVal__y[__15] = __14; } -- Alwyn E. Goodloe, Ph.D. agoodloe at gmail.com Computer Scientist National Institute of Aerospace -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100720/7077f921/attachment.htm>