request of clarification about using the address of a formal argument
ID0002392: This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002392 | Frama-C | Documentation > ACSL | public | 2018-07-25 | 2018-07-25 |
| Reporter | jens | Assigned To | virgile | Resolution | suspended |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 17-Chlorine | Target Version | - | Fixed in Version | - |
Description :
In #2390 (closed) 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.
Additional Information :
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.