inductive CProverGOTO.Expr.Identifier.Nullary : Type

• symbol (name : String) : Nullary

  symbol_exprt

• constant (value : String) : Nullary

  constant_exprt

• nondet (name : String) : Nullary

  nondet_symbol_exprt

• nil : Nullary

  nil_exprt

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprNullary : Repr Nullary

Equations

• CProverGOTO.Expr.Identifier.instReprNullary = { reprPrec := CProverGOTO.Expr.Identifier.instReprNullary.repr }

def CProverGOTO.Expr.Identifier.instReprNullary.repr : Nullary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedNullary : Inhabited Nullary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedNullary = { default := CProverGOTO.Expr.Identifier.instInhabitedNullary.default }

def CProverGOTO.Expr.Identifier.instInhabitedNullary.default : Nullary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedNullary.default = CProverGOTO.Expr.Identifier.Nullary.symbol default

def CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (x✝ x✝¹ : Nullary) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.symbol name) (CProverGOTO.Expr.Identifier.Nullary.constant value) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.symbol name) (CProverGOTO.Expr.Identifier.Nullary.nondet name_1) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.symbol name) CProverGOTO.Expr.Identifier.Nullary.nil = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.constant value) (CProverGOTO.Expr.Identifier.Nullary.symbol name) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.constant value) (CProverGOTO.Expr.Identifier.Nullary.nondet name) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.constant value) CProverGOTO.Expr.Identifier.Nullary.nil = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.nondet name) (CProverGOTO.Expr.Identifier.Nullary.symbol name_1) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.nondet name) (CProverGOTO.Expr.Identifier.Nullary.constant value) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq (CProverGOTO.Expr.Identifier.Nullary.nondet name) CProverGOTO.Expr.Identifier.Nullary.nil = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq CProverGOTO.Expr.Identifier.Nullary.nil (CProverGOTO.Expr.Identifier.Nullary.symbol name) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq CProverGOTO.Expr.Identifier.Nullary.nil (CProverGOTO.Expr.Identifier.Nullary.constant value) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq CProverGOTO.Expr.Identifier.Nullary.nil (CProverGOTO.Expr.Identifier.Nullary.nondet name) = isFalse ⋯
• CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq CProverGOTO.Expr.Identifier.Nullary.nil CProverGOTO.Expr.Identifier.Nullary.nil = isTrue ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqNullary : DecidableEq Nullary

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqNullary = CProverGOTO.Expr.Identifier.instDecidableEqNullary.decEq

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatNullary : Std.ToFormat Nullary

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier.Unary : Type

• UnaryMinus : Unary

  unary_minus_exprt

• UnaryPlus : Unary

  unary_plus_exprt

• Not : Unary

  not_exprt

• Bitnot : Unary

  bitnot_exprt

• Old : Unary

  history_exprt with ID_old

• ArrayOf : Unary

  array_of_exprt (constant map/array)

• Typecast : Unary

  typecast_exprt

• UnaryMinusOverflow : Unary

  unary_minus_overflow_exprt

• Dereference : Unary

  dereference_exprt (*p)

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprUnary : Repr Unary

Equations

• CProverGOTO.Expr.Identifier.instReprUnary = { reprPrec := CProverGOTO.Expr.Identifier.instReprUnary.repr }

def CProverGOTO.Expr.Identifier.instReprUnary.repr : Unary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedUnary : Inhabited Unary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedUnary = { default := CProverGOTO.Expr.Identifier.instInhabitedUnary.default }

def CProverGOTO.Expr.Identifier.instInhabitedUnary.default : Unary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedUnary.default = CProverGOTO.Expr.Identifier.Unary.UnaryMinus

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqUnary : DecidableEq Unary

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqUnary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatUnary : Std.ToFormat Unary

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier.Binary : Type

Representation of identifiers specific to binary expressions, binary_exprt.

• Div : Binary

  div_exprt

• Mod : Binary

  mod_exprt

• Minus : Binary

  minus_exprt

• Shl : Binary

  shl_exprt

• Ashr : Binary

  ashr_exprt

• Lshr : Binary

  lshr_exprt

• PlusOverflow : Binary

  plus_overflow_exprt

• MinusOverflow : Binary

  minus_overflow_exprt

• MultOverflow : Binary

  mult_overflow_exprt

• Implies : Binary

  implies_exprt

• Index : Binary

  index_exprt (map/array select)

• Forall : Binary

  forall_exprt

• Exists : Binary

  exists_exprt

• Gt : Binary
• Lt : Binary
• Ge : Binary
• Le : Binary
• Equal : Binary
• NotEqual : Binary
• Bitand : Binary

  bitand_exprt

• Bitor : Binary

  bitor_exprt

• Bitxor : Binary

  bitxor_exprt

• Concatenation : Binary

  concatenation_exprt (bitvector concatenation)

• Extractbits : Binary

  extractbits_exprt (bitvector extraction)

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprBinary : Repr Binary

Equations

• CProverGOTO.Expr.Identifier.instReprBinary = { reprPrec := CProverGOTO.Expr.Identifier.instReprBinary.repr }

def CProverGOTO.Expr.Identifier.instReprBinary.repr : Binary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def CProverGOTO.Expr.Identifier.instInhabitedBinary.default : Binary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedBinary.default = CProverGOTO.Expr.Identifier.Binary.Div

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedBinary : Inhabited Binary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedBinary = { default := CProverGOTO.Expr.Identifier.instInhabitedBinary.default }

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqBinary : DecidableEq Binary

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqBinary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatBinary : Std.ToFormat Binary

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier.Ternary : Type

• ite : Ternary

  if_exprt

• with : Ternary

  with_exprt (map/array update)

def CProverGOTO.Expr.Identifier.instReprTernary.repr : Ternary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprTernary : Repr Ternary

Equations

• CProverGOTO.Expr.Identifier.instReprTernary = { reprPrec := CProverGOTO.Expr.Identifier.instReprTernary.repr }

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedTernary : Inhabited Ternary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedTernary = { default := CProverGOTO.Expr.Identifier.instInhabitedTernary.default }

def CProverGOTO.Expr.Identifier.instInhabitedTernary.default : Ternary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedTernary.default = CProverGOTO.Expr.Identifier.Ternary.ite

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqTernary : DecidableEq Ternary

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqTernary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatTernary : Std.ToFormat Ternary

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier.Multiary : Type

• And : Multiary

  and_exprt

• Or : Multiary

  or_exprt

• Mult : Multiary

  mult_exprt

• Plus : Multiary

  plus_exprt

def CProverGOTO.Expr.Identifier.instReprMultiary.repr : Multiary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprMultiary : Repr Multiary

Equations

• CProverGOTO.Expr.Identifier.instReprMultiary = { reprPrec := CProverGOTO.Expr.Identifier.instReprMultiary.repr }

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedMultiary : Inhabited Multiary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedMultiary = { default := CProverGOTO.Expr.Identifier.instInhabitedMultiary.default }

def CProverGOTO.Expr.Identifier.instInhabitedMultiary.default : Multiary

Equations

• CProverGOTO.Expr.Identifier.instInhabitedMultiary.default = CProverGOTO.Expr.Identifier.Multiary.And

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqMultiary : DecidableEq Multiary

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqMultiary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatMultiary : Std.ToFormat Multiary

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier.SideEffect : Type

• Nondet : SideEffect

  side_effect_expr_nondett

• Assign : SideEffect

  side_effect_expr_assignt

• Allocate : SideEffect

  side_effect_exprt with ID_allocate (native dynamic-object allocation; operands = [size, zeroInitFlag], type is the result pointer).

def CProverGOTO.Expr.Identifier.instReprSideEffect.repr : SideEffect → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instReprSideEffect : Repr SideEffect

Equations

• CProverGOTO.Expr.Identifier.instReprSideEffect = { reprPrec := CProverGOTO.Expr.Identifier.instReprSideEffect.repr }

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instInhabitedSideEffect : Inhabited SideEffect

Equations

• CProverGOTO.Expr.Identifier.instInhabitedSideEffect = { default := CProverGOTO.Expr.Identifier.instInhabitedSideEffect.default }

def CProverGOTO.Expr.Identifier.instInhabitedSideEffect.default : SideEffect

Equations

• CProverGOTO.Expr.Identifier.instInhabitedSideEffect.default = CProverGOTO.Expr.Identifier.SideEffect.Nondet

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instDecidableEqSideEffect : DecidableEq SideEffect

Equations

• CProverGOTO.Expr.Identifier.instDecidableEqSideEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.Identifier.instToFormatSideEffect : Std.ToFormat SideEffect

Equations

• One or more equations did not get rendered due to their size.

inductive CProverGOTO.Expr.Identifier : Type

• nullary (n : Nullary) : Identifier
• unary (u : Unary) : Identifier
• binary (b : Binary) : Identifier
• ternary (t : Ternary) : Identifier
• multiary (m : Multiary) : Identifier
• side_effect (s : SideEffect) : Identifier
• functionApplication (name : String) : Identifier

  function_application_exprt - uninterpreted function application

def CProverGOTO.Expr.instReprIdentifier.repr : Identifier → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.Expr.instReprIdentifier : Repr Identifier

Equations

• CProverGOTO.Expr.instReprIdentifier = { reprPrec := CProverGOTO.Expr.instReprIdentifier.repr }

def CProverGOTO.Expr.instInhabitedIdentifier.default : Identifier

Equations

• CProverGOTO.Expr.instInhabitedIdentifier.default = CProverGOTO.Expr.Identifier.nullary default

@[implicit_reducible]

instance CProverGOTO.Expr.instInhabitedIdentifier : Inhabited Identifier

Equations

• CProverGOTO.Expr.instInhabitedIdentifier = { default := CProverGOTO.Expr.instInhabitedIdentifier.default }

@[implicit_reducible]

instance CProverGOTO.Expr.instDecidableEqIdentifier : DecidableEq Identifier

Equations

• CProverGOTO.Expr.instDecidableEqIdentifier = CProverGOTO.Expr.instDecidableEqIdentifier.decEq

def CProverGOTO.Expr.instDecidableEqIdentifier.decEq (x✝ x✝¹ : Identifier) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary a) (CProverGOTO.Expr.Identifier.nullary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.nullary n) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary a) (CProverGOTO.Expr.Identifier.unary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.unary u) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary a) (CProverGOTO.Expr.Identifier.binary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.binary b) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary a) (CProverGOTO.Expr.Identifier.ternary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.ternary t) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary a) (CProverGOTO.Expr.Identifier.multiary b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.multiary m) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect a) (CProverGOTO.Expr.Identifier.side_effect b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.side_effect s) (CProverGOTO.Expr.Identifier.functionApplication name) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.nullary n) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.unary u) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.binary b) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.ternary t) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.multiary m) = isFalse ⋯
• CProverGOTO.Expr.instDecidableEqIdentifier.decEq (CProverGOTO.Expr.Identifier.functionApplication name) (CProverGOTO.Expr.Identifier.side_effect s) = isFalse ⋯

@[implicit_reducible]

instance CProverGOTO.Expr.instToFormatIdentifier : Std.ToFormat Identifier

Equations

• One or more equations did not get rendered due to their size.

structure CProverGOTO.Expr : Type

GOTO Expressions

For now, we have primarily focused on expr_protectedt class.

We will also confine ourselves to expressions that can appear at the lowest level of CProver IRs -- i.e., GOTO assembly instructions.

• id : Identifier

  The interpretation of Expr depends on the id field. CBMC pre-defines some IDs here: util/irep_ids.def.

• type : Ty
• operands : List Expr
• sourceLoc : SourceLocation
• namedFields : List (String × Expr)

  Named fields for expressions that need additional data (e.g., side_effect_exprt has a statement field).

partial def CProverGOTO.instReprExpr.repr : Expr → Nat → Std.Format

@[implicit_reducible]

instance CProverGOTO.instReprExpr : Repr Expr

Equations

• CProverGOTO.instReprExpr = { reprPrec := CProverGOTO.instReprExpr.repr }

def CProverGOTO.instInhabitedExpr.default : Expr

Equations

• CProverGOTO.instInhabitedExpr.default = { id := default, type := default, operands := default, sourceLoc := default, namedFields := default }

@[implicit_reducible]

instance CProverGOTO.instInhabitedExpr : Inhabited Expr

Equations

• CProverGOTO.instInhabitedExpr = { default := CProverGOTO.instInhabitedExpr.default }

@[irreducible]

def CProverGOTO.Expr.beq (x y : Expr) : Bool

Equations

• x.beq y = (x.id == y.id && x.type == y.type && x.sourceLoc == y.sourceLoc && CProverGOTO.Expr.beq.go✝ x.operands y.operands)

@[implicit_reducible]

instance CProverGOTO.instBEqExpr : BEq Expr

Equations

• CProverGOTO.instBEqExpr = { beq := CProverGOTO.Expr.beq }

@[irreducible]

def CProverGOTO.formatExpr (e : Expr) : Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CProverGOTO.instToFormatExpr : Std.ToFormat Expr

Equations

• CProverGOTO.instToFormatExpr = { format := fun (e : CProverGOTO.Expr) => CProverGOTO.formatExpr e }

def CProverGOTO.Expr.true : Expr

Equations

• CProverGOTO.Expr.true = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.constant "true"), type := CProverGOTO.Ty.Boolean }

def CProverGOTO.Expr.getNamedField (e : Expr) (name : String) : Option Expr

Get a named field from the expression.

Equations

• One or more equations did not get rendered due to their size.

def CProverGOTO.Expr.setNamedField (e : Expr) (name : String) (value : Expr) : Expr

Set a named field in the expression.

Equations

• One or more equations did not get rendered due to their size.

def CProverGOTO.Expr.symbol (name : String) (type : Ty) : Expr

Symbol expression

Equations

• CProverGOTO.Expr.symbol name type = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.symbol name), type := type }

def CProverGOTO.Expr.constant (value : String) (type : Ty) : Expr

Constant expression

Equations

• CProverGOTO.Expr.constant value type = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.constant value), type := type }

def CProverGOTO.Expr.nondet (name : String) (type : Ty) : Expr

Nondet expression

Equations

• CProverGOTO.Expr.nondet name type = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.nondet name), type := type }

def CProverGOTO.Expr.neg (operand : Expr) : Expr

Unary minus

Equations

• operand.neg = { id := CProverGOTO.Expr.Identifier.unary CProverGOTO.Expr.Identifier.Unary.UnaryMinus, type := operand.type, operands := [operand] }

def CProverGOTO.Expr.not (operand : Expr) : Expr

Logical not

Equations

• operand.not = { id := CProverGOTO.Expr.Identifier.unary CProverGOTO.Expr.Identifier.Unary.Not, type := operand.type, operands := [operand] }

def CProverGOTO.Expr.plus_overflow (left right : Expr) : Expr

Overflow-+

Equations

• left.plus_overflow right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.PlusOverflow, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.minus_overflow (left right : Expr) : Expr

Overflow--

Equations

• left.minus_overflow right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.MinusOverflow, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.mult_overflow (left right : Expr) : Expr

Overflow-*

Equations

• left.mult_overflow right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.MultOverflow, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.unary_minus_overflow (operand : Expr) : Expr

Overflow-unary-

Equations

• operand.unary_minus_overflow = { id := CProverGOTO.Expr.Identifier.unary CProverGOTO.Expr.Identifier.Unary.UnaryMinusOverflow, type := CProverGOTO.Ty.Boolean, operands := [operand] }

def CProverGOTO.Expr.typecast (operand : Expr) (targetType : Ty) : Expr

Typecast expression

Equations

• operand.typecast targetType = { id := CProverGOTO.Expr.Identifier.unary CProverGOTO.Expr.Identifier.Unary.Typecast, type := targetType, operands := [operand] }

def CProverGOTO.Expr.dereference (ptr : Expr) (pointee : Ty) : Expr

Dereference (*ptr) yielding a value of type pointee.

Equations

• ptr.dereference pointee = { id := CProverGOTO.Expr.Identifier.unary CProverGOTO.Expr.Identifier.Unary.Dereference, type := pointee, operands := [ptr] }

def CProverGOTO.Expr.allocate (size zeroFlag : Expr) (ptrTy : Ty) : Expr

Native dynamic-object allocation (side_effect ID_allocate): allocate size bytes, optionally zero-initialized, returning a pointer of type ptrTy. Mirrors CBMC's __CPROVER_allocate.

Equations

• size.allocate zeroFlag ptrTy = { id := CProverGOTO.Expr.Identifier.side_effect CProverGOTO.Expr.Identifier.SideEffect.Allocate, type := ptrTy, operands := [size, zeroFlag] }

def CProverGOTO.Expr.toSigned (e : Expr) : Expr

Cast a bitvector expression to its signed interpretation.

Equations

• e.toSigned = match e.type.id with | CProverGOTO.Ty.Identifier.bitVector (CProverGOTO.Ty.Identifier.BitVector.unsignedbv w) => e.typecast (CProverGOTO.Ty.SignedBV w) | x => e

def CProverGOTO.Expr.div (left right : Expr) : Expr

Division

Equations

• left.div right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.Div, type := left.type, operands := [left, right] }

def CProverGOTO.Expr.mod (left right : Expr) : Expr

Modulo

Equations

• left.mod right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.Mod, type := left.type, operands := [left, right] }

def CProverGOTO.Expr.gt (left right : Expr) : Expr

Greater than

Equations

• left.gt right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.Gt, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.lt (left right : Expr) : Expr

Less than

Equations

• left.lt right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.Lt, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.eq (left right : Expr) : Expr

Equal

Equations

• left.eq right = { id := CProverGOTO.Expr.Identifier.binary CProverGOTO.Expr.Identifier.Binary.Equal, type := CProverGOTO.Ty.Boolean, operands := [left, right] }

def CProverGOTO.Expr.add (operands : List Expr) : Expr

Addition

Equations

• CProverGOTO.Expr.add [] = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.constant "0"), type := CProverGOTO.Ty.Integer }
• CProverGOTO.Expr.add [x] = x
• CProverGOTO.Expr.add (x :: tail) = { id := CProverGOTO.Expr.Identifier.multiary CProverGOTO.Expr.Identifier.Multiary.Plus, type := x.type, operands := x :: tail }

def CProverGOTO.Expr.mul (operands : List Expr) : Expr

Multiplication

Equations

• CProverGOTO.Expr.mul [] = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.constant "1"), type := CProverGOTO.Ty.Integer }
• CProverGOTO.Expr.mul [x] = x
• CProverGOTO.Expr.mul (x :: tail) = { id := CProverGOTO.Expr.Identifier.multiary CProverGOTO.Expr.Identifier.Multiary.Mult, type := x.type, operands := x :: tail }

def CProverGOTO.Expr.and (operands : List Expr) : Expr

Logical and

Equations

• CProverGOTO.Expr.and [] = CProverGOTO.Expr.true
• CProverGOTO.Expr.and [x] = x
• CProverGOTO.Expr.and operands = { id := CProverGOTO.Expr.Identifier.multiary CProverGOTO.Expr.Identifier.Multiary.And, type := CProverGOTO.Ty.Boolean, operands := operands }

def CProverGOTO.Expr.or (operands : List Expr) : Expr

Logical or

Equations

• CProverGOTO.Expr.or [] = { id := CProverGOTO.Expr.Identifier.nullary (CProverGOTO.Expr.Identifier.Nullary.constant "false"), type := CProverGOTO.Ty.Boolean }
• CProverGOTO.Expr.or [x] = x
• CProverGOTO.Expr.or operands = { id := CProverGOTO.Expr.Identifier.multiary CProverGOTO.Expr.Identifier.Multiary.Or, type := CProverGOTO.Ty.Boolean, operands := operands }

def CProverGOTO.Expr.ite (cond then_expr else_expr : Expr) : Expr

If-then-else

Equations

• cond.ite then_expr else_expr = { id := CProverGOTO.Expr.Identifier.ternary CProverGOTO.Expr.Identifier.Ternary.ite, type := then_expr.type, operands := [cond, then_expr, else_expr] }

def CProverGOTO.Expr.side_effect_nondet (namedFields : List (String × Expr)) : Expr

Non-deterministic side effects

Equations

• One or more equations did not get rendered due to their size.

partial def CProverGOTO.Expr.hasUnsupportedQuantifierTypes (e : Expr) : Bool

Check whether an expression contains quantifiers over types that CBMC's SMT2 backend cannot encode (e.g., struct_tag, regex).