field_compatible0_Tarray_offset does not need naturally_aligned

PrincetonUniversity / VST

Verified Software Toolchain

https://vst.cs.princeton.edu

Other

425 stars 91 forks source link

field_compatible0_Tarray_offset does not need naturally_aligned #710

Closed andrew-appel closed 10 months ago

andrew-appel commented 10 months ago

The lemma field_compatible0_Tarray_offset in floyd/field_compat.v does not need the naturally_aligned premise. Stating this premise is harmful when used on arrays of int_or_ptr_type. The premise should be deleted.

andrew-appel commented 10 months ago

Same as #700