Incorrect procedure summary

[l-kent]

In ProcedureSummaryTests, the test procedure_summary3 currently produces incorrect summaries.

For the procedure f it produces

ensures gamma_load32(Gamma_mem, $x_addr);
ensures Gamma_R1;
ensures Gamma_R0;

R1 and R0 should not be low here, they are dependent on the input security level of R0.

This may be related to the lack of correct handling of non-returning calls in BASIL more broadly - the test case verifying despite the summaries being incorrect is definitely due to this.