Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2277

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

Attachments

  • stack.jessie.tar.gz
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking