Module dev.civl.mc
Package dev.civl.mc.model.IF.expression
package dev.civl.mc.model.IF.expression
Submodule model.expression defines expression in CIVL.
-
ClassDescriptionAn 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 CIVL model counterpart ofCompoundLiteralObjectin ABC.The CIVL model counterpart ofLiteralObjectin ABC.The CIVL model counterpart ofScalarLiteralObjectin ABC.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.A function guard expression is the guard expression of a function call with a function pointer.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.The parent of all literal expressions.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.This class represents a $state_null constant expression.a[i], where "a" is an array and "i" is an expression evaluating to an integer.A system guard expression is a pseudo guard expression for system function calls.A unary operation.Self expression.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.