CBMC: Add prove and spec for adrs_set_hash_address

[h2parson]

Resolves issue #30

[h2parson]

Not sure if the VALID_SLH_VAR_T macro is complete. Should adrs->u32 be memory no aliased?

[mkannwischer]

Not sure if the VALID_SLH_VAR_T macro is complete. Should adrs->u32 be memory no aliased?

It is certainly not complete, but that is okay. We can extend it when another proof requires it.
No, you don't need another memory_no_alias for u32 as it's statically allocated - it's included in adrs.

[mkannwischer]

The changes do look good to me, but the proofs time out.
Does this proof pass for you locally?

[h2parson]

The changes do look good to me, but the proofs time out. Does this proof pass for you locally?

Hi Matthias, sorry for the delay. This should be fixed now.

[mkannwischer]

Thanks @h2parson. The changes LGTM. Can you please clean up the commit history (i.e., squash into one commit and make sure that it accurately reflects your changes).

[h2parson]

It's squashed now.