Once Linux kernel indexing is done, you can now run the analysis scripts.
(1) Open the Atlas Shell to Invoke L-SAP
To open the Atlas Shell, from the menu toolbar, go to Window > Show View > Other... and look for Atlas Shell under Atlas category. You may have the Eclipse setup as follows:
(2) Analysis Scripts
All the analysis scripts reside in class LinuxScripts.java. Before invoking the analysis scripts, you need to set the following flags/strings in code to your preferences:
SHOW_GRAPHS field: if it is set to true, the script will produce the CFGs, MPGs, and EFGs for each signature in the lock/unlock pairing analysis.
WORKSPACE_PATH field: to determine the path where the analysis results will be written.
If you want to invoke the spin/mutex lock/unlock pairing analysis, then write into the Atlas Shell the respective commands:
var x = new LinuxScripts() , then
x.verifySpin(true) for spin lock/unlock pairing analysis OR x.verifyMutex(true) for mutex lock/unlock pairing analysis. The true/false argument passed to each function correspond to whether to enable feasibility checking for the potentially-error paths if found.
The analysis results will written into WORKSPACE_PATH folder.