diff options
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/Main.cs | 4 | ||||
| -rw-r--r-- | Source/ModelViewer/ModelViewer.csproj | 3 | ||||
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 2 |
3 files changed, 6 insertions, 3 deletions
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 46342a9f..dfe24b6f 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -99,7 +99,7 @@ namespace Microsoft.Boogie.ModelViewer using (var rd = new StringReader(model))
{
- allModels = Model.ParseModels(rd).ToArray();
+ allModels = Model.ParseModels(rd, "").ToArray();
}
AddAndLoadModel(setModelIdTo);
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie.ModelViewer if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {
using (var rd = File.OpenText(modelFileName)) {
- allModels = Model.ParseModels(rd).ToArray();
+ allModels = Model.ParseModels(rd,"").ToArray();
}
AddAndLoadModel(setModelIdTo);
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index f708ddda..75e5521c 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -97,6 +97,8 @@ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup>
<StartupObject />
@@ -122,6 +124,7 @@ <DependentUpon>Main.cs</DependentUpon>
</Compile>
<Compile Include="..\Model\Model.cs" />
+ <Compile Include="..\Model\ModelParser.cs" />
<Compile Include="Namer.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="SourceView.cs">
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index c226d646..b4540717 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -274,7 +274,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc new string[] {
"$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",
"$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",
- "@MV_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
+ "$mv_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
"$field_parent_type", "$field_type", "$file_name_is", "$good_state",
"$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",
"$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",
|