0000342: Assertion failed instead of typing error report - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000342

Frama-C

Kernel > ACSL implementation

public

2009-11-23 15:38

2014-02-12 16:55

Reporter

nrousset

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Beryllium-20090902

Target Version

Fixed in Version

Frama-C Boron-20100401

Summary

0000342: Assertion failed instead of typing error report

Description

In the example below, I forgot the parentheses in the expression
(&x[i])->i1 in annotations:

----------------------------------------
typedef struct { int i1; int i2; } s;

/*@ requires
  @ \valid(x + i) && &x[i]->i1 != 0;
  @*/
int f (s x[], int i) {
  return 1 / (&x[i])->i1;
}
-----------------------------------------

It crashes with
assertion failed in cil/src/cil.ml line 2044
instead of reporting a typing error.

Tags

No tags attached.

Relationships

Notes
(0000573) monate (reporter) 2009-11-23 19:11	Thanks for the report. The error will be in the next release: tests/cil/bts342.c:6:[kernel] user error: Error during annotations analysis: type s is not a pointer type [kernel] user error: skipping file "tests/cil/bts342.c" that has errors. [kernel] Plugin kernel aborted because of invalid user input(s).

Issue History
Date Modified	Username	Field	Change
2009-11-23 15:38	nrousset	New Issue
2009-11-23 17:57	signoles	Status	new => assigned
2009-11-23 17:57	signoles	Assigned To	=> virgile
2009-11-23 19:09	svn	Checkin
2009-11-23 19:09	svn	Status	assigned => resolved
2009-11-23 19:09	svn	Resolution	open => fixed
2009-11-23 19:11	monate	Note Added: 0000573
2010-02-05 09:45	signoles	Category	Kernel => Kernel > ACSL implementation
2010-04-13 15:30	signoles	Status	resolved => new
2010-04-13 15:31	signoles	Status	new => closed
2010-04-13 15:33	signoles	Fixed in Version	=> Frama-C Boron

Copyright © 2000 - 2019 MantisBT Team