--- layout: fc_discuss_archives title: Message 37 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??



Hello,
 
Assuming the following typedefs et defines:
    typedef unsigned int bool;
    typedef int int32_t;
    typedef unsigned long uint64_t;
    #define true 1
    #define false 0
 
this example of code is a good candidate for the "-fast-wp" Why option (Leino's quadractic implementation for WP computation).
Trying 
    frama-c -jessie loe.c -jessie-why-opt="-fast-wp"
gives good results!
 
Indeed, boolean expressions in the code introduce lots of different control flows and so an explosion of the number of POs.
 
HTH
D.
 


________________________________

	De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Alwyn Goodloe
	Envoy? : mardi 20 juillet 2010 15:20
	? : frama-c-discuss
	Objet : [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/17f1557f/attachment.htm>