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] small function yields 7K proof obligations??

  • Subject: [Frama-c-discuss] small function yields 7K proof obligations??
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Tue, 20 Jul 2010 09:20:29 -0400
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>