search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

Improve VSU diagnostics related to missing (vacuous) funspecs #682

Closed andrew-appel closed 1 year ago

andrew-appel commented 1 year ago

When a function definition is in the .c file, but no funspec is in the ASI, now the mkVSU tactic will automatically insert a vacuous funspec.