0000568: cast to const type not handled in acsl annotations - 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

0000568

Frama-C

Kernel > ACSL implementation

public

2010-08-23 14:53

2014-02-12 16:55

Reporter

derepas

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Boron-20100401

Target Version

Fixed in Version

Frama-C Carbon-20101201-beta1

Summary

0000568: cast to const type not handled in acsl annotations

Description

Let us consider the following file "ex.c" :
1 : int main() {
2 : const char * p1="foo1";
3 : //@ assert (\valid_index( (const char * ) p1,0));
4 : return 0;
5 : }
Then the command line "frama-c ex.c" yields the following error :
ex.c:3:[kernel] user error: syntax error while parsing annotation

This is the same for the following types : (char const *) or (char * const).

Tags

No tags attached.

Relationships

Notes
(0001101) virgile (developer) 2010-08-25 14:39	const is now recognized in casts in ACSL. Since the logic do not contain mutable values, T and const T are considered equivalent though.

Issue History
Date Modified	Username	Field	Change
2010-08-23 14:53	derepas	New Issue
2010-08-23 14:53	derepas	Status	new => assigned
2010-08-23 14:53	derepas	Assigned To	=> virgile
2010-08-24 21:22	svn	Checkin
2010-08-25 14:39	virgile	Note Added: 0001101
2010-08-25 14:39	virgile	Status	assigned => resolved
2010-08-25 14:39	virgile	Resolution	open => fixed
2010-12-10 15:45	signoles	Fixed in Version	=> Frama-C Carbon-20101201-beta1
2010-12-17 19:35	signoles	Status	resolved => closed

Copyright © 2000 - 2019 MantisBT Team