Table of Contents - bam-bam-boogieman-1.0.10 Documentation
Pages
- lexer.rex
- parser.racc
- df_async_removal.rb.old
- eqr_sequentialization.rb.old
- flat_sequentialization.rb.old
- static_segments.rb.old
- violin.rb.old
- model_parser.racc
- model_parser.rex
Classes and Modules
- BAM
- BoogieLanguage
- BoogieLanguage::ScanError
- Bpl
- Bpl::AST
- Bpl::AST::ArithmeticNegation
- Bpl::AST::AssertStatement
- Bpl::AST::AssignStatement
- Bpl::AST::AssumeStatement
- Bpl::AST::Attribute
- Bpl::AST::AxiomDeclaration
- Bpl::AST::BinaryExpression
- Bpl::AST::Binding
- Bpl::AST::BitvectorExtract
- Bpl::AST::BitvectorLiteral
- Bpl::AST::BitvectorType
- Bpl::AST::Block
- Bpl::AST::Body
- Bpl::AST::BooleanLiteral
- Bpl::AST::BreakStatement
- Bpl::AST::CallStatement
- Bpl::AST::CodeExpression
- Bpl::AST::ConstantDeclaration
- Bpl::AST::CustomType
- Bpl::AST::Declaration
- Bpl::AST::EnsuresClause
- Bpl::AST::Expression
- Bpl::AST::FunctionApplication
- Bpl::AST::FunctionDeclaration
- Bpl::AST::FunctionIdentifier
- Bpl::AST::GotoStatement
- Bpl::AST::HavocStatement
- Bpl::AST::Identifier
- Bpl::AST::IfExpression
- Bpl::AST::IfStatement
- Bpl::AST::ImplementationDeclaration
- Bpl::AST::IntegerLiteral
- Bpl::AST::LabelIdentifier
- Bpl::AST::Literal
- Bpl::AST::LogicalNegation
- Bpl::AST::LoopInvariant
- Bpl::AST::MapSelect
- Bpl::AST::MapType
- Bpl::AST::MapUpdate
- Bpl::AST::ModifiesClause
- Bpl::AST::Node
- Bpl::AST::OldExpression
- Bpl::AST::Printing
- Bpl::AST::ProcedureDeclaration
- Bpl::AST::ProcedureIdentifier
- Bpl::AST::Program
- Bpl::AST::QuantifiedExpression
- Bpl::AST::RequiresClause
- Bpl::AST::ReturnStatement
- Bpl::AST::Scope
- Bpl::AST::Specification
- Bpl::AST::Statement
- Bpl::AST::StorageDeclaration
- Bpl::AST::StorageIdentifier
- Bpl::AST::Token
- Bpl::AST::Trace
- Bpl::AST::Trigger
- Bpl::AST::Type
- Bpl::AST::TypeDeclaration
- Bpl::AST::UnaryExpression
- Bpl::AST::VariableDeclaration
- Bpl::AST::WhileStatement
- Bpl::Abstraction
- Bpl::AssertionLocalization
- Bpl::AtomicAnnotation
- Bpl::Atomicity
- Bpl::CallGraphConstruction
- Bpl::CfgConstruction
- Bpl::ConditionalIdentification
- Bpl::CostModeling
- Bpl::CtAnnotation
- Bpl::DefinitionLocalization
- Bpl::Domination
- Bpl::EntrypointAnnotation
- Bpl::EntrypointLocalization
- Bpl::Extraction
- Bpl::Inlining
- Bpl::Liveness
- Bpl::LoopIdentification
- Bpl::Modification
- Bpl::ModifiesCorrection
- Bpl::Normalization
- Bpl::Pass
- Bpl::Preemption
- Bpl::Pruning
- Bpl::Reading
- Bpl::Resolution
- Bpl::Selection
- Bpl::Shadowing
- Bpl::Simplification
- Bpl::Sorting
- Bpl::Splitting
- Bpl::TypeChecking
- Bpl::UnreachableBlockElimination
- Bpl::Unrolling
- Bpl::Unstructuring
- Bpl::Verification
- Bpl::Writing
- Kernel
- Object
- String
- Symbol
- Z3
- Z3::Model
- Z3::ModelParser
- Z3::ModelParser::ScanError
Methods
- ::braces — Bpl::AST::Printing
- ::children — Bpl::AST::Node
- ::depends — Bpl::Pass
- ::flag — Bpl::Pass
- ::flags — Bpl::Pass
- ::indent — Bpl::AST::Printing
- ::inherited — Bpl::AST::Node
- ::inherited — Bpl::Pass
- ::invalidates — Bpl::Pass
- ::new — Bpl::AST::Node
- ::new — Bpl::AST::Token
- ::new — Bpl::AST::Trace
- ::new — Bpl::Pass
- ::new — Z3::Model
- ::notify — Bpl::AST::Binding
- ::notify — Bpl::AST::Scope
- ::observers — Bpl::AST::Node
- ::option — Bpl::Pass
- ::options — Bpl::Pass
- ::process_source_file — BAM
- ::result — Bpl::Pass
- ::sanity_check — Bpl::Normalization
- ::stmt_modifies — Bpl::Modification
- ::switch — Bpl::Pass
- ::uniq_starts_and_ends! — Bpl::Normalization
- #_next_token — BoogieLanguage
- #_reduce_none — BoogieLanguage
- #_reduce_none — Z3::ModelParser
- #abort — Kernel
- #abstract — Bpl::AST::FunctionDeclaration
- #abstract — Bpl::AST::AxiomDeclaration
- #abstract — Bpl::AST::VariableDeclaration
- #abstract — Bpl::AST::ProcedureDeclaration
- #abstract — Bpl::AST::Node
- #abstract — Bpl::AST::AssertStatement
- #abstract — Bpl::AST::AssumeStatement
- #abstract — Bpl::AST::AssignStatement
- #abstract — Bpl::AST::CallStatement
- #abstract — Bpl::AST::Block
- #abstractions — Bpl::AST::Node
- #accesses — Bpl::Shadowing
- #action — BoogieLanguage
- #action — Z3::ModelParser
- #add_assertion! — Bpl::Shadowing
- #add_assertions! — Bpl::Shadowing
- #add_attribute — Bpl::AST::Node
- #add_def — Bpl::DefinitionLocalization
- #add_inline_annotations! — Bpl::Verification
- #add_loop_invariants! — Bpl::Shadowing
- #add_shadow_variables! — Bpl::Shadowing
- #added — Bpl::Pass
- #annotate_function_body! — Bpl::CostModeling
- #annotated_specifications — Bpl::Shadowing
- #append_children — Bpl::AST::Node
- #bind — Bpl::AST::Binding
- #bindings — Bpl::AST::Declaration
- #blue — String
- #bold — String
- #boogie — Kernel
- #bpl — Kernel
- #bpl_assert — Bpl::Shadowing
- #bpl_expr — Kernel
- #bpl_type — Kernel
- #classify — String
- #collect_map_values! — Z3::Model
- #command_line_options — Object
- #comment — String
- #cond — Bpl::Unstructuring
- #constants — Z3::Model
- #copy — Bpl::AST::Node
- #copy — Bpl::AST::Block
- #cost_of — Bpl::CostModeling
- #create_wrapper_block — Bpl::Shadowing
- #cross_product — Bpl::Shadowing
- #cross_product_block! — Bpl::Shadowing
- #declaration — Bpl::AST::Binding
- #declarations — Bpl::AST::FunctionDeclaration
- #declarations — Bpl::AST::ProcedureDeclaration
- #declarations — Bpl::AST::QuantifiedExpression
- #declarations — Bpl::AST::IfStatement
- #declarations — Bpl::AST::WhileStatement
- #declarations — Bpl::AST::Body
- #default_entrypoint? — Bpl::EntrypointLocalization
- #defined — Bpl::Liveness
- #dependent_variables — Bpl::Shadowing
- #dominators — Bpl::ConditionalIdentification
- #each — Bpl::AST::Node
- #each_abstraction — Bpl::Abstraction
- #each_ancestor — Bpl::AST::Node
- #each_child — Bpl::AST::Node
- #enumerate — Bpl::AST::Node
- #enumerate_ancestors — Bpl::AST::Node
- #enumerate_children — Bpl::AST::Node
- #eql? — Bpl::AST::BooleanLiteral
- #eql? — Bpl::AST::IntegerLiteral
- #eql? — Bpl::AST::BitvectorLiteral
- #eql? — Bpl::AST::FunctionApplication
- #eql? — Bpl::AST::UnaryExpression
- #eql? — Bpl::AST::BinaryExpression
- #eql? — Bpl::AST::IfExpression
- #eql? — Bpl::AST::CodeExpression
- #eql? — Bpl::AST::MapSelect
- #eql? — Bpl::AST::MapUpdate
- #eql? — Bpl::AST::BitvectorExtract
- #eql? — Bpl::AST::QuantifiedExpression
- #eql? — Bpl::AST::Trigger
- #exempt? — Bpl::CostModeling
- #exempt? — Bpl::Shadowing
- #exists_path? — Bpl::UnreachableBlockElimination
- #exit? — Bpl::ConditionalIdentification
- #expand — Bpl::AST::Type
- #expand — Bpl::AST::CustomType
- #expand — Bpl::AST::MapType
- #external? — Bpl::ConditionalIdentification
- #extract — Bpl::Extraction
- #extract_branches — Bpl::CostModeling
- #extract_control_blocks — Bpl::CostModeling
- #file_switch? — Object
- #first? — Bpl::Writing
- #flatten — Bpl::AST::StorageDeclaration
- #fmt — String
- #forall? — Bpl::AST::CallStatement
- #fresh_from — Bpl::AST::Body
- #fresh_id — Bpl::Extraction
- #fresh_id — Bpl::Unstructuring
- #fresh_label — Bpl::AST::ProcedureDeclaration
- #fresh_label — Bpl::AST::Body
- #fresh_var — Bpl::AST::ProcedureDeclaration
- #fresh_var — Bpl::AST::Program
- #fresh_var — Bpl::AST::Body
- #full_self_composition — Bpl::Shadowing
- #functions — Z3::Model
- #get_annotation_value — Bpl::CostModeling
- #get_attribute — Bpl::AST::Node
- #get_block — Object
- #get_proc — Object
- #global_variables — Bpl::AST::Program
- #green — String
- #has_annotation? — Bpl::CostModeling
- #has_attribute? — Bpl::AST::Node
- #has_yield? — Bpl::Atomicity
- #hilite — String
- #hilite — Symbol
- #hilite — Bpl::AST::Identifier
- #hilite — Bpl::AST::FunctionApplication
- #hilite — Bpl::AST::Node
- #hilite — Bpl::AST::CustomType
- #hyphenate — String
- #id — Bpl::AST::Block
- #ident — Bpl::AST::Identifier
- #ident — Bpl::AST::MapSelect
- #ident_pattern — Z3::Model
- #idents — Bpl::AST::StorageDeclaration
- #indent — String
- #info — Kernel
- #insert_after — Bpl::AST::Node
- #insert_before — Bpl::AST::Node
- #insert_children — Bpl::AST::Node
- #insert_siblings — Bpl::AST::Node
- #insert_user_leakage! — Bpl::CostModeling
- #inspect — Bpl::AST::Node
- #invalidates — Bpl::Pass
- #is_annotation_stmt? — Bpl::CostModeling
- #is_global? — Bpl::AST::Identifier
- #is_variable? — Bpl::AST::Identifier
- #light_black — String
- #link — Bpl::AST::Node
- #load_file — BoogieLanguage
- #load_file — Z3::ModelParser
- #loads — Bpl::Shadowing
- #locate_child — Bpl::AST::Node
- #lookup — Z3::Model
- #lookup_table — Bpl::AST::Scope
- #loop? — Bpl::ConditionalIdentification
- #magic? — Bpl::Shadowing
- #modifies — Bpl::AST::ProcedureDeclaration
- #name — Bpl::AST::Block
- #names — Bpl::AST::Declaration
- #next_sibling — Bpl::AST::Node
- #next_token — BoogieLanguage
- #next_token — Z3::ModelParser
- #nounify — String
- #old_abort — Kernel
- #order — Bpl::Sorting
- #parse_args — Bpl::Shadowing
- #prepare_for_boogie_fi! — Bpl::Verification
- #prepare_for_boogie_si! — Bpl::Verification
- #prepend_children — Bpl::AST::Node
- #previous_sibling — Bpl::AST::Node
- #readonly_variable? — Bpl::Simplification
- #red — String
- #redirect_to_stub! — Bpl::CostModeling
- #redo! — Bpl::Pass
- #redo? — Bpl::Pass
- #remove — Bpl::AST::Node
- #remove_attribute — Bpl::AST::Node
- #remove_call! — Bpl::Shadowing
- #removed — Bpl::Pass
- #replace_children — Bpl::AST::Node
- #replace_with — Bpl::AST::Node
- #resolve — Z3::Model
- #resolve — Bpl::AST::Scope
- #resolve! — Z3::Model
- #run! — Bpl::Pass
- #run! — Bpl::AssertionLocalization
- #run! — Bpl::CallGraphConstruction
- #run! — Bpl::CfgConstruction
- #run! — Bpl::ConditionalIdentification
- #run! — Bpl::DefinitionLocalization
- #run! — Bpl::Domination
- #run! — Bpl::EntrypointLocalization
- #run! — Bpl::Liveness
- #run! — Bpl::LoopIdentification
- #run! — Bpl::Modification
- #run! — Bpl::Resolution
- #run! — Bpl::TypeChecking
- #run! — Bpl::EntrypointAnnotation
- #run! — Bpl::ModifiesCorrection
- #run! — Bpl::AtomicAnnotation
- #run! — Bpl::Atomicity
- #run! — Bpl::Preemption
- #run! — Bpl::CostModeling
- #run! — Bpl::CtAnnotation
- #run! — Bpl::Shadowing
- #run! — Bpl::Abstraction
- #run! — Bpl::Extraction
- #run! — Bpl::Inlining
- #run! — Bpl::Normalization
- #run! — Bpl::Pruning
- #run! — Bpl::Simplification
- #run! — Bpl::Sorting
- #run! — Bpl::UnreachableBlockElimination
- #run! — Bpl::Unrolling
- #run! — Bpl::Unstructuring
- #run! — Bpl::Reading
- #run! — Bpl::Selection
- #run! — Bpl::Splitting
- #run! — Bpl::Verification
- #run! — Bpl::Writing
- #save_result — Bpl::ConditionalIdentification
- #scan — BoogieLanguage
- #scan_evaluate — Z3::ModelParser
- #scan_file — BoogieLanguage
- #scan_file — Z3::ModelParser
- #scan_setup — BoogieLanguage
- #scan_setup — Z3::ModelParser
- #scan_str — BoogieLanguage
- #scan_str — Z3::ModelParser
- #selective_self_composition — Bpl::Shadowing
- #self_composition_block! — Bpl::Shadowing
- #shadow — Bpl::Shadowing
- #shadow_assert — Bpl::Shadowing
- #shadow_copy — Bpl::Shadowing
- #shadow_decl — Bpl::Shadowing
- #shadow_eq — Bpl::Shadowing
- #shadow_proc_call! — Bpl::Shadowing
- #shadow_var_decl — Bpl::Shadowing
- #show — Bpl::AST::TypeDeclaration
- #show — Bpl::AST::FunctionDeclaration
- #show — Bpl::AST::AxiomDeclaration
- #show — Bpl::AST::StorageDeclaration
- #show — Bpl::AST::VariableDeclaration
- #show — Bpl::AST::ConstantDeclaration
- #show — Bpl::AST::ProcedureDeclaration
- #show — Bpl::AST::ImplementationDeclaration
- #show — Bpl::AST::BooleanLiteral
- #show — Bpl::AST::IntegerLiteral
- #show — Bpl::AST::BitvectorLiteral
- #show — Bpl::AST::Identifier
- #show — Bpl::AST::FunctionApplication
- #show — Bpl::AST::OldExpression
- #show — Bpl::AST::LogicalNegation
- #show — Bpl::AST::ArithmeticNegation
- #show — Bpl::AST::BinaryExpression
- #show — Bpl::AST::IfExpression
- #show — Bpl::AST::CodeExpression
- #show — Bpl::AST::MapSelect
- #show — Bpl::AST::MapUpdate
- #show — Bpl::AST::BitvectorExtract
- #show — Bpl::AST::QuantifiedExpression
- #show — Bpl::AST::Trigger
- #show — Bpl::AST::Attribute
- #show — Bpl::AST::Program
- #show — Bpl::AST::LoopInvariant
- #show — Bpl::AST::RequiresClause
- #show — Bpl::AST::ModifiesClause
- #show — Bpl::AST::EnsuresClause
- #show — Bpl::AST::AssertStatement
- #show — Bpl::AST::AssumeStatement
- #show — Bpl::AST::HavocStatement
- #show — Bpl::AST::AssignStatement
- #show — Bpl::AST::GotoStatement
- #show — Bpl::AST::ReturnStatement
- #show — Bpl::AST::CallStatement
- #show — Bpl::AST::IfStatement
- #show — Bpl::AST::WhileStatement
- #show — Bpl::AST::BreakStatement
- #show — Bpl::AST::Block
- #show — Bpl::AST::Body
- #show — Bpl::AST::BitvectorType
- #show — Bpl::AST::CustomType
- #show — Bpl::AST::MapType
- #show_attrs — Bpl::AST::Node
- #siblings — Bpl::AST::Node
- #sig — Bpl::AST::ProcedureDeclaration
- #signature — Bpl::AST::TypeDeclaration
- #signature — Bpl::AST::FunctionDeclaration
- #signature — Bpl::AST::StorageDeclaration
- #signature — Bpl::AST::VariableDeclaration
- #signature — Bpl::AST::ConstantDeclaration
- #signature — Bpl::AST::ProcedureDeclaration
- #silly_expression? — Bpl::Pruning
- #simplify — Bpl::Simplification
- #smack — Kernel
- #source_file_options — Object
- #split? — Bpl::Splitting
- #stub? — Bpl::CostModeling
- #successors — Bpl::ConditionalIdentification
- #summarize_loops! — Bpl::CostModeling
- #svg_craziness — Bpl::AST::Trace
- #target — Bpl::AST::CallStatement
- #timed — Object
- #to_range — String
- #to_s — Bpl::AST::Node
- #to_s — Bpl::AST::Token
- #to_s — Bpl::AST::Trace
- #to_s — Z3::Model
- #trivial_block? — Bpl::Simplification
- #trivial_branch? — Bpl::Simplification
- #trivial_implementation? — Bpl::Simplification
- #trivial_statement? — Bpl::Simplification
- #type — Bpl::AST::BooleanLiteral
- #type — Bpl::AST::IntegerLiteral
- #type — Bpl::AST::BitvectorLiteral
- #type — Bpl::AST::Identifier
- #type — Bpl::AST::FunctionApplication
- #type — Bpl::AST::OldExpression
- #type — Bpl::AST::LogicalNegation
- #type — Bpl::AST::ArithmeticNegation
- #type — Bpl::AST::BinaryExpression
- #type — Bpl::AST::IfExpression
- #type — Bpl::AST::CodeExpression
- #type — Bpl::AST::MapSelect
- #type — Bpl::AST::MapUpdate
- #type — Bpl::AST::BitvectorExtract
- #type — Bpl::AST::QuantifiedExpression
- #type_check — Bpl::AST::FunctionApplication
- #type_check — Bpl::AST::CallStatement
- #type_order — Bpl::Sorting
- #unbind — Bpl::AST::Binding
- #unclassify — String
- #underline — String
- #unhyphenate — String
- #unlink — Bpl::AST::Declaration
- #unlink — Bpl::AST::Node
- #unroll — Bpl::Unrolling
- #unshadow — Bpl::Shadowing
- #unstructure_conditional — Bpl::Unstructuring
- #unstructure_loop — Bpl::Unstructuring
- #unused_storage? — Bpl::Simplification
- #used — Bpl::Liveness
- #value_to_s — Bpl::AST::Trace
- #variable_pattern — Z3::Model
- #variables — Z3::Model
- #verify_incremental — Bpl::Verification
- #verify_one_shot — Bpl::Verification
- #verify_parallel_accelerated — Bpl::Verification
- #verify_parallel_worklist — Bpl::Verification
- #visible — Z3::Model
- #vvvvv — Bpl::Verification
- #warn — Kernel
- #yellow — String