diff options
| author |  Shaz Qadeer <qadeer@microsoft.com> | 2015-09-28 09:47:27 -0700 |
|---|---|---|
| committer | Shaz Qadeer <qadeer@microsoft.com> | 2015-09-28 09:47:27 -0700 |
| commit | 7a2aec84f1d924086b6f8e0f3dcbde036e12345c (patch) | |
| tree | 71bab46500300b795a85659d9aa2299728f106d1 | |
| parent | 80e6c54ccfeac0a2ae07c18f3c8f21970e483185 (diff) | |
update
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 6 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 4 | ||||
| -rw-r--r-- | 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<Expr,Expr,Expr> withType = (Expr from, Expr to) => { NAryExpr nFrom = from as NAryExpr; |