JML translation are not correctly handled by Final Fields support

[wadoon]

Description

In constructors, the access to final fields should happen via Heap.

But instead, it uses the new final function.

Please describe your concern in detail!

Example Java

public class A  {
    public final Object o;

    /*@ ensures true; requires true; */
    public A() {
        o = new Object();
        //@ assert o != null;
    }
}

Reproducible

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Load A.java.
2. Run auto
3. Inspect the translation of JMLAssertStatement w/o pretty-printing.

What is your expected behavior and what was the actual behavior?

Object::final(self, A::#o) becomes Object::select(heap, self, A::#o).

• Commit: Current main.