2021-03-01 05:56 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000427Frama-CPlug-in > jessiepublic2010-03-13 08:202010-12-18 11:19
Reporterclandcx 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000427: 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 InformationAttached is the stack.jessie directory.

MD5 (stack.jessie.tar.gz) = d4a27838551febf2252b712e308e7ca6
TagsNo tags attached.
Attached Files

-Relationships
+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.
+Notes

-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
+Issue History