0000427: Jessie crashes on \old(*ptr) - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000427

Frama-C

Plug-in > jessie

public

2010-03-13 08:20

2010-12-18 11:19

Reporter

clandcx

Assigned To

cmarche

Priority

normal

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090901

Target Version

Fixed in Version

Frama-C Carbon-20101202-beta2

Summary

0000427: Jessie crashes on \old(*ptr)

Description

$ frama-c --version
Version: Beryllium-20090902

$ uname -a
FreeBSD viper.internal.network 8.0-RELEASE-p2
  FreeBSD 8.0-RELEASE-p2 #0: Tue Jan 5 21:11:58 UTC 2010
    root@amd64-builder.daemonology.net:/usr/obj/usr/src/sys/GENERIC amd64

Jessie crashes with the following (probably invalid) set of annotations.
Specifically, the problem line is:

  @ ensures !stack_full (\old (*stack)) ==> \old(stack->used) < stack->used;

$ frama-c -jessie stack.c
[kernel] preprocessing with "gcc -C -E -I. -dD stack.c"
[jessie] Starting Jessie translation
stack.c:57:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "norm.ml:494:27").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com [^]

stack.c:

#include <stddef.h>

typedef struct stack_t {
  int *data;
  unsigned long size;
  unsigned long used;
} stack_t;

void stack_init (stack_t *, int *, unsigned long);
int stack_valid (const stack_t *stack);
int stack_push (stack_t *, int);
int stack_pop (stack_t *, int *);

/*@ predicate stack_initialized (stack_t s) =
  @ (0 < s.size) && \valid (s.data) && \valid_range (s.data, 0, s.size);
  @
  @ predicate stack_full (stack_t s) =
  @ stack_initialized (s) && (s.used == s.size);
  @
  @ predicate stack_empty (stack_t s) =
  @ stack_initialized (s) && (s.used == 0);
  @ */

/*@ requires \valid (stack);
  @ ensures 0 <= \result <= 1;
  @ ensures stack_initialized (*stack) ==> \result == 1;
  @ */

int
stack_valid (const stack_t *stack)
{
  return ((stack->data != NULL) && (stack->size != 0));
}

/*@ requires \valid (stack);
  @ requires \valid (data);
  @ requires \valid_range (data, 0, size);
  @ requires 0 < size;
  @ ensures stack_initialized (*stack);
  @ ensures stack->used == 0;
  @ */

void
stack_init (stack_t *stack, int *data, unsigned long size)
{
  stack->data = data;
  stack->size = size;
  stack->used = 0;
}

/*@ requires \valid (stack);
  @ requires stack_initialized (*stack);
  @ ensures !stack_full (\old (*stack)) ==> \old(stack->used) < stack->used;
  @ */

int
stack_push (stack_t *stack, int item)
{
  if (stack->used < stack->size) {
    stack->used++;
    stack->data [stack->used] = item;
    return 1;
  } else
    return 0;
}

/*@ requires \valid (stack);
  @ requires stack_initialized (*stack);
  @ requires \valid (item); */

int
stack_pop (stack_t *stack, int *item)
{
  if (stack->used > 0) {
    *item = stack->data [stack->used];
    stack->used--;
    return 1;
  } else
    return 0;
}

Additional Information

Attached is the stack.jessie directory.

MD5 (stack.jessie.tar.gz) = d4a27838551febf2252b712e308e7ca6

Tags

No tags attached.

Attached Files

stack.jessie.tar.gz [^] (60,996 bytes) 2010-03-13 08:20

Relationships

Notes
(0000730) cmarche (developer) 2010-03-16 15:38	The workaround is to use hybrid predicates taking pointers as argument: predicate stack_initialized (stack_t *s) = (0 < s->size) && \valid (s->data) && \valid_range (s->data, 0, s->size); and so on

(0001322) cmarche (developer) 2010-12-16 17:35	using struct as parameters to logic symbols is disallowed in jessie now. If you change parameters (stack_t s) into (stack *s) and change to function calls accrodingly, then everything works fine.

Issue History
Date Modified	Username	Field	Change
2010-03-13 08:20	clandcx	New Issue
2010-03-13 08:20	clandcx	Status	new => assigned
2010-03-13 08:20	clandcx	Assigned To	=> cmarche
2010-03-13 08:20	clandcx	File Added: stack.jessie.tar.gz
2010-03-16 15:38	cmarche	Note Added: 0000730
2010-12-16 17:35	cmarche	Note Added: 0001322
2010-12-16 17:35	cmarche	Status	assigned => resolved
2010-12-16 17:35	cmarche	Resolution	open => fixed
2010-12-18 11:18	signoles	Fixed in Version	=> Frama-C Carbon-20101202-beta2
2010-12-18 11:19	signoles	Status	resolved => closed