Module Goblint_lib.TerminationPreprocessing

module VarToStmt : sig ... end
val counter_ikind : GoblintCil.ikind
val counter_typ : GoblintCil.typ
val min_int_exp : GoblintCil.exp
class loopCounterVisitor : GoblintCil.stmt VarToStmt.t Stdlib.ref -> GoblintCil.fundec -> object ... end
type jump = {
  1. jump_stmt : GoblintCil.stmt;
  2. jump_loc : GoblintCil.location;
  3. target_stmt : GoblintCil.stmt;
}

A jump of a goto (or asm goto) statement jump_stmt at jump_loc to target_stmt.

class jumpCollector : jump list Stdlib.ref -> GoblintCil.stmt list Stdlib.ref -> object ... end

Collects the jumps of gotos into jumps and the continue statements of loops into continue_stmts.

val jumps_backwards : jump -> bool

Whether jump goes backwards, i.e., to a statement with a smaller or equal sid.

val upjumping_gotos : GoblintCil.fundec -> GoblintCil.location list

Locations of the gotos in fd that jump backwards. Jumps to the continue statement of a loop are not included, since the loop counter bounds them. The CFG of fd must already be computed, as this relies on sids and on the continue statements of loops introduced by prepareCFG.