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??

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>