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] VCs generated on bit operations

  • Subject: [Frama-c-discuss] VCs generated on bit operations
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Tue, 26 Nov 2013 21:05:26 -0500
Hi All,
   As I go through the VCs produced by jessie, I noticed VCs left  unprovable by automatic provers(Ergo, CVC, etc). After splitting the conjunctions, they can not be proved either. 
   I looked at the VCs in details. They do not appear straight-forward to me. My guess, might be incorrect, is that they come from the bit-shift and bit-and operations from C code.  I can hardly interpret the VC shown in why3IDE up-right corner. Also i am interested in knowing why they are given and how to make use of them.. Any ideas?
   Many thanks.

xiao-lei 

   Here are two examples I run into:

1) code segment:
/*@
    behavior b1:
        assumes (level >= LVL_MSK_HW_ERR) && (level <= LVL_EXTINT4);
        ensures \result==OK;
    behavior b2:
        assumes !((level >= LVL_MSK_HW_ERR) && (level <= LVL_EXTINT4));
        ensures \result==ERROR;
 @*/
STATUS itp_level_disable(INT level)
{
    FAST UINT temp;
    FAST INT key;

    if ((level >= 1) && (level <= 14))
    {
        temp = (0x1 << level);
    //do some work with temp here
        return (OK);
    }
    return (ERROR);
}


Unproved VC shown in why3IDE up-right conner:

  constant level : int32
  
  axiom H : integer_of_int32 level >= 1
  
  axiom H1 : integer_of_int32 level <= 14
  
  goal WP_parameter_itp_level_disable_ensures_default :
    integer_of_int32 level >= 0 &&
     integer_of_int32 level < 32 &&
      1 <= asr 2147483647 (integer_of_int32 level)
end
---------------------------------------------------------------------------
 
2. 

#define TRAP_DEBUG_ENABLE        ((unsigned int)(0X80000000))

unsigned int  Sys_health = 0 ;

VOID os_init(VOID)
{
   //..... some code

    if ( TRAP_DEBUG_ENABLE == (Sys_health & TRAP_DEBUG_ENABLE) )
    {
        // some code
    }
}

Unproved VC shown in why3IDE up-right corner:

 goal WP_parameter_szos_init_safety :
    0 <= bw_and (integer_of_uint32 usSys_health) 2147483648 /\
     bw_and (integer_of_uint32 usSys_health) 2147483648 <= 4294967295
 end

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131126/5916c185/attachment.html>