diff options
| author |  mikebarnett <unknown> | 2010-12-20 18:53:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2010-12-20 18:53:41 +0000 |
| commit | 1fd6537e40b262e6a67d836b4a66f3444e5911bb (patch) | |
| tree | ba06431288cf1067ade34b1b4f21d8b787bf6b7f /BCT/BytecodeTranslator/TraverserFactory.cs | |
| parent | 791a8698f31b69330a37bc1c4f655f7bdaa84289 (diff) | |
Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each statement that has a source location.
Diffstat (limited to 'BCT/BytecodeTranslator/TraverserFactory.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 4a48cf5f..953e5030 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -18,8 +18,15 @@ using Bpl = Microsoft.Boogie; namespace BytecodeTranslator {
public abstract class TraverserFactory {
- public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(new Sink(this), contractProvider); }
- public virtual StatementTraverser MakeStatementTraverser(Sink sink) { return new StatementTraverser(sink); }
- public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) { return new ExpressionTraverser(sink, statementTraverser); }
+ public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, ISourceLocationProvider/*?*/ sourceLocationProvider)
+ {
+ return new MetadataTraverser(new Sink(this), contractProvider, sourceLocationProvider);
+ }
+ public virtual StatementTraverser MakeStatementTraverser(Sink sink, ISourceLocationProvider/*?*/ sourceLocationProvider) {
+ return new StatementTraverser(sink, sourceLocationProvider);
+ }
+ public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {
+ return new ExpressionTraverser(sink, statementTraverser);
+ }
}
}
\ No newline at end of file |