Verify preconditions when calling functions

xr0-org / xr0

The Xr0 Verifier for C

https://xr0.dev

Apache License 2.0

173 stars 4 forks source link

Verify preconditions when calling functions #29

Closed claude-betz closed 5 months ago

claude-betz commented 6 months ago

When calling a function transitively (from the body of a function under verification) we are currently not checking whether the preconditions specified in that function's abstract are met by the parameters that are passed into it.

claude-betz commented 5 months ago

was implemented naively but refined in #32