--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject



taken into account. The file
"dev-random-pass-gen.jessie/dev-random-pass-gen.jc" contains:

int32 read(int32 fd, char_P[..] buf, uint32 count)
  requires (C_6 : (fd >=3D 0));
  requires (C_7 : (count > 0));
  requires (C_8 : ((C_9 : (\offset_min(buf) <=3D 0)) &&
                    (C_10 : (\offset_max(buf) >=3D (count - 1)))));
behavior default:
  assumes true;
  assigns \nothing;
  ensures (C_11 : true);
behavior error:
  assumes true;
  assigns global_error_number;
  ensures (C_12 : (\result < 0));
behavior end_of_file:
  assumes true;
  assigns \nothing;
  ensures (C_13 : (\result =3D=3D 0));
behavior normal:
  assumes true;
  assigns (buf + [0..(count - 1)]).char_M;
  ensures (C_14 : (((C_16 : ((buf + 0).char_M >=3D 0)) &&
                     (C_17 : ((buf + 0).char_M < 256))) &&
                    (C_18 : (\result > 0))));
;

And within the file
"dev-random-pass-gen.jessie/why/dev-random-pass-gen.why", I find:

parameter read :
 fd:int32 ->
  buf:char_P pointer ->
   count:uint32 ->
    char_P_char_M_buf_23:(char_P, int8) memory ref ->
     char_P_buf_23_alloc_table:char_P alloc_table ->
      { } int32
      reads char_P___string_open_1_alloc_table,char_P___string_read_2_alloc=
_table,char_P_char_M___string_open_1,char_P_char_M___string_read_2,char_P_c=
har_M_buf_23
      writes char_P_char_M_buf_23,global_error_number
      { ((JC_204:
         ((JC_200:
          valid___string_open(char_P___string_open_1_alloc_table,
          char_P_char_M___string_open_1))
         and ((JC_201:
              valid___string_open_0(char_P___string_open_1_alloc_table))
             and ((JC_202:
                  valid___string_read(char_P___string_read_2_alloc_table,
                  char_P_char_M___string_read_2))
                 and (JC_203:

valid___string_read_0(char_P___string_read_2_alloc_table))))))
        and (((true =3D true) ->
              (JC_262:
              ((JC_259:
               ((JC_254:
                ((JC_251:
                 ge_int(integer_of_int8(select(char_P_char_M_buf_23,
                                        shift(buf, (0)))),
                 (0)))
                and ((JC_252:
                     lt_int(integer_of_int8(select(char_P_char_M_buf_23,
                                            shift(buf, (0)))),
                     (256)))
                    and (JC_253: gt_int(integer_of_int32(result), (0))))))
               and ((JC_255:
                    valid___string_open(char_P___string_open_1_alloc_table,
[...]

and

parameter read_requires :
 fd:int32 ->
  buf:char_P pointer ->
   count:uint32 ->
    char_P_char_M_buf_23:(char_P, int8) memory ref ->
     char_P_buf_23_alloc_table:char_P alloc_table ->
      { (JC_177:
        (((JC_169: ge_int(integer_of_int32(fd), (0)))
         and ((JC_170: gt_int(integer_of_uint32(count), (0)))
             and ((JC_171:
                  le_int(offset_min(char_P_buf_23_alloc_table, buf), (0)))
                 and (JC_172:
                     ge_int(offset_max(char_P_buf_23_alloc_table, buf),
                     sub_int(integer_of_uint32(count), (1)))))))
        and ((JC_173:
             valid___string_open(char_P___string_open_1_alloc_table,
             char_P_char_M___string_open_1))
            and ((JC_174:
                 valid___string_open_0(char_P___string_open_1_alloc_table))
                and ((JC_175:
                     valid___string_read(char_P___string_read_2_alloc_table=
,
                     char_P_char_M___string_read_2))
                    and (JC_176:

valid___string_read_0(char_P___string_read_2_alloc_table)))))))}
      int32
      reads char_P___string_open_1_alloc_table,char_P___string_read_2_alloc=
_table,char_P_char_M___string_open_1,char_P_char_M___string_read_2,char_P_c=
har_M_buf_23
      writes char_P_char_M_buf_23,global_error_number
      { ((JC_204:
         ((JC_200:
          valid___string_open(char_P___string_open_1_alloc_table,
          char_P_char_M___string_open_1))
         and ((JC_201:
[...]


So I would say the message "No code for function read, default assigns
generated" is spurious or erroneous.

Yours,
d.