Module dev.civl.mc
Package dev.civl.mc.model.IF
package dev.civl.mc.model.IF
Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
-
ClassDescriptionAn abstract function is an uninterpreted mathematical function.The kind of a special relation represented by this abstract functionAn accuracy assumption builder provides logic for determining additional assumptions that should be added after an assumption involving an abstract function call.Root of CIVL exception hierarchy, representing any kind of event where something goes wrong in CIVL.A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error.A CIVL function.A CIVL internal exception represents an error that is "not supposed to happen." It can be used like an assertion, whenever you feel that something should always be true.Enum class for representing different properties that CIVL checks for.A CIVLSource object represents a range of text in a source file.An exception thrown when there is syntax error in the program being verified, e.g., calling $choose_int with more than one arguments, etc.The CIVL type factory provides the CIVL primitive types, like
$bool,int,float,$scope, etc.An exception thrown when there is not necessarily anything wrong with the program begin verified, but some CIVL feature has not yet been implemented.A fragment is a sequence of statements.An identifier.A logic function is a function whose definition (body) is either absent (i.e.A model of a CIVL program.Class to provide translation from an AST to a model.This file contains the constants used by the model builder/translator, which reflects the translation strategy of CIVL.The factory to create all model components.This is the entry point of the module model.A scope.A system function is a function that is implemented in a library executor, not in source code.