0002126: WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002126

Frama-C

Plug-in > wp

public

2015-06-02 08:52

2016-01-26 08:43

Reporter

virgile

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Magnesium

Summary

0002126: WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)

Description

On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed

Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).

-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);

/*@
  assigns \nothing;
*/
void fn2(void) {
  char pcr_index;
  fn1(&pcr_index);
}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0005951) correnson (manager) 2015-06-29 16:42	Proved by Qed.

Issue History
Date Modified	Username	Field	Change
2015-06-02 08:52	virgile	New Issue
2015-06-02 08:52	virgile	Status	new => assigned
2015-06-02 08:52	virgile	Assigned To	=> correnson
2015-06-02 08:53	virgile	Relationship added	has duplicate 0002124
2015-06-29 16:42	correnson	Note Added: 0005951
2015-06-29 16:42	correnson	Status	assigned => resolved
2015-06-29 16:42	correnson	Fixed in Version	=> Frama-C Magnesium
2015-06-29 16:42	correnson	Resolution	open => fixed
2016-01-26 08:43	signoles	Status	resolved => closed