[CN] Add parsing of a->b expressions in CN assertions

[septract]

Work on addressing #328

This works by modifying parsers/c/c_parser.mly to desugar a->b expressions to (*a).b

I also added a testcase demonstrating the new syntax.

[septract]

cc @dc-mak

[cp526]

That looks good. Though ideally we'd delay the desugaring until after parsing, so we have the parse AST record exactly what the user wrote (and be able to give better error messages).

That would involve a bit more work:

• adding an AST node for the arrow notation to frontend/model/cn.lem
• changing c_parser.mly to output that AST node instead of immediately desugaring
• extending cabs_to_ail.lem (which does symbol resolution) for the new AST node, just following the way that code works for other similar constructs
• making compile.ml (which translates parse AST to internal ast) do the desugaring

Which sounds like a lot but, I suspect, is on the order of 30 lines of code.

[septract]

@cp526 I pushed desugaring later down the pipeline. Does this look good?

I accidentally merged main to my branch so you should squash before merging.

[cp526]

Looks good!