--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] small function yields 7K proof obligations??



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>