search

acsl-language / acsl

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

Type invariant and local variable #5

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

Does a local variable from a caller function still satisfy its invariant when the callee returns?

vprevosto commented 7 years ago

The only way for the callee to modify it would be if it is passed through a pointer, and the manual explicitely says that nothing is guaranteed for memory locations accessed through a pointer.