0001647: compatibility between \null in ACSL and NULL in C in wp

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

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001647

Frama-C

Plug-in > wp

public

2014-02-17 15:58

2015-03-17 22:17

Reporter

Anne

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Sodium

Summary

0001647: compatibility between \null in ACSL and NULL in C in wp

Description

I have tried to prove properties involving NULL pointers, and I had problem to write the ACSL part. Here is and example:
/*@
    ensures e1: \result == \null;
    ensures e2: \result == 0;
    ensures e3: \result == (int *) \null;
    ensures e4: \result == (int *) 0;
    ensures e5: \result == (int *)((void *)0);
*/
int * f (void) {
  return NULL;
}

None of the properties are proved with the default memory model.
I finally manage to prove them with: -wp-model Typed+cast

Since NULL is used very often in programs, even with a clean typing, maybe something could be done for this special case ? Just a suggestion... ;-)

Tags

No tags attached.

Attached Files

Relationships

Notes
(0005177) correnson (manager) 2014-06-02 13:58	Fix committed to master branch.

Issue History
Date Modified	Username	Field	Change
2014-02-17 15:58	Anne	New Issue
2014-02-17 15:58	Anne	Status	new => assigned
2014-02-17 15:58	Anne	Assigned To	=> correnson
2014-06-02 13:58	correnson	Note Added: 0005177
2014-06-02 13:58	correnson	Status	assigned => resolved
2014-06-02 13:58	correnson	Resolution	open => fixed
2015-03-17 22:17	signoles	Fixed in Version	=> Frama-C Sodium
2015-03-17 22:17	signoles	Status	resolved => closed