search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Scope of invariant #4

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

Do invariant hold for functions defined before them, as in

typedef struct S { int x; } S;

void reset(S *p) { p->x = 0; }

//@ type invariant I(S *p) { p.x > 0 }
davidcok commented 6 years ago

I would expect so - at least for type invariants. Otherwise when writing the type invariant the field names have not yet been declared -- so it gets messy.