Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002392Frama-CDocumentation > ACSLpublic2018-07-25 15:002018-07-25 15:40
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002392: request of clarification about using the address of a formal argument
DescriptionIn 0002390 the issue was raised whether functions contracts such as

/*@ requires
    ensures \false; */
void f(int a) {
  return ;

are meaningful.
More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition is illegal.
(When I see that WP uses such a precondition to verify \false, them I am all in for disallowing it.)

Of course, it would also be nice if Frama-C (the kernel?) would issue a diagnostics.
Additional InformationThe question also came up about using the address of a formal argument in a postcondition.
For the time being, I don't see it as a meaningful feature.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
virgile (developer)
2018-07-25 15:39

This issue is about ACSL semantics and has been ported on ACSL's github repository at [^]
virgile (developer)
2018-07-25 15:40

@jens, sorry if I wasn't clear, but I meant opening an issue on ACSL's new home on github, not here.

- Issue History
Date Modified Username Field Change
2018-07-25 15:00 jens New Issue
2018-07-25 15:00 jens Status new => assigned
2018-07-25 15:00 jens Assigned To => patrick
2018-07-25 15:39 virgile Note Added: 0006616
2018-07-25 15:39 virgile Status assigned => closed
2018-07-25 15:39 virgile Assigned To patrick => virgile
2018-07-25 15:39 virgile Resolution open => suspended
2018-07-25 15:40 virgile Note Added: 0006617

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker