UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

Procedure summaries involving global variables when memory is not accessed #236

Open l-kent opened 3 weeks ago

l-kent commented 3 weeks ago

The procedure summarisation currently in some cases produces summaries relating to global variables even when a procedure does not access memory at all. An example of this is the procedure_summary test in ProcedureSummaryTests, which generates summaries for the global variables x and y for the procedure get_two, even though that procedure doesn't access memory at all. These summaries are redundant.

According to @b-paul this is because global variables are initially marked as tainting themselves in a procedure, even if memory is never accessed, leading to them erroneously being used in the procedure summary. It should be checked whether memory is accessed at all (or the relevant memory region for a global variable, once that is added), before generating summaries for global variables.