package goblint-cil

For debugging purposes, the name of the analysis

Whether to turn on debugging

The type of the data we compute for each block start. In many * presentations of backwards data flow analysis we maintain the * data at the block end. This is not easy to do with JVML because * a block has many exceptional ends. So we maintain the data for * the statement start.

Pretty-print the state

For each block id, the data at the start. This data structure must be * initialized with the initial data for each block

The data at function exit. Used for statements with no successors. This is usually bottom, since we'll also use doStmt on Return statements.

When the analysis reaches the start of a block, combine the old data * with the one we have just computed. Return None if the combination is * the same as the old data, otherwise return the combination. In the * latter case, the predecessors of the statement are put on the working * list.

Take the data from two successors and combine it

The (backwards) transfer function for a branch. The Cil.currentLoc is * set before calling this. If it returns None, then we have some default * handling. Otherwise, the returned data is the data before the branch * (not considering the exception handlers)

The (backwards) transfer function for an instruction. The * Cil.currentLoc is set before calling this. If it returns None, then we * have some default handling. Otherwise, the returned data is the data * before the branch (not considering the exception handlers)

Whether to put this predecessor block in the worklist. We give the * predecessor and the block whose predecessor we are (and whose data has * changed)