Currently, the presence of a Hermes annotation implies that the annotated function will return without diverging, and all ensures clauses provide conditions which hold given that the function doesn't diverge. However, users may want to annotate functions which diverge under some conditions (e.g. Option::unwrap) or even all conditions (e.g. panic!). We'll need a syntax that allows distinguishing the common case, where an ensures clause is implicitly prefixed with "this function returns and...", and the more general case where the user can write "raw" conditions which also specify the conditions under which a function diverges.
Currently, the presence of a Hermes annotation implies that the annotated function will return without diverging, and all
ensuresclauses provide conditions which hold given that the function doesn't diverge. However, users may want to annotate functions which diverge under some conditions (e.g.Option::unwrap) or even all conditions (e.g.panic!). We'll need a syntax that allows distinguishing the common case, where anensuresclause is implicitly prefixed with "this function returns and...", and the more general case where the user can write "raw" conditions which also specify the conditions under which a function diverges.