cprover
symex_targett Class Referenceabstract

#include <symex_target.h>

+ Inheritance diagram for symex_targett:

Classes

struct  sourcet
 

Public Types

enum  assignment_typet {
  assignment_typet::STATE, assignment_typet::HIDDEN, assignment_typet::VISIBLE_ACTUAL_PARAMETER, assignment_typet::HIDDEN_ACTUAL_PARAMETER,
  assignment_typet::PHI, assignment_typet::GUARD
}
 

Public Member Functions

 symex_targett ()
 
virtual ~symex_targett ()
 
virtual void shared_read (const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
 
virtual void shared_write (const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
 
virtual void assignment (const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
 
virtual void decl (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
 
virtual void dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
 
virtual void function_call (const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source)=0
 
virtual void function_return (const exprt &guard, const sourcet &source)=0
 
virtual void location (const exprt &guard, const sourcet &source)=0
 
virtual void output (const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
 
virtual void output_fmt (const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)=0
 
virtual void input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
 
virtual void assumption (const exprt &guard, const exprt &cond, const sourcet &source)=0
 
virtual void assertion (const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
 
virtual void goto_instruction (const exprt &guard, const exprt &cond, const sourcet &source)=0
 
virtual void constraint (const exprt &cond, const std::string &msg, const sourcet &source)=0
 
virtual void spawn (const exprt &guard, const sourcet &source)=0
 
virtual void memory_barrier (const exprt &guard, const sourcet &source)=0
 
virtual void atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
 
virtual void atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
 

Detailed Description

Definition at line 20 of file symex_target.h.

Member Enumeration Documentation

◆ assignment_typet

Enumerator
STATE 
HIDDEN 
VISIBLE_ACTUAL_PARAMETER 
HIDDEN_ACTUAL_PARAMETER 
PHI 
GUARD 

Definition at line 56 of file symex_target.h.

Constructor & Destructor Documentation

◆ symex_targett()

symex_targett::symex_targett ( )
inline

Definition at line 23 of file symex_target.h.

◆ ~symex_targett()

virtual symex_targett::~symex_targett ( )
inlinevirtual

Definition at line 27 of file symex_target.h.

Member Function Documentation

◆ assertion()

virtual void symex_targett::assertion ( const exprt guard,
const exprt cond,
const std::string &  msg,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ assignment()

virtual void symex_targett::assignment ( const exprt guard,
const ssa_exprt ssa_lhs,
const exprt ssa_full_lhs,
const exprt original_full_lhs,
const exprt ssa_rhs,
const sourcet source,
assignment_typet  assignment_type 
)
pure virtual

Implemented in symex_target_equationt.

◆ assumption()

virtual void symex_targett::assumption ( const exprt guard,
const exprt cond,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ atomic_begin()

virtual void symex_targett::atomic_begin ( const exprt guard,
unsigned  atomic_section_id,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ atomic_end()

virtual void symex_targett::atomic_end ( const exprt guard,
unsigned  atomic_section_id,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ constraint()

virtual void symex_targett::constraint ( const exprt cond,
const std::string &  msg,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ dead()

virtual void symex_targett::dead ( const exprt guard,
const ssa_exprt ssa_lhs,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ decl()

virtual void symex_targett::decl ( const exprt guard,
const ssa_exprt ssa_lhs,
const sourcet source,
assignment_typet  assignment_type 
)
pure virtual

Implemented in symex_target_equationt.

◆ function_call()

virtual void symex_targett::function_call ( const exprt guard,
const irep_idt function_identifier,
const std::vector< exprt > &  ssa_function_arguments,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ function_return()

virtual void symex_targett::function_return ( const exprt guard,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ goto_instruction()

virtual void symex_targett::goto_instruction ( const exprt guard,
const exprt cond,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ input()

virtual void symex_targett::input ( const exprt guard,
const sourcet source,
const irep_idt input_id,
const std::list< exprt > &  args 
)
pure virtual

Implemented in symex_target_equationt.

◆ location()

virtual void symex_targett::location ( const exprt guard,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ memory_barrier()

virtual void symex_targett::memory_barrier ( const exprt guard,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ output()

virtual void symex_targett::output ( const exprt guard,
const sourcet source,
const irep_idt output_id,
const std::list< exprt > &  args 
)
pure virtual

Implemented in symex_target_equationt.

◆ output_fmt()

virtual void symex_targett::output_fmt ( const exprt guard,
const sourcet source,
const irep_idt output_id,
const irep_idt fmt,
const std::list< exprt > &  args 
)
pure virtual

Implemented in symex_target_equationt.

◆ shared_read()

virtual void symex_targett::shared_read ( const exprt guard,
const ssa_exprt ssa_rhs,
unsigned  atomic_section_id,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ shared_write()

virtual void symex_targett::shared_write ( const exprt guard,
const ssa_exprt ssa_rhs,
unsigned  atomic_section_id,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.

◆ spawn()

virtual void symex_targett::spawn ( const exprt guard,
const sourcet source 
)
pure virtual

Implemented in symex_target_equationt.


The documentation for this class was generated from the following file: