diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 15:27:58 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 15:27:58 +0100 |
| commit | 27382bdb27ab6eb405374ffebed4e62b449355f4 (patch) | |
| tree | a303a401a1970a0fe7cfa746917fcc16d9c9900b /Source/VCGeneration | |
| parent | 7313085a16269a7cf8dabd5a03fac78f23f526fa (diff) | |
| parent | 259906d91cf52af536c0be3c3121e8cf2f7463e9 (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 202557ff..dbe20415 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -237,7 +237,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;
@@ -1702,11 +1702,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 01b34504..da413984 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" />
|