--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2009 ---
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.