Skip to content

Interpreter #267

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

Closed
wants to merge 9 commits into from
Closed

Interpreter #267

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
6ee70ea
get symbol of member
dcattaruzza Oct 25, 2016
471473e
Auxiliary function for getting byte offsets of members
dcattaruzza Oct 25, 2016
59746be
Auxiliary function to check if the ssa has enough data to build an id…
dcattaruzza Oct 25, 2016
019ef0c
Bitwise operators for mpinteger
dcattaruzza Oct 25, 2016
b484a6f
Auxiliary function to retrieve tail of trace
dcattaruzza Oct 25, 2016
3bfe1e9
Changes to interpreter to cover a number of java functions and objects
dcattaruzza Oct 25, 2016
ea88204
Interpreter class header guards
dcattaruzza Nov 10, 2016
25e429f
_H for header guards
dcattaruzza Nov 10, 2016
caca1d2
avoid throw in non-bodied function parameters and output (other) inst…
dcattaruzza Nov 24, 2016
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
1 change: 1 addition & 0 deletions src/goto-instrument/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../langapi/langapi$(LIBEXT) \
../xmllang/xmllang$(LIBEXT) \
../util/util$(LIBEXT) \
../json/json$(LIBEXT) \
../solvers/solvers$(LIBEXT)

INCLUDES= -I ..
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/goto_instrument_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -442,7 +442,7 @@ int goto_instrument_parse_optionst::doit()
if(cmdline.isset("interpreter"))
{
status() << "Starting interpreter" << eom;
interpreter(symbol_table, goto_functions);
interpreter(symbol_table, goto_functions, this);
return 0;
}

Expand Down
6 changes: 5 additions & 1 deletion src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ void goto_trace_stept::output(
case goto_trace_stept::ASSIGNMENT: out << "ASSIGNMENT"; break;
case goto_trace_stept::GOTO: out << "GOTO"; break;
case goto_trace_stept::DECL: out << "DECL"; break;
case goto_trace_stept::DEAD: out << "DEAD"; break;
case goto_trace_stept::OUTPUT: out << "OUTPUT"; break;
case goto_trace_stept::INPUT: out << "INPUT"; break;
case goto_trace_stept::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break;
Expand All @@ -75,7 +76,10 @@ void goto_trace_stept::output(
case goto_trace_stept::SHARED_WRITE: out << "SHARED WRITE"; break;
case goto_trace_stept::FUNCTION_CALL: out << "FUNCTION CALL"; break;
case goto_trace_stept::FUNCTION_RETURN: out << "FUNCTION RETURN"; break;
default: assert(false);
default: {
out << "unknown type: " << type << std::endl;
assert(false);
}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm generally in favour of omitting the "default" clause when all cases are covered, so as to let the compiler warn about this. But that view isn't necessarily shared by others.

That said: the placement of { and } does not match coding guidelines.

}

if(type==ASSERT || type==ASSUME || type==GOTO)
Expand Down
6 changes: 6 additions & 0 deletions src/goto-programs/goto_trace.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,12 @@ class goto_tracet
steps.push_back(step);
}

//Retrieves the final step in the trace
inline goto_trace_stept &get_last_step()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need to use "inline" within class definition.

{
return steps.back();
}

// delete all steps after (not including) s
void trim_after(stepst::iterator s)
{
Expand Down
Loading