Frama-C Bug Tracking System - Frama-C
View Issue Details
0002392Frama-CDocumentation > ACSLpublic2018-07-25 15:002018-07-25 15:40
jens 
virgile 
normalminoralways
closedsuspended 
Frama-C 17-Chlorine 
 
0002392: request of clarification about using the address of a formal argument
In 0002390 the issue was raised whether functions contracts such as

/*@ requires
    \valid(&a);
    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.
The 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.
No tags attached.
Issue History
2018-07-25 15:00jensNew Issue
2018-07-25 15:00jensStatusnew => assigned
2018-07-25 15:00jensAssigned To => patrick
2018-07-25 15:39virgileNote Added: 0006616
2018-07-25 15:39virgileStatusassigned => closed
2018-07-25 15:39virgileAssigned Topatrick => virgile
2018-07-25 15:39virgileResolutionopen => suspended
2018-07-25 15:40virgileNote Added: 0006617

Notes
(0006616)
virgile   
2018-07-25 15:39   
This issue is about ACSL semantics and has been ported on ACSL's github repository at https://github.com/acsl-language/acsl/issues/49 [^]
(0006617)
virgile   
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.