--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on August 2015 ---
Hello Tim, Le 21/08/2015 09:00, David MENTRE a écrit : > YMMV. I haven't look at your code, but it might appear that your > specific code indeed needs hours to check due to some very complex > functions. Or you need optimizations provided by TrustInSoft Analyser > (for memcpy and the like functions). ;-) For what is worth, your code is analysed in 1m40s with TrustInSoft Analyser. It found 6 warnings: bits.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&byte); sha2.c:377:[kernel] warning: accessing uninitialized left-value: assert \initialized(&tmp); auth.c:32:[kernel] warning: accessing uninitialized left-value: assert \initialized(x); frama-driver.c:34:[value] Assertion got status unknown. auth.c:64:[value] Function auth: precondition got status unknown. auth.c:93:[value] Assertion got status unknown. DISCLAIMER: I did this verification very quickly, so I might have badly configured Frama-C or missed an obvious error message! I join to the email the resulting verification log. I didn't look at verification result to understand the warnings. Best regards, david -------------- next part -------------- [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing FRAMAC_SHARE/libc/tis_runtime.c (with preprocessing) [kernel] Parsing FRAMAC_SHARE/mt/mthread_pthread.c (with preprocessing) [kernel] Parsing auth.c (with preprocessing) [kernel] Parsing bits.c (with preprocessing) [kernel] Parsing frama-driver.c (with preprocessing) [kernel] Parsing hmac.c (with preprocessing) [kernel] Parsing seq.c (with preprocessing) [kernel] Parsing sha2.c (with preprocessing) [kernel] Parsing frama-extras.c (with preprocessing) frama-extras.c:39:[kernel] warning: def'n of func memcpy at frama-extras.c:39 (sum 713830) conflicts with the one at FRAMAC_SHARE/libc/string.c:19 (sum 70962); keeping the one at FRAMAC_SHARE/libc/string.c:19. frama-extras.c:50:[kernel] warning: def'n of func memset at frama-extras.c:50 (sum 713830) conflicts with the one at FRAMAC_SHARE/libc/string.c:52 (sum 37378371); keeping the one at FRAMAC_SHARE/libc/string.c:52. [value] Analyzing an incomplete application starting at main [value] Computing initial state [value] Initial state computed [value] using specification for function Frama_C_interval FRAMAC_SHARE/libc/__fc_builtin.h:51:[value] Function Frama_C_interval: precondition got status valid. stack: Frama_C_interval :: frama-driver.c:26 <- main FRAMAC_SHARE/libc/__fc_builtin.h:51:[value] Function Frama_C_interval: precondition got status valid. stack: Frama_C_interval :: frama-driver.c:28 <- main [value] Semantic level unrolling superposing up to 100 states [value] Semantic level unrolling superposing up to 200 states FRAMAC_SHARE/libc/__fc_builtin.h:51:[value] Function Frama_C_interval: precondition got status valid. stack: Frama_C_interval :: frama-driver.c:29 <- main FRAMAC_SHARE/libc/__fc_builtin.h:51:[value] Function Frama_C_interval: precondition got status valid. stack: Frama_C_interval :: frama-driver.c:31 <- main [value] Semantic level unrolling superposing up to 300 states FRAMAC_SHARE/libc/__fc_builtin.h:51:[value] Function Frama_C_interval: precondition got status valid. stack: Frama_C_interval :: frama-driver.c:32 <- main frama-driver.c:34:[value] Assertion got status unknown. auth.c:64:[value] Function auth: precondition got status unknown. stack: auth :: frama-driver.c:37 <- main bits.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&byte); stack: getBit :: bits.c:25 <- proofOfWork :: auth.c:88 <- auth :: frama-driver.c:37 <- main sha2.c:251:[value] Function SHA256_Init: postcondition got status valid. stack: SHA256_Init :: hmac.c:94 <- hmac_sha256_init :: hmac.c:131 <- hmac_sha256 :: auth.c:50 <- checkHmac :: auth.c:90 <- auth :: frama-driver.c:37 <- main sha2.c:251:[value] Function SHA256_Init: postcondition got status valid. stack: SHA256_Init :: hmac.c:97 <- hmac_sha256_init :: hmac.c:131 <- hmac_sha256 :: auth.c:50 <- checkHmac :: auth.c:90 <- auth :: frama-driver.c:37 <- main sha2.c:377:[kernel] warning: accessing uninitialized left-value: assert \initialized(&tmp); stack: SHA256_Transform :: sha2.c:470 <- SHA256_Update :: hmac.c:107 <- hmac_sha256_update :: hmac.c:132 <- hmac_sha256 :: auth.c:50 <- checkHmac :: auth.c:90 <- auth :: frama-driver.c:37 <- main auth.c:32:[kernel] warning: accessing uninitialized left-value: assert \initialized(x); stack: memcmp_ct :: auth.c:51 <- checkHmac :: auth.c:90 <- auth :: frama-driver.c:37 <- main auth.c:93:[value] Assertion got status unknown. auth.c:10:[value] Function getWord64: precondition got status valid. stack: getWord64 :: auth.c:94 <- auth :: frama-driver.c:37 <- main [value] using specification for function Frama_C_nondet FRAMAC_SHARE/libc/stdio.h:106:[value] Function fopen: postcondition got status unknown. stack: fopen :: seq.c:27 <- getSeq :: seq.c:56 <- checkSeq :: auth.c:95 <- auth :: frama-driver.c:37 <- main auth.c:68:[value] Function auth: postcondition got status valid. stack: auth :: frama-driver.c:37 <- main frama-driver.c:38:[value] Assertion got status valid. [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values at end of function SHA256_Transform: ctx{.ctx_inside; .ctx_outside.state[0..7]} â [--..--] .ctx_outside.bitcount â {0; 512; 281474976710656; 844424930131968} {.ctx_outside.buffer[0..63]; .block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] data â {{ (sha2_word32 const *)&buf{[96], [160], [224]} ; &ctx + {104; 208; 272; 336} }} a â {0} b â {0} c â {0} d â {0} e â {0} f â {0} g â {0} h â {0} s0 â [--..--] s1 â [--..--] T1 â {0} T2 â {0} W256 â {{ (sha2_word32 *)&ctx{.ctx_inside.buffer, .ctx_outside.buffer} }} j â {64} [value] Values at end of function coinflip: Frama_C_entropy_source â [--..--] [value] Values at end of function fopen: Frama_C_entropy_source â [--..--] __retres â {{ NULL ; &S___fc_stdin[0] }} [value] Values at end of function getBit: idx â {0; 1; 2; 3; 4} bnum â {0; 1; 2; 3; 4; 5; 6; 7} byte â [--..--] __retres â {0; 1} [value] Values at end of function getSeq: Frama_C_entropy_source â [--..--] fp â {0} ret â {0} [value] Values at end of function checkSeq: Frama_C_entropy_source â [--..--] targ â {0} [value] Values at end of function getWord64: __retres â [--..--] [value] Values at end of function memcmp_ct: x â {{ &buf[32] }} y â {{ &hmac[32] }} sz â {4294967295} r â [0..255] [value] Values at end of function SHA256_Update: ctx.ctx_inside.state[0..7] â [--..--] .ctx_inside.bitcount â [0..2304],0%8 .ctx_inside.buffer[0..62] â [--..--] or UNINITIALIZED {.ctx_inside.buffer[63]; .ctx_outside.state[0..7]} â [--..--] .ctx_outside.bitcount â {0; 256; 512; 768} {.ctx_outside.buffer[0..63]; .block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] data â {{ &buf{[32], [96], [160], [224]} ; &digest_inside[0] ; &ctx + {272; 336} }} len â [0..63] freespace â {0} usedspace â {0} [value] Values at end of function hmac_sha256_update: ctx.ctx_inside.state[0..7] â [--..--] .ctx_inside.bitcount â [576..2304],0%8 .ctx_inside.buffer[0..62] â [--..--] or UNINITIALIZED {.ctx_inside.buffer[63]; .ctx_outside.state[0..7]} â [--..--] .ctx_outside.bitcount â {512} {.ctx_outside.buffer[0..63]; .block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function SHA256_Final: hmac[0..31] â [--..--] or UNINITIALIZED digest_inside[0..31] â [--..--] ctx.ctx_inside â {0} .ctx_outside.state[0..7] â [--..--] .ctx_outside.bitcount â {0; 512} {.ctx_outside.buffer[0..63]; .block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] d â {{ (sha2_word32 *)&hmac[32] ; (sha2_word32 *)&digest_inside[32] }} usedspace â {0} [value] Values at end of function SHA256_Init: ctx.ctx_inside.state[0..7] â [--..--] .ctx_inside.bitcount â {0; 512} .ctx_inside.buffer[0..63] â [--..--] .ctx_outside.state[0] â {0; 1779033703} .ctx_outside.state[1] â {0; 3144134277} .ctx_outside.state[2] â {0; 1013904242} .ctx_outside.state[3] â {0; 2773480762} .ctx_outside.state[4] â {0; 1359893119} .ctx_outside.state[5] â {0; 2600822924} .ctx_outside.state[6] â {0; 528734635} .ctx_outside.state[7] â {0; 1541459225} .ctx_outside{.bitcount; .buffer[0..63]} â {0} {.block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function hmac_sha256_final: hmac[0..31] â [--..--] digest_inside[0..31] â [--..--] ctx{.ctx_inside; .ctx_outside} â {0} {.block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function pad_init: i â {64} ctx{.ctx_inside; .ctx_outside} â {0} {.block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function hmac_sha256_init: final_key[0..63] â [--..--] init_key[0..63] â [--..--] final_len â [0..64] ctx.ctx_inside.state[0..7] â [--..--] .ctx_inside.bitcount â {512} {.ctx_inside.buffer[0..63]; .ctx_outside.state[0..7]} â [--..--] .ctx_outside.bitcount â {512} {.ctx_outside.buffer[0..63]; .block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function hmac_sha256: hmac[0..31] â [--..--] ctx{.ctx_inside; .ctx_outside} â {0} {.block_inner_pad[0..63]; .block_outer_pad[0..63]} â [--..--] [value] Values at end of function checkHmac: hmac[0..31] â [--..--] __retres â {0; 1} [value] Values at end of function proofOfWork: i â [0..40] __retres â {0; 1} [value] Values at end of function auth: Frama_C_entropy_source â [--..--] seq â [--..--] or UNINITIALIZED __retres â {0} [value] Values at end of function main: Frama_C_entropy_source â [--..--] kbuf[0..63] â [--..--] or UNINITIALIZED buf[0..255] â [--..--] or UNINITIALIZED pay â {0} sz â [0..256] ksz â [0..64] paysz â {0} i â [0..64] work â [0..40] ok â {0} __retres â {0}