Frama-C/Codex Analysis results

/* Generated by Frama-C */
struct message {
   struct message *next ;
   char *buffer ;
};
struct message_box {
   int length ;
   struct message *first ;
};
void zeros_buffer(struct message_box *box)
{
  struct message *first = box->first;
  struct message *current = first;
  int length = box->length;
  while (1) {
    {
      int i = 0;
      while (i < length) {
        *(current->buffer + i) = (char)0;
        i ++;
      }
    }
    current = current->next;
    if (! (current != first)) break;
  }
  return;
}

Unproved alarms:

example.c:12: Memory_access(box->first,
read) {true;false}

example.c:19: Memory_access(current->buffer,
read) {true;false}

example.c:19: Memory_access(*(current->buffer + i),
write) {true;false}

example.c:21: Memory_access(current->next,
read) {true;false}

Proved 1/5 alarms

/	Name	Type	Value
Expr	box->first	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	box->first	struct message *
Expr	box	struct message_box *	{0} or ([1..0xFFFFFFFF] : struct message_box*)
Lval	box	struct message_box *
Expr	first	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	first	struct message *
Expr	box->length	int	[--..--]
Lval	box->length	int
Expr	box	struct message_box *	([1..0xFFFFFFFB] : struct message_box*)
Lval	box	struct message_box *
Expr	0	int	{0x0}
Expr	i < length	int	{0; 1}
Expr	i	int	[0..0x7FFFFFFF]
Lval	i	int
Expr	length	int	[--..--]
Lval	length	int
Lval	*(current->buffer + i)	char
Expr	current->buffer + i	char *	[0..0x7FFFFFFE] or ([1..0xFFFFFFFF] : buffer[{0}].[0..0x7FFFFFFE]*)
Expr	current->buffer	char *	{0} or ([1..0xFFFFFFFF] : buffer*)
Lval	current->buffer	char *
Expr	current	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	current	struct message *
Expr	i	int	[0..0x7FFFFFFE]
Lval	i	int
Expr	(char)0	char	{0}
Expr	0	int	{0x0}
Lval	i	int
Lval	current	struct message *
Expr	current->next	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	current->next	struct message *
Expr	current	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	current	struct message *
Expr	! (current != first)	int
Expr	current != first	int	{0; 1}
Expr	current	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	current	struct message *
Expr	first	struct message *	{0} or ([1..0xFFFFFFFF] : struct message*)
Lval	first	struct message *
Func	zeros_buffer	Name(function zeros_buffer)