View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | 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 | ||||||
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 |
|
![]() |
|
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 |
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. |
![]() |
|||
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 |