--- layout: fc_discuss_archives title: Message 120 from Frama-C-discuss on November 2013 ---
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>