diff options
| author |  Ally Donaldson <unknown> | 2014-05-27 10:03:29 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2014-05-27 10:03:29 +0100 |
| commit | 8764209cdceaf1b07446759b02b05654c3582a93 (patch) | |
| tree | a4f87eb3d6a6007ba863c833a238b8b1da7076ad | |
| parent | 440625852cc22770912129c33cea936bf72028b9 (diff) | |
Merge
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 65 |
1 files changed, 64 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index acb329ed..00d18942 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -9,7 +9,7 @@ using System.Threading; using System.Threading.Tasks;
using VC;
using BoogiePL = Microsoft.Boogie;
-
+using System.Diagnostics;
namespace Microsoft.Boogie
{
@@ -773,6 +773,9 @@ namespace Microsoft.Boogie Contract.Requires(stats != null);
Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
+ KatyaDemo(program);
+
+
if (requestId == null)
{
requestId = "unknown";
@@ -931,6 +934,66 @@ namespace Microsoft.Boogie return outcome;
}
+ private static void KatyaDemo(Program program) {
+ // Look for an implementation called "main"
+ // Add a new variable "our_counter"
+ // Initialise it to 0
+ // At every loop, add "our_counter := our_counter + 1" as first statement
+
+ foreach(Declaration d in program.TopLevelDeclarations) {
+ Implementation impl = d as Implementation;
+ if(impl != null && impl.Name == "main") {
+ // Add the new variable "our_counter"
+ LocalVariable our_counter = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, "our_counter", Type.Int));
+ impl.LocVars.Add(our_counter);
+
+ // Initialise it to 0
+ impl.StructuredStmts.BigBlocks[0].simpleCmds.Insert(0, new AssignCmd(Token.NoToken,
+ new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken,
+ new IdentifierExpr(Token.NoToken, our_counter)) },
+ new List<Expr> { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0)) }));
+
+ AddIncrements(impl.StructuredStmts, our_counter);
+
+ }
+
+ }
+
+
+ using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))
+ {
+ program.Emit(writer);
+ }
+
+ Environment.Exit(0);
+ }
+
+ private static void AddIncrements(StmtList stmtList, LocalVariable our_counter) {
+ foreach(BigBlock bb in stmtList.BigBlocks) {
+ AddIncrements(bb, our_counter);
+ }
+ }
+
+ private static void AddIncrements(BigBlock bb, LocalVariable our_counter) {
+ if(bb.ec is IfCmd) {
+ Debug.Assert(false);
+ } else if(bb.ec is WhileCmd) {
+ WhileCmd wc = bb.ec as WhileCmd;
+
+ wc.Body.BigBlocks[0].simpleCmds.Insert(0,
+ new AssignCmd(Token.NoToken,
+ new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, our_counter)) },
+ new List<Expr> {
+ new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Add),
+ new List<Expr> {
+ new IdentifierExpr(Token.NoToken, our_counter),
+ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)) }) }));
+ AddIncrements(wc.Body, our_counter);
+ }
+
+ }
+
public static void CancelRequest(string requestId)
{
|