Jessie crashes on \old(*ptr)
ID0000427: This issue was created automatically from Mantis Issue 427. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000427 | Frama-C | Plug-in > jessie | public | 2010-03-13 | 2010-12-18 |
| Reporter | clandcx | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090901 | Target Version | - | Fixed in Version | Frama-C Carbon-20101202-beta2 |
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