Frama-C Bug Tracking System - Frama-C
View Issue Details
0000427Frama-CPlug-in > jessiepublic2010-03-13 08:202010-12-18 11:19
clandcx 
cmarche 
normalcrashalways
closedfixed 
Frama-C Beryllium-20090901 
Frama-C Carbon-20101202-beta2 
0000427: Jessie crashes on \old(*ptr)
$ 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 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; }
Attached is the stack.jessie directory. MD5 (stack.jessie.tar.gz) = d4a27838551febf2252b712e308e7ca6
No tags attached.
gz stack.jessie.tar.gz (60,996) 2010-03-13 08:20
https://bts.frama-c.com/file_download.php?file_id=68&type=bug
Issue History
2010-03-13 08:20clandcxNew Issue
2010-03-13 08:20clandcxStatusnew => assigned
2010-03-13 08:20clandcxAssigned To => cmarche
2010-03-13 08:20clandcxFile Added: stack.jessie.tar.gz
2010-03-16 15:38cmarcheNote Added: 0000730
2010-12-16 17:35cmarcheNote Added: 0001322
2010-12-16 17:35cmarcheStatusassigned => resolved
2010-12-16 17:35cmarcheResolutionopen => fixed
2010-12-18 11:18signolesFixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19signolesStatusresolved => closed

Notes
(0000730)
cmarche   
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   
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.