Session Voblint_Framework

Theories

• TD.Basics_side
• TD.Destabilization_side
• TD.TD_side
• TD.Warrowing
• TD.Update_rules
• TD.TD_side_upd_rule
• TD.TD_side_Interface
• Voblint_Solver.TD_Solver_Bridge
• Voblint_Solver.Globals_Rule
• CFG_Enumeration
• Voblint_Domain.Abstract_Domain
• Voblint_Domain.State_Concretization
• DG_State
• Voblint_Solver.Strategy_Tree_Program
• Voblint_Solver.Strategy_Program_Fold
• DG_Constraint_Programs
• Voblint_Domain.Query_Lift
• Voblint_Domain.Sign_Lattice
• Voblint_Domain.Interval_Lattice
• Voblint_Domain.Parity_Lattice
• Voblint_Domain.Congruence_Lattice
• Voblint_Domain.Int_Lattice
• Analysis_Query
• DG_Manager
• DG_Spec
• DG_Spec_Sound
• Voblint_Domain.Nonrelational_State
• Transfer_Algebra
• Voblint_Domain.Reachability_Lift
• State_Restriction
• MCP_Spec
• Voblint_Domain.Nonrelational_Reachability
• DG_Local_State_Spec
• DG_Ownership_Split_Spec
• Voblint_Solver.Strategy_Tree_Side_Buffering
• DG_Indexed_Generator
• Routed_Call_Programs
• DG_Ctx_Activation
• Activation_Backbone
• Routed_Context
• Routed_Context_Unit
• DG_Reader_Transport
• DG_Keyed_Split_Spec
• Local_Spec_Product
• Channel_Wrappers
• Call_String_Context
• Solved_Table
• Checks
• Check_Result
• Voblint_Domain.Numeric_Queries
• Voblint_Domain.Forward_Domain
• Voblint_Domain.Three_Valued
• Abstract_Checks
• Check_Report
• Contextual_Check_Report
• Check_Answer
• DG_Analysis_Adapter
• Routed_Analysis_Sound