There are certain attributes in the AST right now that do not exist in the grammar and cannot survive a round trip (they get printed, but will then fail to parse). This only comes up when the attributes are added from code, so it's hard to produce an example, however the memory encoding currently does generate such an example as of #161 inserting boogie attributes into ApplyFun expressions. This gets added to free but does not parse:
requires ($me_addr_is_heap) { .boogie = { .msg = "\"Memory Error: Invalid Free\"" } } ($mem_encoding, R0_in:bv64)
It seems like all of the expression variants have unused attribtues: ApplyFun, Binary, Lambda, Unary, Let and ApplyIntrin. Most declarations are fine but variable declaration also have this issue.
There are certain attributes in the AST right now that do not exist in the grammar and cannot survive a round trip (they get printed, but will then fail to parse). This only comes up when the attributes are added from code, so it's hard to produce an example, however the memory encoding currently does generate such an example as of #161 inserting boogie attributes into
ApplyFunexpressions. This gets added to free but does not parse:It seems like all of the expression variants have unused attribtues:
ApplyFun,Binary,Lambda,Unary,LetandApplyIntrin. Most declarations are fine but variable declaration also have this issue.