diff options
| author |  MichalMoskal <unknown> | 2010-10-08 21:24:00 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-10-08 21:24:00 +0000 |
| commit | e8179179ffa552074c55636ef3c9e1ddf600f16f (patch) | |
| tree | 12041a9ce74aadacaf453306bdc6cb51abee2f97 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | cf81e610ba128610007ed49cd79980c830d79752 (diff) | |
Add state sequence API and creation, still untested
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a449dc82..48b982bf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -206,6 +206,63 @@ namespace Microsoft.Boogie { }
}
+ public Model GetModelWithStates()
+ {
+ if (Model == null) return null;
+
+ Model m = Model.ToModel();
+
+ var mvstates = m.TryGetFunc("@MV_state");
+ if (MvInfo == null || mvstates == null)
+ return m;
+
+ Contract.Assert(mvstates.Arity == 1);
+
+ foreach (Variable v in MvInfo.AllVariables) {
+ var fn = m.TryGetFunc(v.Name);
+ if (fn != null && fn.Arity == 0) {
+ m.InitialState.AddBinding(v.Name, fn.GetConstant());
+ }
+ }
+
+ var states = new List<int>();
+ foreach (var t in mvstates.Apps)
+ states.Add(t.Args[0].AsInt());
+
+ states.Sort();
+
+ foreach (int s in states) {
+ if (0 <= s && s < MvInfo.CapturePoints.Count) {
+ VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];
+ var cs = m.MkState(map.Description);
+
+ foreach (Variable v in MvInfo.AllVariables) {
+ var e = (Expr)map.IncarnationMap[v];
+ if (e == null) continue;
+
+ Model.Element elt;
+
+ if (e is IdentifierExpr) {
+ IdentifierExpr ide = (IdentifierExpr)e;
+ elt = m.GetFunc(ide.Decl.Name).GetConstant();
+ } else if (e is LiteralExpr) {
+ LiteralExpr lit = (LiteralExpr)e;
+ elt = m.MkElement(lit.Val.ToString());
+ } else {
+ elt = m.MkFunc(e.ToString(), 0).GetConstant();
+ }
+
+ cs.AddBinding(v.Name, elt);
+ }
+
+ } else {
+ Contract.Assume(false);
+ }
+ }
+
+ return m;
+ }
+
void PrintCapturedState(int indent, Hashtable/*Variable -> Expr*/ incarnations) {
Contract.Requires(0 <= indent);
Contract.Requires(Model != null && MvInfo != null);
|