|
ilang
1.1.4
ILAng: A Modeling and Verification Platform for SoCs
|
|
ilang
1.1.4
ILAng: A Modeling and Verification Platform for SoCs
|
This is the complete list of members for ilang::Tso, including all inherited members.
| _all_inst_trace_steps | ilang::MemoryModel | protected |
| _all_trace_steps | ilang::MemoryModel | protected |
| _constr | ilang::MemoryModel | protected |
| _ctx_ | ilang::MemoryModel | protected |
| _expr2z3_ | ilang::MemoryModel | mutableprotected |
| _final_trace_step | ilang::MemoryModel | protected |
| _ila_trace_steps | ilang::MemoryModel | protected |
| _init_trace_step | ilang::MemoryModel | protected |
| AddDoubleTraceStepProperty(std::function< z3::expr(const TraceStep &, const TraceStep &)>, std::function< bool(const TraceStep &, const TraceStep &)>) | ilang::MemoryModel | virtual |
| AddrDataVec typedef | ilang::MemoryModel | |
| AddSingleTraceStepProperty(const ExprPtr &property, std::function< bool(const TraceStep &)> filter) | ilang::MemoryModel | virtual |
| ApplyAxioms() override | ilang::Tso | virtual |
| AxiomFuncHint enum name (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| ConvertZ3(const ExprPtr &ast, const std::string &suffix) const | ilang::MemoryModel | inline |
| CreateGlobalFinalStep(const ExprPtr &property) | ilang::MemoryModel | protected |
| CreateGlobalInitStep() | ilang::MemoryModel | protected |
| ctx() const | ilang::MemoryModel | inlineprotected |
| Decode(const TraceStep &l) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| DecodeStatic(const TraceStep &l) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| FENCE_list (defined in ilang::Tso) | ilang::Tso | protected |
| FinishRegisterSteps() override | ilang::Tso | virtual |
| GetAllTraceSteps() const | ilang::MemoryModel | inline |
| GetSingleTraceStepProperty(const ExprPtr &property, std::function< bool(const TraceStep &)> filter, std::function< void(const z3::expr &)> collector) | ilang::MemoryModel | virtual |
| HB(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| HINT_NONE enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| HINT_READ enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| HINT_WRITE enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| ILANameStateNameSetMap typedef | ilang::MemoryModel | |
| InitSize(const ProgramTemplate &_tmpl) | ilang::MemoryModel | virtual |
| InstrVec typedef | ilang::MemoryModel | |
| m_ila_private_state_names | ilang::MemoryModel | protected |
| m_p_global_ila | ilang::MemoryModel | protected |
| m_shared_state_names | ilang::MemoryModel | protected |
| MemoryModel(z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr) (defined in ilang::MemoryModel) | ilang::MemoryModel | |
| nested_finder_ | ilang::MemoryModel | mutableprotected |
| PerILATraceStepPtrSet typedef | ilang::MemoryModel | |
| PO(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| ProgramTemplate typedef | ilang::MemoryModel | |
| PureWrite_list (defined in ilang::Tso) | ilang::Tso | protected |
| READ_list (defined in ilang::Tso) | ilang::Tso | protected |
| RegisterSteps(size_t regIdx, const InstrVec &_inst_seq) override | ilang::Tso | virtual |
| RMW_list (defined in ilang::Tso) | ilang::Tso | protected |
| SameAddress(const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| SameAddressStatic(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| SameCore(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| SameCoreStatic(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| SameData(const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| SetFinalProperty(const ExprPtr &property) override | ilang::Tso | virtual |
| SetLocalState(const std::vector< bool > &ordered) | ilang::MemoryModel | virtual |
| StateNameSet typedef | ilang::MemoryModel | |
| STATIC_FALSE enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| STATIC_TRUE enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| STATIC_UNKNOWN enum value (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| StaticResult enum name (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| Sync(const TraceStep &l, const TraceStep &r) const (defined in ilang::MemoryModel) | ilang::MemoryModel | protected |
| TraceStepPtr typedef | ilang::MemoryModel | |
| TraceStepPtrSet typedef | ilang::MemoryModel | |
| TraceStepType typedef | ilang::MemoryModel | |
| Tso(z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr) | ilang::Tso | inline |
| TsoModel | ilang::Tso | static |
| TsoTraceStepPtr typedef | ilang::Tso | |
| TsoTraceStepPtrSet typedef | ilang::Tso | |
| WRITE_list (defined in ilang::Tso) | ilang::Tso | protected |
| Z3ExistsList(const ZExprVec &l) const | ilang::MemoryModel | protected |
| Z3ForallList(const ZExprVec &l) const | ilang::MemoryModel | protected |
| ZExpr typedef | ilang::MemoryModel | |
| ZExprVec typedef | ilang::MemoryModel | |
| ~MemoryModel() (defined in ilang::MemoryModel) | ilang::MemoryModel | inlinevirtual |
1.8.5
