Skip to content

[depends: #1330] Interpreter fixes #1274

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 19 commits into from
Closed

[depends: #1330] Interpreter fixes #1274

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
e3e7bb8
Get symbol of member expression
dcattaruzza Oct 25, 2016
3c8bcb9
Auxiliary function to check if the ssa has enough data to build an id…
dcattaruzza Oct 25, 2016
1c9ace0
Bitwise operators for mpinteger
dcattaruzza Oct 25, 2016
74ade14
Auxiliary function to retrieve tail of trace and added dead command t…
dcattaruzza Oct 25, 2016
10c2651
Fix arithmetic shift operators
smowton Jan 13, 2017
4cc9e72
Add size/value checks to bitwise mp_arith operations
Aug 22, 2017
5d8884f
update interpreter
Mar 2, 2017
a2628d7
New class for sparse vectors in util
romainbrenguier Mar 30, 2017
9a910fc
Interpreter: switch to sparse vector memory map
romainbrenguier Mar 23, 2017
784bd51
Add support for unbounded-size objects
romainbrenguier Mar 23, 2017
46a87bb
Add includes to sparse_vector.h
Mar 31, 2017
e63a8c6
Remove trace_stackt
smowton Apr 12, 2017
8e9937e
Handle typecast when evaluating addresses in the interpreter
cristina-david Apr 20, 2017
346ef12
Change two errors to warnings
Jun 20, 2017
7a6f39f
Fix interpreter allocation sizing
smowton Jul 19, 2017
fcf6ffa
Remove constant_exprt::integer_constant
tautschnig Aug 23, 2017
a0b4094
Interpreter: replace assert by invariants
tautschnig Aug 23, 2017
61639a1
Replace 3-valued char by enum
tautschnig Aug 23, 2017
fdbb38e
Interpreter: constify mp_integer typed address parameters
tautschnig Aug 23, 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: 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 @@ -540,7 +540,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, get_message_handler());
return 0;
}

Expand Down
5 changes: 4 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 @@ -44,6 +44,7 @@ void goto_trace_stept::output(
case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
case goto_trace_stept::typet::DECL: out << "DECL"; break;
case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
case goto_trace_stept::typet::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break;
Expand All @@ -53,7 +54,9 @@ void goto_trace_stept::output(
case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
case goto_trace_stept::typet::FUNCTION_RETURN:
out << "FUNCTION RETURN"; break;
default: UNREACHABLE;
default:
out << "unknown type: " << static_cast<int>(type) << std::endl;
UNREACHABLE;
}

if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO)
Expand Down
7 changes: 7 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 @@ -174,6 +174,13 @@ class goto_tracet
steps.push_back(step);
}

// retrieves the final step in the trace for manipulation
// (used to fill a trace from code, hence non-const)
inline goto_trace_stept &get_last_step()
{
return steps.back();
}

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