package goblint

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Termination analysis for loops and goto statements (termination).

Contains all loop counter variables (varinfo) and maps them to their corresponding loop statement.

val check_bounded : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.varinfo -> bool

Checks whether a variable can be bounded.

module Statements : sig ... end

We want to record termination information of loops and use the loop * statements for that. We use this lifting because we need to have a * lattice.

The termination analysis considering loops and gotos

OCaml

Innovation. Community. Security.