What is the semantics of a string literal in an ACSL annotation?
Proposal: it is equivalent to declare a new ghost variable: assert P("foo") would then become assert P(ghost_foo);, with a global declaration /*@ ghost const char ghost_foo[4] = "foo"; */ inserted before.
What is the semantics of a string literal in an ACSL annotation?
Proposal: it is equivalent to declare a new ghost variable:
assert P("foo")would then becomeassert P(ghost_foo);, with a global declaration/*@ ghost const char ghost_foo[4] = "foo"; */inserted before.