tests/syntax/asm_with_contracts.i · f7d8e1c68421061b5f551818d6b826cf8caea5e4 · pub / frama-c

5 years ago

[kernel] avoid generating ill-formed asm contracts in presence of void ptrs · df86ea52

When a `void *` lval is referenced in an asm directive, use its conversion
as `char *` in the contract to obtain well-formed `assigns` clauses.

Fixes #609

df86ea52

History

[kernel] avoid generating ill-formed asm contracts in presence of void ptrs

Virgile Prevosto authored 5 years ago

When a `void *` lval is referenced in an asm directive, use its conversion
as `char *` in the contract to obtain well-formed `assigns` clauses.

Fixes #609

asm_with_contracts.i 607 B