Advanced Debugging
Memory Analysis
The memory analysis makes sure that memory access is safe. That is, the allocation of objects and the update of the free memory pointer are done correctly, and pointers are consistent.
In Results.txt
one can find indications of whether the points-to analysis (a major component of the memory analysis) fails or not, e.g., Pointer analysis failed while analyzing
as in the full message, also indicating the source location:
[main] WARN POINTS_TO - Pointer analysis failed while analyzing simplifiedVaultHarness-batchSwap @ LTACCmd(ptr=CmdPointer(block=24991_998_0_0_0_0_0_0, pos=2), cmd=ByteStore R38900:bv256 R39227:bv256 tacM:bytemap (5059:58:5:0xce4604a0000000000000000000000004) // .certora_config/simplifiedVaultHarness.sol_4/5_SignaturesValidator.sol)