search

UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

Incorrect procedure summary #235

Open l-kent opened 3 weeks ago

l-kent commented 3 weeks ago

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.