diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-15 12:21:57 +0100 |
| commit | 578382b6bd2ace4926e9ed97cf59ec38c7b07797 (patch) | |
| tree | 5ea634e0c5c2881f674c38c5d3b1307c83db8916 /Source/VCGeneration | |
| parent | ad34aee0bb9e9090418fd1cb2e2fced7ddb625d8 (diff) | |
| parent | ee4be4f6280d39c31d95e50ac3ac039c6d2ba5f5 (diff) | |
Merge
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.csproj | 4 |
3 files changed, 8 insertions, 4 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8afbf027..ad2b7e68 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -234,7 +234,7 @@ namespace Microsoft.Boogie { Model m = Model;
ApplyRedirections(m);
- var mvstates = m.TryGetFunc("@MV_state");
+ var mvstates = m.TryGetFunc("$mv_state");
if (MvInfo == null || mvstates == null)
return m;
@@ -1700,11 +1700,11 @@ namespace VC { {
public readonly List<Variable> AllVariables = new List<Variable>();
public readonly List<Mapping> CapturePoints = new List<Mapping>();
- public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "@MV_state",
+ public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));
- public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));
+ public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int));
public ModelViewInfo(Program program, Implementation impl) {
Contract.Requires(program != null);
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index b4db817f..f90788d7 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2444,7 +2444,7 @@ namespace VC { private void GetModelWithStates(Model m) {
if (m == null) return;
var mvInfo = mainInfo.mvInfo;
- var mvstates = m.TryGetFunc("@MV_state");
+ var mvstates = m.TryGetFunc("$mv_state");
if (mvstates == null)
return;
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index f724307b..a7be5827 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -97,6 +97,8 @@ <ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
|