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

View Issue Details [ Jump to Notes ]

[ 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

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

Relationships

Notes

~0005177

correnson (manager)

2014-06-02 13:58

Fix committed to master branch.

Notes

Date Modified	Username	Field	Change
Issue History
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	Source_changeset_attached	=> framac master 300363a6
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

Issue History