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] 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}