--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] my first frama verification



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}