--- layout: fc_discuss_archives title: Message 120 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VCs generated on bit operations



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>