Skip to content

Assignment typet fix master #872

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jul 22, 2017
Merged

Assignment typet fix master #872

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1f8b504
Make assignment_typet into an enum class
reuk Apr 24, 2017
5b42bc7
Initialise variables in symex_target_equation.h
reuk Apr 24, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,9 @@ void build_goto_trace(
symex_target_equationt::assignment_typet::PHI ||
SSA_step.assignment_type==
symex_target_equationt::assignment_typet::GUARD))
{
continue;
}

goto_tracet::stepst &steps=time_map[current_time];
steps.push_back(goto_trace_stept());
Expand Down
7 changes: 6 additions & 1 deletion src/goto-symex/symex_target.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,12 @@ class symex_targett

enum class assignment_typet
{
STATE, HIDDEN, VISIBLE_ACTUAL_PARAMETER, HIDDEN_ACTUAL_PARAMETER, PHI, GUARD
STATE,
HIDDEN,
VISIBLE_ACTUAL_PARAMETER,
HIDDEN_ACTUAL_PARAMETER,
PHI,
GUARD,
};

// read event
Expand Down
18 changes: 12 additions & 6 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1002,17 +1002,23 @@ void symex_target_equationt::SSA_stept::output(
switch(assignment_type)
{
case assignment_typet::HIDDEN:
out << "HIDDEN"; break;
out << "HIDDEN";
break;
case assignment_typet::STATE:
out << "STATE"; break;
out << "STATE";
break;
case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
out << "VISIBLE_ACTUAL_PARAMETER"; break;
out << "VISIBLE_ACTUAL_PARAMETER";
break;
case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
out << "HIDDEN_ACTUAL_PARAMETER"; break;
out << "HIDDEN_ACTUAL_PARAMETER";
break;
case assignment_typet::PHI:
out << "PHI"; break;
out << "PHI";
break;
case assignment_typet::GUARD:
out << "GUARD"; break;
out << "GUARD";
break;
default:
{
}
Expand Down
10 changes: 5 additions & 5 deletions src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ class symex_target_equationt:public symex_targett
bool is_atomic_end() const { return type==goto_trace_stept::typet::ATOMIC_END; }

// we may choose to hide
bool hidden;
bool hidden=false;

exprt guard;
literalt guard_literal;
Expand All @@ -213,7 +213,7 @@ class symex_target_equationt:public symex_targett
ssa_exprt ssa_lhs;
exprt ssa_full_lhs, original_full_lhs;
exprt ssa_rhs;
assignment_typet assignment_type;
assignment_typet assignment_type=assignment_typet::STATE;

// for ASSUME/ASSERT/GOTO/CONSTRAINT
exprt cond_expr;
Expand All @@ -222,18 +222,18 @@ class symex_target_equationt:public symex_targett

// for INPUT/OUTPUT
irep_idt format_string, io_id;
bool formatted;
bool formatted=false;
std::list<exprt> io_args;
std::list<exprt> converted_io_args;

// for function call/return
irep_idt identifier;

// for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
unsigned atomic_section_id;
unsigned atomic_section_id=0;

// for slicing
bool ignore;
bool ignore=false;

SSA_stept():
type(goto_trace_stept::typet::NONE),
Expand Down