From 7a2aec84f1d924086b6f8e0f3dcbde036e12345c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 28 Sep 2015 09:47:27 -0700 Subject: update --- Source/Core/CommandLineOptions.cs | 6 +++--- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- Source/VCGeneration/VC.cs | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2dda1dd9..f4cba1dc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -588,7 +588,7 @@ namespace Microsoft.Boogie { } } - public string OwickiGriesDesugaredOutputFile = null; + public string CivlDesugaredFile = null; public bool TrustAtomicityTypes = false; public bool TrustNonInterference = false; public int TrustLayersUpto = -1; @@ -915,9 +915,9 @@ namespace Microsoft.Boogie { } return true; - case "OwickiGries": + case "CivlDesugaredFile": if (ps.ConfirmArgumentCount(1)) { - OwickiGriesDesugaredOutputFile = args[ps.i]; + CivlDesugaredFile = args[ps.i]; } return true; diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cf44a77f..15fdc081 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -502,11 +502,11 @@ namespace Microsoft.Boogie { Concurrency.Transform(linearTypeChecker, civlTypeChecker); (new LinearEraser()).VisitProgram(program); - if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) + if (CommandLineOptions.Clo.CivlDesugaredFile != null) { int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; CommandLineOptions.Clo.PrintUnstructured = 1; - PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); + PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b457b383..94584027 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1632,7 +1632,7 @@ namespace VC { //use Duplicator and Substituter rather than new //nested IToken? //document expand attribute (search for {:ignore}, for example) - //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs + //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs Func withType = (Expr from, Expr to) => { NAryExpr nFrom = from as NAryExpr; -- cgit v1.2.3