// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! find mod.rs for centralized documentation //! //! This file contains [IrepId] which is the id's used in CBMC. //! c.f. CBMC source code [src/util/irep_ids.def] use crate::cbmc_string::InternedString; use crate::utils::NumUtils; use num::bigint::{BigInt, BigUint, Sign}; #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)] pub enum IrepId { /// In addition to the standard enums defined below, CBMC also allows ids to be strings. /// For e.g, to store the id of a variable. This enum variant captures those strings. FreeformString(InternedString), /// An integer, to be encoded as a decimal string FreeformInteger(BigInt), /// A constant, stored as a bit pattern (negative numbers in 2's complement). FreeformBitPattern(BigUint), EmptyString, Let, LetBinding, Nil, Type, Bool, CBool, ProperBool, Signedbv, Unsignedbv, VerilogSignedbv, VerilogUnsignedbv, Floatbv, Fixedbv, X86Extended, CSourceLocation, CEndLocation, CIsPadding, CDoNotDump, File, Line, Column, Comment, Property, PropertyClass, PropertyId, Function, MathematicalFunction, Code, Typecast, StaticCast, DynamicCast, ConstCast, ReinterpretCast, Index, Ptrmember, Member, MemberName, CMemberName, Equal, Implies, And, Nand, Or, Nor, Xor, Not, Bitand, Bitor, Bitnot, Bitxor, Bitnand, Bitnor, Bitxnor, Notequal, If, Symbol, NextSymbol, NondetSymbol, PredicateSymbol, PredicateNextSymbol, NondetBool, Empty, SideEffect, Statement, StatementExpression, Value, Constant, Block, Decl, Dead, Assign, AssignDiv, AssignMult, AssignPlus, AssignMinus, AssignMod, AssignShl, AssignShr, AssignAshr, AssignLshr, AssignBitand, AssignBitxor, AssignBitor, Assume, Assert, Assertion, Precondition, Postcondition, PreconditionInstance, Goto, GccComputedGoto, Ifthenelse, Label, Break, Continue, FunctionCall, Return, Skip, Arguments, Array, Size, FrontendPointer, Pointer, BlockPointer, Switch, SwitchCase, GccSwitchCaseRange, For, While, Dowhile, Int, Integer, Natural, Real, Rational, Complex, Signed, Unsigned, Asm, GccAsmInput, GccAsmOutput, GccAsmClobberedRegister, Incomplete, IncompleteClass, CIncomplete, Identifier, Name, InnerName, CppName, ComponentCppName, CIdClass, Declaration, DeclarationList, Declarator, Struct, CBitField, Union, Class, MergedType, Range, From, To, Module, Parameter, ComponentName, ComponentNumber, Tag, Default, CDefaultValue, BaseName, CBaseName, String, CStringConstant, StringConstant, Width, Components, Bv, F, With, Trans, Throw, TryCatch, Noexcept, CPROVERThrow, CPROVERTryCatch, CPROVERTryFinally, Protection, Private, Public, Protected, Virtual, Volatile, Const, Constexpr, Inline, Forall, Exists, Repeat, Extractbit, Extractbits, CReference, CRvalueReference, True, False, AddressOf, Dereference, CLvalue, CBase, Destination, Main, Expression, Allocate, CCxxAllocType, CppNew, CppDelete, CppNewArray, CppDeleteArray, JavaNew, JavaNewArray, JavaNewArrayData, JavaStringLiteral, Printf, Input, Output, Nondet, NULL, Null, Nullptr, CEnum, Enumeration, Elements, Unknown, Uninitialized, Invalid, CInvalidObject, PointerOffset, PointerObject, IsInvalidPointer, IeeeFloatEqual, IeeeFloatNotequal, Isnan, Lambda, ArrayComprehension, ArrayOf, ArrayEqual, ArraySet, ArrayCopy, ArrayList, Mod, Rem, Shr, Ashr, Lshr, Shl, Rol, Ror, Comma, Concatenation, Infinity, ReturnType, Typedef, TypedefType, CTypedef, Extern, Static, Auto, Register, ThreadLocal, Thread, CThreadLocal, CStaticLifetime, Mutable, Void, Int8, Int16, Int32, Int64, Ptr32, Ptr64, Char, Short, Long, Float, Double, Byte, Boolean, LongDouble, SignedChar, UnsignedChar, SignedInt, UnsignedInt, SignedLongInt, UnsignedLongInt, SignedShortInt, UnsignedShortInt, SignedLongLongInt, UnsignedLongLongInt, SignedInt128, UnsignedInt128, Case, CInlined, CHide, Hide, Abs, Sign, Access, CAccess, Postincrement, Postdecrement, Preincrement, Predecrement, IntegerBits, KnR, CKnR, ConstraintSelectOne, Cond, BvLiterals, IsFinite, Isinf, Isnormal, Alignof, ClangBuiltinConvertvector, GccBuiltinVaArg, GccBuiltinTypesCompatibleP, VaStart, GccFloat16, GccFloat32, GccFloat32x, GccFloat64, GccFloat64x, GccFloat80, GccFloat128, GccFloat128x, GccInt128, GccDecimal32, GccDecimal64, GccDecimal128, BuiltinOffsetof, Id0, Id1, Sizeof, TypeArg, ExprArg, ExpressionList, InitializerList, GccConditionalExpression, GccLocalLabel, Gcc, Msc, Typeof, Ellipsis, Flavor, Ge, Le, Gt, Lt, Plus, Minus, UnaryMinus, UnaryPlus, Mult, Div, Power, FactorialPower, PrettyName, CClass, CField, CInterface, DesignatedInitializer, Designator, MemberDesignator, IndexDesignator, CConstant, CVolatile, CRestricted, CIdentifier, CImplicit, CPtr32, CPtr64, CAtomic, Restrict, ByteExtractBigEndian, ByteExtractLittleEndian, ByteUpdateBigEndian, ByteUpdateLittleEndian, Replication, CproverAtomic, Atomic, AtomicTypeSpecifier, AtomicBegin, AtomicEnd, StartThread, EndThread, CoverageCriterion, Initializer, Anonymous, CIsAnonymous, IsEnumConstant, IsInline, IsExtern, IsSynchronized, IsNativeMethod, IsVarargsMethod, IsGlobal, IsThreadLocal, IsParameter, IsMember, IsType, IsRegister, IsTypedef, IsStatic, IsTemplate, IsStaticAssert, IsVirtual, CIsVirtual, Literal, MemberInitializers, MemberInitializer, MethodQualifier, Methods, StaticMembers, Constructor, Destructor, Bases, Base, FromBase, Operator, Template, TemplateClassInstance, TemplateFunctionInstance, TemplateType, TemplateArgs, TemplateParameter, TemplateParameterSymbolType, TemplateParameters, CTemplate, CTemplateArguments, CTemplateCase, Typename, C, Cpp, Java, DeclBlock, DeclType, Parameters, WcharT, Char16T, Char32T, SizeT, SsizeT, Mode, This, CThis, ReductionAnd, ReductionOr, ReductionNand, ReductionNor, ReductionXor, ReductionXnor, CZeroInitializer, Body, TemporaryObject, OverflowPlus, OverflowMinus, OverflowMult, OverflowResultPlus, OverflowResultMinus, OverflowResultMult, OverflowUnaryMinus, ObjectDescriptor, IsDynamicObject, DynamicObject, CDynamic, ObjectSize, GoodPointer, IntegerAddress, IntegerAddressObject, NullObject, StaticObject, StackObject, CIsFailedSymbol, CFailedSymbol, Friend, CFriends, Explicit, StorageSpec, MemberSpec, MscDeclspec, Packed, CPacked, TransparentUnion, CTransparentUnion, Aligned, CAlignment, FrontendVector, Vector, Abstract, FunctionApplication, CppDeclarator, CppLinkageSpec, CppNamespaceSpec, CppStorageSpec, CppUsing, CppDeclaration, CppStaticAssert, CppMemberSpec, CCType, Namespace, Linkage, Decltype, CTagOnlyDeclaration, StructTag, UnionTag, CEnumTag, VerilogCaseEquality, VerilogCaseInequality, UserSpecifiedPredicate, UserSpecifiedParameterPredicates, UserSpecifiedReturnPredicates, Unassigned, NewObject, ComplexReal, ComplexImag, Imag, MscTryExcept, MscTryFinally, MscLeave, MscUuidof, MscIfExists, MscIfNotExists, MscUnderlyingType, MscBased, Alias, PtrObject, CCSizeofType, ArrayUpdate, Update, StaticAssert, GccAttributeMode, BuiltIn, ExceptionList, ExceptionId, PredicatePassiveSymbol, CwVaArgTypeof, Fence, Sync, Lwsync, Isync, WRfence, RRfence, RWfence, WWfence, RRcumul, RWcumul, WWcumul, WRcumul, GenericSelection, GenericAssociations, GenericAssociation, FloatbvPlus, FloatbvMinus, FloatbvMult, FloatbvDiv, FloatbvRem, FloatbvTypecast, CompoundLiteral, CustomBv, CustomUnsignedbv, CustomSignedbv, CustomFixedbv, CustomFloatbv, CSSASymbol, L0, L1, L2, L1ObjectIdentifier, AlreadyTypechecked, CVaArgType, Smt2Symbol, Onehot, Onehot0, Popcount, CountLeadingZeros, CountTrailingZeros, EmptyUnion, FunctionType, Noreturn, CNoreturn, Weak, IsWeak, Used, IsUsed, CSpecLoopInvariant, CSpecRequires, CSpecEnsures, VirtualFunction, ElementType, WorkingDirectory, Section, Bswap, BitReverse, JavaBytecodeIndex, JavaInstanceof, JavaSuperMethodCall, JavaEnumStaticUnwind, PushCatch, PopCatch, ExceptionLandingpad, LengthUpperBound, CproverAssociateArrayToPointerFunc, CproverAssociateLengthToArrayFunc, CproverCharLiteralFunc, CproverStringLiteralFunc, CproverStringCharAtFunc, CproverStringCharSetFunc, CproverStringCodePointAtFunc, CproverStringCodePointBeforeFunc, CproverStringCodePointCountFunc, CproverStringOffsetByCodePointFunc, CproverStringCompareToFunc, CproverStringConcatFunc, CproverStringConcatCharFunc, CproverStringConcatCodePointFunc, CproverStringConstrainCharactersFunc, CproverStringContainsFunc, CproverStringCopyFunc, CproverStringDeleteFunc, CproverStringDeleteCharAtFunc, CproverStringEqualFunc, CproverStringEqualsIgnoreCaseFunc, CproverStringEmptyStringFunc, CproverStringEndswithFunc, CproverStringFormatFunc, CproverStringIndexOfFunc, CproverStringInsertFunc, CproverStringIsPrefixFunc, CproverStringIsSuffixFunc, CproverStringIsEmptyFunc, CproverStringLastIndexOfFunc, CproverStringLengthFunc, CproverStringOfIntFunc, CproverStringOfIntHexFunc, CproverStringOfLongFunc, CproverStringOfFloatFunc, CproverStringOfFloatScientificNotationFunc, CproverStringOfDoubleFunc, CproverStringParseIntFunc, CproverStringIsValidIntFunc, CproverStringIsValidLongFunc, CproverStringReplaceFunc, CproverStringSetLengthFunc, CproverStringStartswithFunc, CproverStringSubstringFunc, CproverStringToLowerCaseFunc, CproverStringToUpperCaseFunc, CproverStringTrimFunc, SkipInitialize, BasicBlockCoveredLines, BasicBlockSourceLines, IsNondetNullable, ArrayReplace, SwitchCaseNumber, JavaArrayAccess, JavaMemberAccess, CJavaGenericParameter, CJavaGenericsClassType, CJavaImplicitlyGenericClassType, CJavaGenericSymbol, GenericTypes, ImplicitGenericTypes, TypeVariables, HandleType, JavaLambdaMethodHandle, JavaLambdaMethodHandleIndex, JavaLambdaMethodHandles, HavocObject, OverflowShl, CNoInitializationRequired, CNoNondetInitialization, OverlayClass, OverlayMethod, IgnoredMethod, IsAnnotation, CAnnotations, Final, BitsPerByte, CAbstract, Synthetic, Interface, CMustNotThrow, IsInnerClass, IsAnonymous, OuterClass, IsBridgeMethod, CIsOperator, CNotAccessible, COverrideConstantness, CBound, CBoundsCheck, CIsStatic, CCallByValue, CVirtualName, CUnnamedObject, CTemporaryAvoided, CQualifier, CArrayIni, ROk, WOk, SuperClass, ExceptionsThrownList, CJavaMethodType, Compiled, PartialSpecializationArgs, SpecializationOf, InitArgs, Ambiguous, SpecializationTemplateArgs, FullTemplateArgs, InstantiatedWith, TemplateMethods, CppNotTypechecked, Noaccess, IsOperator, IsCastOperator, IsExplicit, IsMutable, VirtualName, IsPureVirtual, IsVtptr, Prefix, Cv, CppDummyDestructor, CastExpression, PodConstructor, TemplateDecls, ThrowDecl, Typeid, CQuoted, ToMember, PointerToMember, Tuple, FunctionBody, GetMay, SetMay, ClearMay, GetMust, SetMust, ClearMust, Pragma, StatementList, StatementListType, StatementListFunction, StatementListFunctionBlock, StatementListMainFunction, StatementListDataBlock, StatementListVersion, StatementListVarInput, StatementListVarInout, StatementListVarOutput, StatementListVarConstant, StatementListVarTemp, StatementListVarStatic, StatementListReturn, StatementListReturnValueId, StatementListVarEntry, StatementListVarDecls, StatementListNetwork, StatementListNetworks, StatementListTitle, StatementListIdentifier, StatementListLoad, StatementListTransfer, StatementListCall, StatementListNop, StatementListConstAdd, StatementListAccuIntAdd, StatementListAccuIntSub, StatementListAccuIntMul, StatementListAccuIntDiv, StatementListAccuIntEq, StatementListAccuIntNeq, StatementListAccuIntGt, StatementListAccuIntLt, StatementListAccuIntGte, StatementListAccuIntLte, StatementListAccuRealAdd, StatementListAccuRealSub, StatementListAccuRealMul, StatementListAccuRealDiv, StatementListAccuRealEq, StatementListAccuRealNeq, StatementListAccuRealGt, StatementListAccuRealLt, StatementListAccuRealGte, StatementListAccuRealLte, StatementListAccuDintAdd, StatementListAccuDintSub, StatementListAccuDintMul, StatementListAccuDintDiv, StatementListAccuDintEq, StatementListAccuDintNeq, StatementListAccuDintGt, StatementListAccuDintLt, StatementListAccuDintGte, StatementListAccuDintLte, StatementListAnd, StatementListAndNot, StatementListOr, StatementListOrNot, StatementListXor, StatementListXorNot, StatementListAndNested, StatementListAndNotNested, StatementListOrNested, StatementListOrNotNested, StatementListXorNested, StatementListXorNotNested, StatementListNestingClosed, StatementListAssign, StatementListSetRlo, StatementListClrRlo, StatementListSet, StatementListReset, StatementListNot, StatementListInstruction, StatementListInstructions, VectorEqual, VectorNotequal, VectorGe, VectorLe, VectorGt, VectorLt, } impl IrepId { pub fn from_int(i: T) -> IrepId where T: Into, { IrepId::FreeformInteger(i.into()) } /// CBMC expects two's complement for negative numbers. /// /// The bignum crate instead does sign/magnitude when making hex. /// So for negatives, do the two's complement ourselves. pub fn bitpattern_from_int(i: T, width: u64, _signed: bool) -> IrepId where T: Into, { let value: BigInt = i.into(); // TODO https://github.com/model-checking/kani/issues/996 // assert!( // value.fits_in_bits(width, signed), // "Cannot fit value into bits. value {} width: {} signed: {}", // value, // width, // signed // ); let bitpattern = if value.sign() == Sign::Minus { value.two_complement(width).to_biguint().unwrap() } else { value.to_biguint().unwrap() }; IrepId::FreeformBitPattern(bitpattern) } //TODO assert that s is not the string produced by any other IrepId pub fn from_string>(s: T) -> IrepId { IrepId::FreeformString(s.into()) } } impl ToString for IrepId { fn to_string(&self) -> String { match self { IrepId::FreeformString(s) => return s.to_string(), IrepId::FreeformInteger(i) => return i.to_string(), IrepId::FreeformBitPattern(i) => { return format!("{i:X}"); } _ => (), } let s = match self { IrepId::FreeformString(_) | IrepId::FreeformInteger(_) | IrepId::FreeformBitPattern { .. } => unreachable!(), IrepId::EmptyString => "", IrepId::Let => "let", IrepId::LetBinding => "let_binding", IrepId::Nil => "nil", IrepId::Type => "type", IrepId::Bool => "bool", IrepId::CBool => "c_bool", IrepId::ProperBool => "proper_bool", IrepId::Signedbv => "signedbv", IrepId::Unsignedbv => "unsignedbv", IrepId::VerilogSignedbv => "verilog_signedbv", IrepId::VerilogUnsignedbv => "verilog_unsignedbv", IrepId::Floatbv => "floatbv", IrepId::Fixedbv => "fixedbv", IrepId::X86Extended => "x86_extended", IrepId::CSourceLocation => "#source_location", IrepId::CEndLocation => "#end_location", IrepId::CIsPadding => "#is_padding", IrepId::CDoNotDump => "C_do_not_dump", IrepId::File => "file", IrepId::Line => "line", IrepId::Column => "column", IrepId::Comment => "comment", IrepId::Property => "property", IrepId::PropertyClass => "property_class", IrepId::PropertyId => "property_id", IrepId::Function => "function", IrepId::MathematicalFunction => "mathematical_function", IrepId::Code => "code", IrepId::Typecast => "typecast", IrepId::StaticCast => "static_cast", IrepId::DynamicCast => "dynamic_cast", IrepId::ConstCast => "const_cast", IrepId::ReinterpretCast => "reinterpret_cast", IrepId::Index => "index", IrepId::Ptrmember => "ptrmember", IrepId::Member => "member", IrepId::MemberName => "member_name", IrepId::CMemberName => "#member_name", IrepId::Equal => "=", IrepId::Implies => "=>", IrepId::And => "and", IrepId::Nand => "nand", IrepId::Or => "or", IrepId::Nor => "nor", IrepId::Xor => "xor", IrepId::Not => "not", IrepId::Bitand => "bitand", IrepId::Bitor => "bitor", IrepId::Bitnot => "bitnot", IrepId::Bitxor => "bitxor", IrepId::Bitnand => "bitnand", IrepId::Bitnor => "bitnor", IrepId::Bitxnor => "bitxnor", IrepId::Notequal => "notequal", IrepId::If => "if", IrepId::Symbol => "symbol", IrepId::NextSymbol => "next_symbol", IrepId::NondetSymbol => "nondet_symbol", IrepId::PredicateSymbol => "predicate_symbol", IrepId::PredicateNextSymbol => "predicate_next_symbol", IrepId::NondetBool => "nondet_bool", IrepId::Empty => "empty", IrepId::SideEffect => "side_effect", IrepId::Statement => "statement", IrepId::StatementExpression => "statement_expression", IrepId::Value => "value", IrepId::Constant => "constant", IrepId::Block => "block", IrepId::Decl => "decl", IrepId::Dead => "dead", IrepId::Assign => "assign", IrepId::AssignDiv => "assign_div", IrepId::AssignMult => "assign*", IrepId::AssignPlus => "assign+", IrepId::AssignMinus => "assign-", IrepId::AssignMod => "assign_mod", IrepId::AssignShl => "assign_shl", IrepId::AssignShr => "assign_shr", IrepId::AssignAshr => "assign_ashr", IrepId::AssignLshr => "assign_lshr", IrepId::AssignBitand => "assign_bitand", IrepId::AssignBitxor => "assign_bitxor", IrepId::AssignBitor => "assign_bitor", IrepId::Assume => "assume", IrepId::Assert => "assert", IrepId::Assertion => "assertion", IrepId::Precondition => "precondition", IrepId::Postcondition => "postcondition", IrepId::PreconditionInstance => "precondition_instance", IrepId::Goto => "goto", IrepId::GccComputedGoto => "gcc_computed_goto", IrepId::Ifthenelse => "ifthenelse", IrepId::Label => "label", IrepId::Break => "break", IrepId::Continue => "continue", IrepId::FunctionCall => "function_call", IrepId::Return => "return", IrepId::Skip => "skip", IrepId::Arguments => "arguments", IrepId::Array => "array", IrepId::Size => "size", IrepId::FrontendPointer => "frontend_pointer", IrepId::Pointer => "pointer", IrepId::BlockPointer => "block_pointer", IrepId::Switch => "switch", IrepId::SwitchCase => "switch_case", IrepId::GccSwitchCaseRange => "gcc_switch_case_range", IrepId::For => "for", IrepId::While => "while", IrepId::Dowhile => "dowhile", IrepId::Int => "int", IrepId::Integer => "integer", IrepId::Natural => "natural", IrepId::Real => "real", IrepId::Rational => "rational", IrepId::Complex => "complex", IrepId::Signed => "signed", IrepId::Unsigned => "unsigned", IrepId::Asm => "asm", IrepId::GccAsmInput => "gcc_asm_input", IrepId::GccAsmOutput => "gcc_asm_output", IrepId::GccAsmClobberedRegister => "gcc_asm_clobbered_register", IrepId::Incomplete => "incomplete", IrepId::IncompleteClass => "incomplete_class", IrepId::CIncomplete => "#incomplete", IrepId::Identifier => "identifier", IrepId::Name => "name", IrepId::InnerName => "inner_name", IrepId::CppName => "cpp_name", IrepId::ComponentCppName => "component_cpp_name", IrepId::CIdClass => "#id_class", IrepId::Declaration => "declaration", IrepId::DeclarationList => "declaration_list", IrepId::Declarator => "declarator", IrepId::Struct => "struct", IrepId::CBitField => "c_bit_field", IrepId::Union => "union", IrepId::Class => "class", IrepId::MergedType => "merged_type", IrepId::Range => "range", IrepId::From => "from", IrepId::To => "to", IrepId::Module => "module", IrepId::Parameter => "parameter", IrepId::ComponentName => "component_name", IrepId::ComponentNumber => "component_number", IrepId::Tag => "tag", IrepId::Default => "default", IrepId::CDefaultValue => "#default_value", IrepId::BaseName => "base_name", IrepId::CBaseName => "#base_name", IrepId::String => "string", IrepId::CStringConstant => "#string_constant", IrepId::StringConstant => "string_constant", IrepId::Width => "width", IrepId::Components => "components", IrepId::Bv => "bv", IrepId::F => "f", IrepId::With => "with", IrepId::Trans => "trans", IrepId::Throw => "throw", IrepId::TryCatch => "try_catch", IrepId::Noexcept => "noexcept", IrepId::CPROVERThrow => "CPROVER_throw", IrepId::CPROVERTryCatch => "CPROVER_try_catch", IrepId::CPROVERTryFinally => "CPROVER_try_finally", IrepId::Protection => "protection", IrepId::Private => "private", IrepId::Public => "public", IrepId::Protected => "protected", IrepId::Virtual => "virtual", IrepId::Volatile => "volatile", IrepId::Const => "const", IrepId::Constexpr => "constexpr", IrepId::Inline => "inline", IrepId::Forall => "forall", IrepId::Exists => "exists", IrepId::Repeat => "repeat", IrepId::Extractbit => "extractbit", IrepId::Extractbits => "extractbits", IrepId::CReference => "#reference", IrepId::CRvalueReference => "#rvalue_reference", IrepId::True => "true", IrepId::False => "false", IrepId::AddressOf => "address_of", IrepId::Dereference => "dereference", IrepId::CLvalue => "#lvalue", IrepId::CBase => "#base", IrepId::Destination => "destination", IrepId::Main => "main", IrepId::Expression => "expression", IrepId::Allocate => "allocate", IrepId::CCxxAllocType => "#cxx_alloc_type", IrepId::CppNew => "cpp_new", IrepId::CppDelete => "cpp_delete", IrepId::CppNewArray => "cpp_new[]", IrepId::CppDeleteArray => "cpp_delete[]", IrepId::JavaNew => "java_new", IrepId::JavaNewArray => "java_new_array", IrepId::JavaNewArrayData => "java_new_array_data", IrepId::JavaStringLiteral => "java_string_literal", IrepId::Printf => "printf", IrepId::Input => "input", IrepId::Output => "output", IrepId::Nondet => "nondet", IrepId::NULL => "NULL", IrepId::Null => "null", IrepId::Nullptr => "nullptr", IrepId::CEnum => "c_enum", IrepId::Enumeration => "enumeration", IrepId::Elements => "elements", IrepId::Unknown => "unknown", IrepId::Uninitialized => "uninitialized", IrepId::Invalid => "invalid", IrepId::CInvalidObject => "#invalid_object", IrepId::PointerOffset => "pointer_offset", IrepId::PointerObject => "pointer_object", IrepId::IsInvalidPointer => "is_invalid_pointer", IrepId::IeeeFloatEqual => "ieee_float_equal", IrepId::IeeeFloatNotequal => "ieee_float_notequal", IrepId::Isnan => "isnan", IrepId::Lambda => "lambda", IrepId::ArrayComprehension => "array_comprehension", IrepId::ArrayOf => "array_of", IrepId::ArrayEqual => "array_equal", IrepId::ArraySet => "array_set", IrepId::ArrayCopy => "array_copy", IrepId::ArrayList => "array_list", IrepId::Mod => "mod", IrepId::Rem => "rem", IrepId::Shr => "shr", IrepId::Ashr => "ashr", IrepId::Lshr => "lshr", IrepId::Shl => "shl", IrepId::Rol => "rol", IrepId::Ror => "ror", IrepId::Comma => "comma", IrepId::Concatenation => "concatenation", IrepId::Infinity => "infinity", IrepId::ReturnType => "return_type", IrepId::Typedef => "typedef", IrepId::TypedefType => "typedef_type", IrepId::CTypedef => "#typedef", IrepId::Extern => "extern", IrepId::Static => "static", IrepId::Auto => "auto", IrepId::Register => "register", IrepId::ThreadLocal => "thread_local", IrepId::Thread => "thread", IrepId::CThreadLocal => "#thread_local", IrepId::CStaticLifetime => "#static_lifetime", IrepId::Mutable => "mutable", IrepId::Void => "void", IrepId::Int8 => "int8", IrepId::Int16 => "int16", IrepId::Int32 => "int32", IrepId::Int64 => "int64", IrepId::Ptr32 => "ptr32", IrepId::Ptr64 => "ptr64", IrepId::Char => "char", IrepId::Short => "short", IrepId::Long => "long", IrepId::Float => "float", IrepId::Double => "double", IrepId::Byte => "byte", IrepId::Boolean => "boolean", IrepId::LongDouble => "long_double", IrepId::SignedChar => "signed_char", IrepId::UnsignedChar => "unsigned_char", IrepId::SignedInt => "signed_int", IrepId::UnsignedInt => "unsigned_int", IrepId::SignedLongInt => "signed_long_int", IrepId::UnsignedLongInt => "unsigned_long_int", IrepId::SignedShortInt => "signed_short_int", IrepId::UnsignedShortInt => "unsigned_short_int", IrepId::SignedLongLongInt => "signed_long_long_int", IrepId::UnsignedLongLongInt => "unsigned_long_long_int", IrepId::SignedInt128 => "signed_int128", IrepId::UnsignedInt128 => "unsigned_int128", IrepId::Case => "case", IrepId::CInlined => "#inlined", IrepId::CHide => "#hide", IrepId::Hide => "hide", IrepId::Abs => "abs", IrepId::Sign => "sign", IrepId::Access => "access", IrepId::CAccess => "#access", IrepId::Postincrement => "postincrement", IrepId::Postdecrement => "postdecrement", IrepId::Preincrement => "preincrement", IrepId::Predecrement => "predecrement", IrepId::IntegerBits => "integer_bits", IrepId::KnR => "KnR", IrepId::CKnR => "#KnR", IrepId::ConstraintSelectOne => "constraint_select_one", IrepId::Cond => "cond", IrepId::BvLiterals => "bv_literals", IrepId::IsFinite => "isfinite", IrepId::Isinf => "isinf", IrepId::Isnormal => "isnormal", IrepId::Alignof => "alignof", IrepId::ClangBuiltinConvertvector => "clang_builtin_convertvector", IrepId::GccBuiltinVaArg => "gcc_builtin_va_arg", IrepId::GccBuiltinTypesCompatibleP => "gcc_builtin_types_compatible_p", IrepId::VaStart => "va_start", IrepId::GccFloat16 => "gcc_float16", IrepId::GccFloat32 => "gcc_float32", IrepId::GccFloat32x => "gcc_float32x", IrepId::GccFloat64 => "gcc_float64", IrepId::GccFloat64x => "gcc_float64x", IrepId::GccFloat80 => "gcc_float80", IrepId::GccFloat128 => "gcc_float128", IrepId::GccFloat128x => "gcc_float128x", IrepId::GccInt128 => "gcc_int128", IrepId::GccDecimal32 => "gcc_decimal32", IrepId::GccDecimal64 => "gcc_decimal64", IrepId::GccDecimal128 => "gcc_decimal128", IrepId::BuiltinOffsetof => "builtin_offsetof", IrepId::Id0 => "0", IrepId::Id1 => "1", IrepId::Sizeof => "sizeof", IrepId::TypeArg => "type_arg", IrepId::ExprArg => "expr_arg", IrepId::ExpressionList => "expression_list", IrepId::InitializerList => "initializer_list", IrepId::GccConditionalExpression => "gcc_conditional_expression", IrepId::GccLocalLabel => "gcc_local_label", IrepId::Gcc => "gcc", IrepId::Msc => "msc", IrepId::Typeof => "typeof", IrepId::Ellipsis => "ellipsis", IrepId::Flavor => "flavor", IrepId::Ge => ">=", IrepId::Le => "<=", IrepId::Gt => ">", IrepId::Lt => "<", IrepId::Plus => "+", IrepId::Minus => "-", IrepId::UnaryMinus => "unary-", IrepId::UnaryPlus => "unary+", IrepId::Mult => "*", IrepId::Div => "/", IrepId::Power => "**", IrepId::FactorialPower => "factorial_power", IrepId::PrettyName => "pretty_name", IrepId::CClass => "#class", IrepId::CField => "#field", IrepId::CInterface => "#interface", IrepId::DesignatedInitializer => "designated_initializer", IrepId::Designator => "designator", IrepId::MemberDesignator => "member_designator", IrepId::IndexDesignator => "index_designator", IrepId::CConstant => "#constant", IrepId::CVolatile => "#volatile", IrepId::CRestricted => "#restricted", IrepId::CIdentifier => "#identifier", IrepId::CImplicit => "#implicit", IrepId::CPtr32 => "#ptr32", IrepId::CPtr64 => "#ptr64", IrepId::CAtomic => "#atomic", IrepId::Restrict => "restrict", IrepId::ByteExtractBigEndian => "byte_extract_big_endian", IrepId::ByteExtractLittleEndian => "byte_extract_little_endian", IrepId::ByteUpdateBigEndian => "byte_update_big_endian", IrepId::ByteUpdateLittleEndian => "byte_update_little_endian", IrepId::Replication => "replication", IrepId::CproverAtomic => "cprover_atomic", IrepId::Atomic => "atomic", IrepId::AtomicTypeSpecifier => "atomic_type_specifier", IrepId::AtomicBegin => "atomic_begin", IrepId::AtomicEnd => "atomic_end", IrepId::StartThread => "start_thread", IrepId::EndThread => "end_thread", IrepId::CoverageCriterion => "coverage_criterion", IrepId::Initializer => "initializer", IrepId::Anonymous => "anonymous", IrepId::CIsAnonymous => "#is_anonymous", IrepId::IsEnumConstant => "is_enum_constant", IrepId::IsInline => "is_inline", IrepId::IsExtern => "is_extern", IrepId::IsSynchronized => "is_synchronized", IrepId::IsNativeMethod => "is_native_method", IrepId::IsVarargsMethod => "is_varargs_method", IrepId::IsGlobal => "is_global", IrepId::IsThreadLocal => "is_thread_local", IrepId::IsParameter => "is_parameter", IrepId::IsMember => "is_member", IrepId::IsType => "is_type", IrepId::IsRegister => "is_register", IrepId::IsTypedef => "is_typedef", IrepId::IsStatic => "is_static", IrepId::IsTemplate => "is_template", IrepId::IsStaticAssert => "is_static_assert", IrepId::IsVirtual => "is_virtual", IrepId::CIsVirtual => "#is_virtual", IrepId::Literal => "literal", IrepId::MemberInitializers => "member_initializers", IrepId::MemberInitializer => "member_initializer", IrepId::MethodQualifier => "method_qualifier", IrepId::Methods => "methods", IrepId::StaticMembers => "static_members", IrepId::Constructor => "constructor", IrepId::Destructor => "destructor", IrepId::Bases => "bases", IrepId::Base => "base", IrepId::FromBase => "from_base", IrepId::Operator => "operator", IrepId::Template => "template", IrepId::TemplateClassInstance => "template_class_instance", IrepId::TemplateFunctionInstance => "template_function_instance", IrepId::TemplateType => "template_type", IrepId::TemplateArgs => "template_args", IrepId::TemplateParameter => "template_parameter", IrepId::TemplateParameterSymbolType => "template_parameter_symbol_type", IrepId::TemplateParameters => "template_parameters", IrepId::CTemplate => "#template", IrepId::CTemplateArguments => "#template_arguments", IrepId::CTemplateCase => "#template_case", IrepId::Typename => "typename", IrepId::C => "C", IrepId::Cpp => "cpp", IrepId::Java => "java", IrepId::DeclBlock => "decl_block", IrepId::DeclType => "decl_type", IrepId::Parameters => "parameters", IrepId::WcharT => "wchar_t", IrepId::Char16T => "char16_t", IrepId::Char32T => "char32_t", IrepId::SizeT => "size_t", IrepId::SsizeT => "ssize_t", IrepId::Mode => "mode", IrepId::This => "this", IrepId::CThis => "#this", IrepId::ReductionAnd => "reduction_and", IrepId::ReductionOr => "reduction_or", IrepId::ReductionNand => "reduction_nand", IrepId::ReductionNor => "reduction_nor", IrepId::ReductionXor => "reduction_xor", IrepId::ReductionXnor => "reduction_xnor", IrepId::CZeroInitializer => "#zero_initializer", IrepId::Body => "body", IrepId::TemporaryObject => "temporary_object", IrepId::OverflowPlus => "overflow-+", IrepId::OverflowMinus => "overflow--", IrepId::OverflowMult => "overflow-*", IrepId::OverflowResultPlus => "overflow_result-+", IrepId::OverflowResultMinus => "overflow_result--", IrepId::OverflowResultMult => "overflow_result-*", IrepId::OverflowUnaryMinus => "overflow-unary-", IrepId::ObjectDescriptor => "object_descriptor", IrepId::IsDynamicObject => "is_dynamic_object", IrepId::DynamicObject => "dynamic_object", IrepId::CDynamic => "#dynamic", IrepId::ObjectSize => "object_size", IrepId::GoodPointer => "good_pointer", IrepId::IntegerAddress => "integer_address", IrepId::IntegerAddressObject => "integer_address_object", IrepId::NullObject => "NULL-object", IrepId::StaticObject => "static_object", IrepId::StackObject => "stack_object", IrepId::CIsFailedSymbol => "#is_failed_symbol", IrepId::CFailedSymbol => "#failed_symbol", IrepId::Friend => "friend", IrepId::CFriends => "#friends", IrepId::Explicit => "explicit", IrepId::StorageSpec => "storage_spec", IrepId::MemberSpec => "member_spec", IrepId::MscDeclspec => "msc_declspec", IrepId::Packed => "packed", IrepId::CPacked => "#packed", IrepId::TransparentUnion => "transparent_union", IrepId::CTransparentUnion => "#transparent_union", IrepId::Aligned => "aligned", IrepId::CAlignment => "#alignment", IrepId::FrontendVector => "frontend_vector", IrepId::Vector => "vector", IrepId::Abstract => "abstract", IrepId::FunctionApplication => "function_application", IrepId::CppDeclarator => "cpp_declarator", IrepId::CppLinkageSpec => "cpp_linkage_spec", IrepId::CppNamespaceSpec => "cpp_namespace_spec", IrepId::CppStorageSpec => "cpp_storage_spec", IrepId::CppUsing => "cpp_using", IrepId::CppDeclaration => "cpp_declaration", IrepId::CppStaticAssert => "cpp_static_assert", IrepId::CppMemberSpec => "cpp_member_spec", IrepId::CCType => "#c_type", IrepId::Namespace => "namespace", IrepId::Linkage => "linkage", IrepId::Decltype => "decltype", IrepId::CTagOnlyDeclaration => "#tag_only_declaration", IrepId::StructTag => "struct_tag", IrepId::UnionTag => "union_tag", IrepId::CEnumTag => "c_enum_tag", IrepId::VerilogCaseEquality => "verilog_case_equality", IrepId::VerilogCaseInequality => "verilog_case_inequality", IrepId::UserSpecifiedPredicate => "user_specified_predicate", IrepId::UserSpecifiedParameterPredicates => "user_specified_parameter_predicates", IrepId::UserSpecifiedReturnPredicates => "user_specified_return_predicates", IrepId::Unassigned => "unassigned", IrepId::NewObject => "new_object", IrepId::ComplexReal => "complex_real", IrepId::ComplexImag => "complex_imag", IrepId::Imag => "imag", IrepId::MscTryExcept => "msc_try_except", IrepId::MscTryFinally => "msc_try_finally", IrepId::MscLeave => "msc_leave", IrepId::MscUuidof => "msc_uuidof", IrepId::MscIfExists => "msc_if_exists", IrepId::MscIfNotExists => "msc_if_not_exists", IrepId::MscUnderlyingType => "msc_underlying_type", IrepId::MscBased => "msc_based", IrepId::Alias => "alias", IrepId::PtrObject => "ptr_object", IrepId::CCSizeofType => "#c_sizeof_type", IrepId::ArrayUpdate => "array_update", IrepId::Update => "update", IrepId::StaticAssert => "static_assert", IrepId::GccAttributeMode => "gcc_attribute_mode", IrepId::BuiltIn => "", IrepId::ExceptionList => "exception_list", IrepId::ExceptionId => "exception_id", IrepId::PredicatePassiveSymbol => "predicate_passive_symbol", IrepId::CwVaArgTypeof => "cw_va_arg_typeof", IrepId::Fence => "fence", IrepId::Sync => "sync", IrepId::Lwsync => "lwsync", IrepId::Isync => "isync", IrepId::WRfence => "WRfence", IrepId::RRfence => "RRfence", IrepId::RWfence => "RWfence", IrepId::WWfence => "WWfence", IrepId::RRcumul => "RRcumul", IrepId::RWcumul => "RWcumul", IrepId::WWcumul => "WWcumul", IrepId::WRcumul => "WRcumul", IrepId::GenericSelection => "generic_selection", IrepId::GenericAssociations => "generic_associations", IrepId::GenericAssociation => "generic_association", IrepId::FloatbvPlus => "floatbv_plus", IrepId::FloatbvMinus => "floatbv_minus", IrepId::FloatbvMult => "floatbv_mult", IrepId::FloatbvDiv => "floatbv_div", IrepId::FloatbvRem => "floatbv_rem", IrepId::FloatbvTypecast => "floatbv_typecast", IrepId::CompoundLiteral => "compound_literal", IrepId::CustomBv => "custom_bv", IrepId::CustomUnsignedbv => "custom_unsignedbv", IrepId::CustomSignedbv => "custom_signedbv", IrepId::CustomFixedbv => "custom_fixedbv", IrepId::CustomFloatbv => "custom_floatbv", IrepId::CSSASymbol => "#SSA_symbol", IrepId::L0 => "L0", IrepId::L1 => "L1", IrepId::L2 => "L2", IrepId::L1ObjectIdentifier => "L1_object_identifier", IrepId::AlreadyTypechecked => "already_typechecked", IrepId::CVaArgType => "#va_arg_type", IrepId::Smt2Symbol => "smt2_symbol", IrepId::Onehot => "onehot", IrepId::Onehot0 => "onehot0", IrepId::Popcount => "popcount", IrepId::CountLeadingZeros => "count_leading_zeros", IrepId::CountTrailingZeros => "count_trailing_zeros", IrepId::EmptyUnion => "empty_union", IrepId::FunctionType => "function_type", IrepId::Noreturn => "noreturn", IrepId::CNoreturn => "#noreturn", IrepId::Weak => "weak", IrepId::IsWeak => "is_weak", IrepId::Used => "used", IrepId::IsUsed => "is_used", IrepId::CSpecLoopInvariant => "#spec_loop_invariant", IrepId::CSpecRequires => "#spec_requires", IrepId::CSpecEnsures => "#spec_ensures", IrepId::VirtualFunction => "virtual_function", IrepId::ElementType => "element_type", IrepId::WorkingDirectory => "working_directory", IrepId::Section => "section", IrepId::Bswap => "bswap", IrepId::BitReverse => "bitreverse", IrepId::JavaBytecodeIndex => "java_bytecode_index", IrepId::JavaInstanceof => "java_instanceof", IrepId::JavaSuperMethodCall => "java_super_method_call", IrepId::JavaEnumStaticUnwind => "java_enum_static_unwind", IrepId::PushCatch => "push_catch", IrepId::PopCatch => "pop_catch", IrepId::ExceptionLandingpad => "exception_landingpad", IrepId::LengthUpperBound => "length_upper_bound", IrepId::CproverAssociateArrayToPointerFunc => "cprover_associate_array_to_pointer_func", IrepId::CproverAssociateLengthToArrayFunc => "cprover_associate_length_to_array_func", IrepId::CproverCharLiteralFunc => "cprover_char_literal_func", IrepId::CproverStringLiteralFunc => "cprover_string_literal_func", IrepId::CproverStringCharAtFunc => "cprover_string_char_at_func", IrepId::CproverStringCharSetFunc => "cprover_string_char_set_func", IrepId::CproverStringCodePointAtFunc => "cprover_string_code_point_at_func", IrepId::CproverStringCodePointBeforeFunc => "cprover_string_code_point_before_func", IrepId::CproverStringCodePointCountFunc => "cprover_string_code_point_count_func", IrepId::CproverStringOffsetByCodePointFunc => { "cprover_string_offset_by_code_point_func" } IrepId::CproverStringCompareToFunc => "cprover_string_compare_to_func", IrepId::CproverStringConcatFunc => "cprover_string_concat_func", IrepId::CproverStringConcatCharFunc => "cprover_string_concat_char_func", IrepId::CproverStringConcatCodePointFunc => "cprover_string_concat_code_point_func", IrepId::CproverStringConstrainCharactersFunc => { "cprover_string_constrain_characters_func" } IrepId::CproverStringContainsFunc => "cprover_string_contains_func", IrepId::CproverStringCopyFunc => "cprover_string_copy_func", IrepId::CproverStringDeleteFunc => "cprover_string_delete_func", IrepId::CproverStringDeleteCharAtFunc => "cprover_string_delete_char_at_func", IrepId::CproverStringEqualFunc => "cprover_string_equal_func", IrepId::CproverStringEqualsIgnoreCaseFunc => "cprover_string_equals_ignore_case_func", IrepId::CproverStringEmptyStringFunc => "cprover_string_empty_string_func", IrepId::CproverStringEndswithFunc => "cprover_string_endswith_func", IrepId::CproverStringFormatFunc => "cprover_string_format_func", IrepId::CproverStringIndexOfFunc => "cprover_string_index_of_func", IrepId::CproverStringInsertFunc => "cprover_string_insert_func", IrepId::CproverStringIsPrefixFunc => "cprover_string_is_prefix_func", IrepId::CproverStringIsSuffixFunc => "cprover_string_is_suffix_func", IrepId::CproverStringIsEmptyFunc => "cprover_string_is_empty_func", IrepId::CproverStringLastIndexOfFunc => "cprover_string_last_index_of_func", IrepId::CproverStringLengthFunc => "cprover_string_length_func", IrepId::CproverStringOfIntFunc => "cprover_string_of_int_func", IrepId::CproverStringOfIntHexFunc => "cprover_string_of_int_hex_func", IrepId::CproverStringOfLongFunc => "cprover_string_of_long_func", IrepId::CproverStringOfFloatFunc => "cprover_string_of_float_func", IrepId::CproverStringOfFloatScientificNotationFunc => { "cprover_string_of_float_scientific_notation_func" } IrepId::CproverStringOfDoubleFunc => "cprover_string_of_double_func", IrepId::CproverStringParseIntFunc => "cprover_string_parse_int_func", IrepId::CproverStringIsValidIntFunc => "cprover_string_is_valid_int_func", IrepId::CproverStringIsValidLongFunc => "cprover_string_is_valid_long_func", IrepId::CproverStringReplaceFunc => "cprover_string_replace_func", IrepId::CproverStringSetLengthFunc => "cprover_string_set_length_func", IrepId::CproverStringStartswithFunc => "cprover_string_startswith_func", IrepId::CproverStringSubstringFunc => "cprover_string_substring_func", IrepId::CproverStringToLowerCaseFunc => "cprover_string_to_lower_case_func", IrepId::CproverStringToUpperCaseFunc => "cprover_string_to_upper_case_func", IrepId::CproverStringTrimFunc => "cprover_string_trim_func", IrepId::SkipInitialize => "skip_initialize", IrepId::BasicBlockCoveredLines => "basic_block_covered_lines", IrepId::BasicBlockSourceLines => "basic_block_source_lines", IrepId::IsNondetNullable => "is_nondet_nullable", IrepId::ArrayReplace => "array_replace", IrepId::SwitchCaseNumber => "switch_case_number", IrepId::JavaArrayAccess => "java_array_access", IrepId::JavaMemberAccess => "java_member_access", IrepId::CJavaGenericParameter => "#java_generic_parameter", IrepId::CJavaGenericsClassType => "#java_generics_class_type", IrepId::CJavaImplicitlyGenericClassType => "#java_implicitly_generic_class_type", IrepId::CJavaGenericSymbol => "#java_generic_symbol", IrepId::GenericTypes => "generic_types", IrepId::ImplicitGenericTypes => "#implicit_generic_types", IrepId::TypeVariables => "type_variables", IrepId::HandleType => "handle_type", IrepId::JavaLambdaMethodHandle => "java_lambda_method_handle", IrepId::JavaLambdaMethodHandleIndex => "lambda_method_handle_index", IrepId::JavaLambdaMethodHandles => "lambda_method_handles", IrepId::HavocObject => "havoc_object", IrepId::OverflowShl => "overflow-shl", IrepId::CNoInitializationRequired => "#no_initialization_required", IrepId::CNoNondetInitialization => "#no_nondet_initialization", IrepId::OverlayClass => "java::org.cprover.OverlayClassImplementation", IrepId::OverlayMethod => "java::org.cprover.OverlayMethodImplementation", IrepId::IgnoredMethod => "java::org.cprover.IgnoredMethodImplementation", IrepId::IsAnnotation => "is_annotation", IrepId::CAnnotations => "#annotations", IrepId::Final => "final", IrepId::BitsPerByte => "bits_per_byte", IrepId::CAbstract => "#abstract", IrepId::Synthetic => "synthetic", IrepId::Interface => "interface", IrepId::CMustNotThrow => "#must_not_throw", IrepId::IsInnerClass => "is_inner_class", IrepId::IsAnonymous => "is_anonymous", IrepId::OuterClass => "outer_class", IrepId::IsBridgeMethod => "is_bridge_method", IrepId::CIsOperator => "#is_operator", IrepId::CNotAccessible => "#not_accessible", IrepId::COverrideConstantness => "#override_constantness", IrepId::CBound => "#bound", IrepId::CBoundsCheck => "#bounds_check", IrepId::CIsStatic => "#is_static", IrepId::CCallByValue => "#call_by_value", IrepId::CVirtualName => "#virtual_name", IrepId::CUnnamedObject => "#unnamed_object", IrepId::CTemporaryAvoided => "#temporary_avoided", IrepId::CQualifier => "#qualifier", IrepId::CArrayIni => "#array_ini", IrepId::ROk => "r_ok", IrepId::WOk => "w_ok", IrepId::SuperClass => "super_class", IrepId::ExceptionsThrownList => "exceptions_thrown_list", IrepId::CJavaMethodType => "#java_method_type", IrepId::Compiled => "compiled", IrepId::PartialSpecializationArgs => "partial_specialization_args", IrepId::SpecializationOf => "specialization_of", IrepId::InitArgs => "init_args", IrepId::Ambiguous => "ambiguous", IrepId::SpecializationTemplateArgs => "specialization_template_args", IrepId::FullTemplateArgs => "full_template_args", IrepId::InstantiatedWith => "instantiated_with", IrepId::TemplateMethods => "template_methods", IrepId::CppNotTypechecked => "cpp_not_typechecked", IrepId::Noaccess => "noaccess", IrepId::IsOperator => "is_operator", IrepId::IsCastOperator => "is_cast_operator", IrepId::IsExplicit => "is_explicit", IrepId::IsMutable => "is_mutable", IrepId::VirtualName => "virtual_name", IrepId::IsPureVirtual => "is_pure_virtual", IrepId::IsVtptr => "is_vtptr", IrepId::Prefix => "prefix", IrepId::Cv => "cv", IrepId::CppDummyDestructor => "cpp_dummy_destructor", IrepId::CastExpression => "cast_expression", IrepId::PodConstructor => "pod_constructor", IrepId::TemplateDecls => "template_decls", IrepId::ThrowDecl => "throw_decl", IrepId::Typeid => "typeid", IrepId::CQuoted => "#quoted", IrepId::ToMember => "to_member", IrepId::PointerToMember => "pointer_to_member", IrepId::Tuple => "tuple", IrepId::FunctionBody => "function_body", IrepId::GetMay => "get_may", IrepId::SetMay => "set_may", IrepId::ClearMay => "clear_may", IrepId::GetMust => "get_must", IrepId::SetMust => "set_must", IrepId::ClearMust => "clear_must", IrepId::Pragma => "pragma", IrepId::StatementList => "Statement List", IrepId::StatementListType => "statement_list_type", IrepId::StatementListFunction => "statement_list_function", IrepId::StatementListFunctionBlock => "statement_list_function_block", IrepId::StatementListMainFunction => "Main", IrepId::StatementListDataBlock => "statement_list_data_block", IrepId::StatementListVersion => "statement_list_version", IrepId::StatementListVarInput => "statement_list_var_input", IrepId::StatementListVarInout => "statement_list_var_inout", IrepId::StatementListVarOutput => "statement_list_var_output", IrepId::StatementListVarConstant => "statement_list_var_constant", IrepId::StatementListVarTemp => "statement_list_var_temp", IrepId::StatementListVarStatic => "statement_list_var_static", IrepId::StatementListReturn => "statement_list_return", IrepId::StatementListReturnValueId => "Ret_Val", IrepId::StatementListVarEntry => "statement_list_var_entry", IrepId::StatementListVarDecls => "statement_list_var_decls", IrepId::StatementListNetwork => "statement_list_network", IrepId::StatementListNetworks => "statement_list_networks", IrepId::StatementListTitle => "statement_list_title", IrepId::StatementListIdentifier => "statement_list_identifier", IrepId::StatementListLoad => "statement_list_load", IrepId::StatementListTransfer => "statement_list_transfer", IrepId::StatementListCall => "statement_list_call", IrepId::StatementListNop => "statement_list_nop", IrepId::StatementListConstAdd => "statement_list_const_add", IrepId::StatementListAccuIntAdd => "statement_list_accu_int_add", IrepId::StatementListAccuIntSub => "statement_list_accu_int_sub", IrepId::StatementListAccuIntMul => "statement_list_accu_int_mul", IrepId::StatementListAccuIntDiv => "statement_list_accu_int_div", IrepId::StatementListAccuIntEq => "statement_list_accu_int_eq", IrepId::StatementListAccuIntNeq => "statement_list_accu_int_neq", IrepId::StatementListAccuIntGt => "statement_list_accu_int_gt", IrepId::StatementListAccuIntLt => "statement_list_accu_int_lt", IrepId::StatementListAccuIntGte => "statement_list_accu_int_gte", IrepId::StatementListAccuIntLte => "statement_list_accu_int_lte", IrepId::StatementListAccuRealAdd => "statement_list_accu_real_add", IrepId::StatementListAccuRealSub => "statement_list_accu_real_sub", IrepId::StatementListAccuRealMul => "statement_list_accu_real_mul", IrepId::StatementListAccuRealDiv => "statement_list_accu_real_div", IrepId::StatementListAccuRealEq => "statement_list_accu_real_eq", IrepId::StatementListAccuRealNeq => "statement_list_accu_real_neq", IrepId::StatementListAccuRealGt => "statement_list_accu_real_gt", IrepId::StatementListAccuRealLt => "statement_list_accu_real_lt", IrepId::StatementListAccuRealGte => "statement_list_accu_real_gte", IrepId::StatementListAccuRealLte => "statement_list_accu_real_lte", IrepId::StatementListAccuDintAdd => "statement_list_accu_dint_add", IrepId::StatementListAccuDintSub => "statement_list_accu_dint_sub", IrepId::StatementListAccuDintMul => "statement_list_accu_dint_mul", IrepId::StatementListAccuDintDiv => "statement_list_accu_dint_div", IrepId::StatementListAccuDintEq => "statement_list_accu_dint_eq", IrepId::StatementListAccuDintNeq => "statement_list_accu_dint_neq", IrepId::StatementListAccuDintGt => "statement_list_accu_dint_gt", IrepId::StatementListAccuDintLt => "statement_list_accu_dint_lt", IrepId::StatementListAccuDintGte => "statement_list_accu_dint_gte", IrepId::StatementListAccuDintLte => "statement_list_accu_dint_lte", IrepId::StatementListAnd => "statement_list_and", IrepId::StatementListAndNot => "statement_list_and_not", IrepId::StatementListOr => "statement_list_or", IrepId::StatementListOrNot => "statement_list_or_not", IrepId::StatementListXor => "statement_list_xor", IrepId::StatementListXorNot => "statement_list_xor_not", IrepId::StatementListAndNested => "statement_list_and_nested", IrepId::StatementListAndNotNested => "statement_list_and_not_nested", IrepId::StatementListOrNested => "statement_list_or_nested", IrepId::StatementListOrNotNested => "statement_list_or_not_nested", IrepId::StatementListXorNested => "statement_list_xor_nested", IrepId::StatementListXorNotNested => "statement_list_xor_not_nested", IrepId::StatementListNestingClosed => "statement_list_nesting_closed", IrepId::StatementListAssign => "statement_list_assign", IrepId::StatementListSetRlo => "statement_list_set_rlo", IrepId::StatementListClrRlo => "statement_list_clr_rlo", IrepId::StatementListSet => "statement_list_set", IrepId::StatementListReset => "statement_list_reset", IrepId::StatementListNot => "statement_list_not", IrepId::StatementListInstruction => "statement_list_instruction", IrepId::StatementListInstructions => "statement_list_instructions", IrepId::VectorEqual => "vector-=", IrepId::VectorNotequal => "vector-!=", IrepId::VectorGe => "vector->=", IrepId::VectorLe => "vector-<=", IrepId::VectorGt => "vector->", IrepId::VectorLt => "vector-<", }; s.to_string() } } #[cfg(test)] mod tests { use crate::irep::IrepId; // #[test] // #[should_panic] // fn test_hex_id_panic1() { // IrepId::hex_from_int(-127, 7, true); // } // #[test] // #[should_panic] // fn test_hex_id_panic2() { // IrepId::hex_from_int(12, 4, true); // } // #[test] // #[should_panic] // fn test_hex_id_panic3() { // IrepId::hex_from_int(-12, 4, true); // } // #[test] // #[should_panic] // fn test_hex_id_panic_string1() { // IrepId::FreeformHexInteger { value: BigInt::from(-127), width: 7, signed: true } // .to_string(); // } // #[test] // #[should_panic] // fn test_hex_id_panic_string2() { // IrepId::FreeformHexInteger { value: BigInt::from(12), width: 4, signed: true }.to_string(); // } // #[test] // #[should_panic] // fn test_hex_id_panic_string3() { // IrepId::FreeformHexInteger { value: BigInt::from(-12), width: 4, signed: true }.to_string(); // } #[test] fn test_hex_id() { // For positive numbers, should just give the smallest representation. // No need to zero pad. // https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424 assert_eq!(IrepId::bitpattern_from_int(0, 4, true).to_string(), "0"); assert_eq!(IrepId::bitpattern_from_int(12, 5, true).to_string(), "C"); assert_eq!(IrepId::bitpattern_from_int(12, 32, true).to_string(), "C"); assert_eq!(IrepId::bitpattern_from_int(234, 16, true).to_string(), "EA"); assert_eq!(IrepId::bitpattern_from_int(234, 32, true).to_string(), "EA"); // For positive numbers, signed and unsigned should produce the same value assert_eq!(IrepId::bitpattern_from_int(0, 4, false).to_string(), "0"); assert_eq!(IrepId::bitpattern_from_int(12, 4, false).to_string(), "C"); assert_eq!(IrepId::bitpattern_from_int(12, 32, false).to_string(), "C"); assert_eq!(IrepId::bitpattern_from_int(234, 16, false).to_string(), "EA"); assert_eq!(IrepId::bitpattern_from_int(234, 32, false).to_string(), "EA"); // // For negative numbers, should convert to 2s complement of `width` bits, then print hex. assert_eq!(IrepId::bitpattern_from_int(-1, 2, true).to_string(), "3"); assert_eq!(IrepId::bitpattern_from_int(-1, 3, true).to_string(), "7"); assert_eq!(IrepId::bitpattern_from_int(-1, 4, true).to_string(), "F"); assert_eq!(IrepId::bitpattern_from_int(-1, 8, true).to_string(), "FF"); assert_eq!(IrepId::bitpattern_from_int(-1, 9, true).to_string(), "1FF"); assert_eq!(IrepId::bitpattern_from_int(-1, 16, true).to_string(), "FFFF"); assert_eq!(IrepId::bitpattern_from_int(-1, 32, true).to_string(), "FFFFFFFF"); assert_eq!(IrepId::bitpattern_from_int(-12, 5, true).to_string(), "14"); assert_eq!(IrepId::bitpattern_from_int(-12, 6, true).to_string(), "34"); assert_eq!(IrepId::bitpattern_from_int(-12, 7, true).to_string(), "74"); assert_eq!(IrepId::bitpattern_from_int(-12, 8, true).to_string(), "F4"); assert_eq!(IrepId::bitpattern_from_int(-12, 32, true).to_string(), "FFFFFFF4"); assert_eq!(IrepId::bitpattern_from_int(-127, 8, true).to_string(), "81"); assert_eq!(IrepId::bitpattern_from_int(-127, 9, true).to_string(), "181"); assert_eq!(IrepId::bitpattern_from_int(-127, 10, true).to_string(), "381"); assert_eq!(IrepId::bitpattern_from_int(-127, 11, true).to_string(), "781"); assert_eq!(IrepId::bitpattern_from_int(-127, 12, true).to_string(), "F81"); assert_eq!(IrepId::bitpattern_from_int(-127, 36, true).to_string(), "FFFFFFF81"); assert_eq!(IrepId::bitpattern_from_int(-255, 9, true).to_string(), "101"); assert_eq!(IrepId::bitpattern_from_int(-255, 32, true).to_string(), "FFFFFF01"); } }