Uses of Package
dev.civl.mc.model.IF.expression
Packages that use dev.civl.mc.model.IF.expression
Package
Description
Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
Submodule model.expression defines expression in CIVL.
Submodule model.location defines a location in the control flow graph of CIVL.
Submodule model.statement defines a statement of a CIVL-C program.
Submodule model.type defines types in CIVL.
Module semantics implements the semantics of CIVL-C.
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IFClassDescriptionAn expression representing a call of an abstract function.This represents an address-of expression, which contains one operand, and has the format:
invalid input: '&x', whereinvalid input: '&'is the address-of operator andxis the operand.A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.A binary operation.This defines all CIVL binary operators:
AND: invalid input: '&'invalid input: '&'(logical and); LEFT_SHIFT:invalid input: '<'(bitwise left shift); RIGHT_SHIFT:>>(bitwise right shift); BITAND:invalid input: '&'(bitwise and); BITCOMPLEMENT:~(bitwise complement); BITOR:|(bitwise or); BITXOR:^(bitwise xor); DIVIDE:/(division); EQUAL:==(equal to); IMPLIES:(implication); LESS_THAN:invalid input: '<'(less than); LESS_THAN_EQUAL:invalid input: '<'=(less than or equal to); MINUS:-(subtraction); MODULO:%(modulo); NOT_EQUAL:!=(not equal to); OR:||(logical or); PLUS:+(addition); POINTER_ADD:+(pointer addition); POINTER_SUBTRACT:-(pointer subtraction); TIMES:*(multiplication);A literal boolean value.A bound variable is a variable used in a quantified expression.A cast of an expression to a different type.This class represents compound literal expressions, including string literals.The ternary conditional expression ("?" in C).An uninterpreted call to the derivative of an abstract function.This expression encodes the claim that a real, abstract function is differentiable.This is the guard expression of CIVL for loops ($for).A dot expression is a reference to a field in a struct or union.A "DynamicTypeOf" expression.The parent of all expressions.The representation for the "fold expression" in ACSL, e.g.An expression yielding the initial value of a variable.An integer literal.A CIVL-C quanti, bound variable declaration list, (optional) restriction and expression.A left-hand-side expression.A memory unit expression is an expression that represents (part of) the memory related to some variable.A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.The different kinds of quantifiers which are possible.A real literal.This is a rectangular domain literal expression, which is the Cartesian product of a number of ranges, e.g.,{range1, range2, range3, ...}.Represents a CIVL-C regular range expression, which has the formlo ..A scopeof expression is "$scopeof(expr)".Self expression.An expression of the form "sizeof(e)" where e is an expression.An expression of the form "sizeof(t)" where t is a type.a[i], where "a" is an array and "i" is an expression evaluating to an integer.A unary operation.A use of a variable in an expression.This represents the expression..., which is used only in contracts and stands for an expression of any type whose value is ignored. -
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.contractClassDescriptionThe parent of all expressions.A left-hand-side expression.
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.expressionClassDescriptionAn expression representing a call of an abstract function.This defines all CIVL binary operators:
AND: invalid input: '&'invalid input: '&'(logical and); LEFT_SHIFT:invalid input: '<'(bitwise left shift); RIGHT_SHIFT:>>(bitwise right shift); BITAND:invalid input: '&'(bitwise and); BITCOMPLEMENT:~(bitwise complement); BITOR:|(bitwise or); BITXOR:^(bitwise xor); DIVIDE:/(division); EQUAL:==(equal to); IMPLIES:(implication); LESS_THAN:invalid input: '<'(less than); LESS_THAN_EQUAL:invalid input: '<'=(less than or equal to); MINUS:-(subtraction); MODULO:%(modulo); NOT_EQUAL:!=(not equal to); OR:||(logical or); PLUS:+(addition); POINTER_ADD:+(pointer addition); POINTER_SUBTRACT:-(pointer subtraction); TIMES:*(multiplication);The CIVL model counterpart ofCompoundLiteralObjectin ABC.The CIVL model counterpart ofLiteralObjectin ABC.The ternary conditional expression ("?" in C).The parent of all expressions.An integer literal.A left-hand-side expression.The parent of all literal expressions.The different kinds of quantifiers which are possible.A use of a variable in an expression. -
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.expression.reference
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.locationClassDescriptionThe parent of all expressions.A memory unit expression is an expression that represents (part of) the memory related to some variable.
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.statementClassDescriptionThe ternary conditional expression ("?" in C).The parent of all expressions.A left-hand-side expression.A use of a variable in an expression.
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.model.IF.type
-
Classes in dev.civl.mc.model.IF.expression used by dev.civl.mc.semantics.IFClassDescriptionA binary operation.The parent of all expressions.A left-hand-side expression.A memory unit expression is an expression that represents (part of) the memory related to some variable.