cprover
symex_target_equationt Class Reference

#include <symex_target_equation.h>

+ Inheritance diagram for symex_target_equationt:
+ Collaboration diagram for symex_target_equationt:

Classes

class  SSA_stept
 

Public Types

typedef std::list< SSA_steptSSA_stepst
 
- Public Types inherited from symex_targett
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

virtual ~symex_target_equationt ()=default
 
virtual void shared_read (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
 read from a shared variable More...
 
virtual void shared_write (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
 write to a sharedvariable More...
 
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)
 write to a variable More...
 
virtual void decl (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
 declare a fresh variable More...
 
virtual void dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
 declare a fresh variable More...
 
virtual void function_call (const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source)
 just record a location More...
 
virtual void function_return (const exprt &guard, const sourcet &source)
 just record a location More...
 
virtual void location (const exprt &guard, const sourcet &source)
 just record a location More...
 
virtual void output (const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
 just record output More...
 
virtual void output_fmt (const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
 just record formatted output More...
 
virtual void input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
 just record input More...
 
virtual void assumption (const exprt &guard, const exprt &cond, const sourcet &source)
 record an assumption More...
 
virtual void assertion (const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
 record an assertion More...
 
virtual void goto_instruction (const exprt &guard, const exprt &cond, const sourcet &source)
 record a goto instruction More...
 
virtual void constraint (const exprt &cond, const std::string &msg, const sourcet &source)
 record a constraint More...
 
virtual void spawn (const exprt &guard, const sourcet &source)
 spawn a new thread More...
 
virtual void memory_barrier (const exprt &guard, const sourcet &source)
 
virtual void atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source)
 start an atomic section More...
 
virtual void atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source)
 end an atomic section More...
 
void convert (prop_convt &prop_conv)
 
void convert_assignments (decision_proceduret &decision_procedure) const
 converts assignments More...
 
void convert_decls (prop_convt &prop_conv) const
 converts declarations More...
 
void convert_assumptions (prop_convt &prop_conv)
 converts assumptions More...
 
void convert_assertions (prop_convt &prop_conv)
 converts assertions More...
 
void convert_constraints (decision_proceduret &decision_procedure) const
 converts constraints More...
 
void convert_goto_instructions (prop_convt &prop_conv)
 converts goto instructions More...
 
void convert_guards (prop_convt &prop_conv)
 converts guards More...
 
void convert_function_calls (decision_proceduret &decision_procedure)
 converts function calls More...
 
void convert_io (decision_proceduret &decision_procedure)
 converts I/O More...
 
exprt make_expression () const
 
std::size_t count_assertions () const
 
std::size_t count_ignored_SSA_steps () const
 
SSA_stepst::iterator get_SSA_step (std::size_t s)
 
void output (std::ostream &out, const namespacet &ns) const
 
void clear ()
 
bool has_threads () const
 
- Public Member Functions inherited from symex_targett
 symex_targett ()
 
virtual ~symex_targett ()
 

Public Attributes

SSA_stepst SSA_steps
 

Protected Member Functions

void merge_ireps (SSA_stept &SSA_step)
 

Protected Attributes

merge_irept merge_irep
 

Detailed Description

Definition at line 32 of file symex_target_equation.h.

Member Typedef Documentation

◆ SSA_stepst

Definition at line 294 of file symex_target_equation.h.

Constructor & Destructor Documentation

◆ ~symex_target_equationt()

virtual symex_target_equationt::~symex_target_equationt ( )
virtualdefault

Member Function Documentation

◆ assertion()

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

record an assertion

Implements symex_targett.

Definition at line 321 of file symex_target_equation.cpp.

◆ assignment()

void symex_target_equationt::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 
)
virtual

write to a variable

Implements symex_targett.

Definition at line 128 of file symex_target_equation.cpp.

◆ assumption()

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

record an assumption

Implements symex_targett.

Definition at line 304 of file symex_target_equation.cpp.

◆ atomic_begin()

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

start an atomic section

Implements symex_targett.

Definition at line 96 of file symex_target_equation.cpp.

◆ atomic_end()

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

end an atomic section

Implements symex_targett.

Definition at line 112 of file symex_target_equation.cpp.

◆ clear()

void symex_target_equationt::clear ( void  )
inline

Definition at line 310 of file symex_target_equation.h.

◆ constraint()

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

record a constraint

Implements symex_targett.

Definition at line 357 of file symex_target_equation.cpp.

◆ convert()

void symex_target_equationt::convert ( prop_convt prop_conv)

Definition at line 375 of file symex_target_equation.cpp.

◆ convert_assertions()

void symex_target_equationt::convert_assertions ( prop_convt prop_conv)

converts assertions

Returns
-

Definition at line 583 of file symex_target_equation.cpp.

◆ convert_assignments()

void symex_target_equationt::convert_assignments ( decision_proceduret decision_procedure) const

converts assignments

parameters: decision procedure
Returns
-

Definition at line 401 of file symex_target_equation.cpp.

◆ convert_assumptions()

void symex_target_equationt::convert_assumptions ( prop_convt prop_conv)

converts assumptions

Returns
-

Definition at line 479 of file symex_target_equation.cpp.

◆ convert_constraints()

void symex_target_equationt::convert_constraints ( decision_proceduret decision_procedure) const

converts constraints

parameters: decision procedure
Returns
-

Definition at line 550 of file symex_target_equation.cpp.

◆ convert_decls()

void symex_target_equationt::convert_decls ( prop_convt prop_conv) const

converts declarations

Returns
-

Definition at line 422 of file symex_target_equation.cpp.

◆ convert_function_calls()

void symex_target_equationt::convert_function_calls ( decision_proceduret dec_proc)

converts function calls

parameters: decision procedure
Returns
-

Definition at line 667 of file symex_target_equation.cpp.

◆ convert_goto_instructions()

void symex_target_equationt::convert_goto_instructions ( prop_convt prop_conv)

converts goto instructions

Returns
-

Definition at line 514 of file symex_target_equation.cpp.

◆ convert_guards()

void symex_target_equationt::convert_guards ( prop_convt prop_conv)

converts guards

Returns
-

Definition at line 447 of file symex_target_equation.cpp.

◆ convert_io()

void symex_target_equationt::convert_io ( decision_proceduret dec_proc)

converts I/O

parameters: decision procedure
Returns
-

Definition at line 700 of file symex_target_equation.cpp.

◆ count_assertions()

std::size_t symex_target_equationt::count_assertions ( ) const
inline

Definition at line 272 of file symex_target_equation.h.

◆ count_ignored_SSA_steps()

std::size_t symex_target_equationt::count_ignored_SSA_steps ( ) const
inline

Definition at line 283 of file symex_target_equation.h.

◆ dead()

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

declare a fresh variable

Implements symex_targett.

Definition at line 186 of file symex_target_equation.cpp.

◆ decl()

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

declare a fresh variable

Implements symex_targett.

Definition at line 159 of file symex_target_equation.cpp.

◆ function_call()

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

just record a location

Implements symex_targett.

Definition at line 210 of file symex_target_equation.cpp.

◆ function_return()

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

just record a location

Implements symex_targett.

Definition at line 229 of file symex_target_equation.cpp.

◆ get_SSA_step()

SSA_stepst::iterator symex_target_equationt::get_SSA_step ( std::size_t  s)
inline

Definition at line 297 of file symex_target_equation.h.

◆ goto_instruction()

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

record a goto instruction

Implements symex_targett.

Definition at line 340 of file symex_target_equation.cpp.

◆ has_threads()

bool symex_target_equationt::has_threads ( ) const
inline

Definition at line 315 of file symex_target_equation.h.

◆ input()

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

just record input

Implements symex_targett.

Definition at line 285 of file symex_target_equation.cpp.

◆ location()

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

just record a location

Implements symex_targett.

Definition at line 195 of file symex_target_equation.cpp.

◆ make_expression()

exprt symex_target_equationt::make_expression ( ) const

◆ memory_barrier()

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

Implements symex_targett.

Definition at line 82 of file symex_target_equation.cpp.

◆ merge_ireps()

void symex_target_equationt::merge_ireps ( SSA_stept SSA_step)
protected

Definition at line 729 of file symex_target_equation.cpp.

◆ output() [1/2]

void symex_target_equationt::output ( const exprt guard,
const sourcet source,
const irep_idt fmt,
const std::list< exprt > &  args 
)
virtual

just record output

Implements symex_targett.

Definition at line 244 of file symex_target_equation.cpp.

◆ output() [2/2]

void symex_target_equationt::output ( std::ostream &  out,
const namespacet ns 
) const

Definition at line 749 of file symex_target_equation.cpp.

◆ output_fmt()

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

just record formatted output

Implements symex_targett.

Definition at line 263 of file symex_target_equation.cpp.

◆ shared_read()

void symex_target_equationt::shared_read ( const exprt guard,
const ssa_exprt ssa_object,
unsigned  atomic_section_id,
const sourcet source 
)
virtual

read from a shared variable

Implements symex_targett.

Definition at line 31 of file symex_target_equation.cpp.

◆ shared_write()

void symex_target_equationt::shared_write ( const exprt guard,
const ssa_exprt ssa_object,
unsigned  atomic_section_id,
const sourcet source 
)
virtual

write to a sharedvariable

Implements symex_targett.

Definition at line 50 of file symex_target_equation.cpp.

◆ spawn()

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

spawn a new thread

Implements symex_targett.

Definition at line 69 of file symex_target_equation.cpp.

Member Data Documentation

◆ merge_irep

merge_irept symex_target_equationt::merge_irep
protected

Definition at line 328 of file symex_target_equation.h.

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

Definition at line 295 of file symex_target_equation.h.


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