diff options
author | 0biha <unknown> | 2014-12-23 18:02:52 +0100 |
---|---|---|
committer | 0biha <unknown> | 2014-12-23 18:02:52 +0100 |
commit | f021627edc28b6093efa874dba006cfcbc234878 (patch) | |
tree | 9f983f81db3642978ab7a90efccdd5bc9a51b85d | |
parent | 54ac6e4a1b96a3611c015717f0b1c21323e0f1fa (diff) |
Made invariant of class 'CommandLineOptions' robust by
-changing the design (replaced public field by private field + getter/setter),
-moving the invariant to class 'CommandLineOptionEngine'.
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index e66a358f..cfc80144 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -24,6 +24,7 @@ namespace Microsoft.Boogie { Contract.Invariant(DescriptiveToolName != null);
Contract.Invariant(this._environment != null);
Contract.Invariant(cce.NonNullElements(this._files));
+ Contract.Invariant(this._fileTimestamp != null);
}
private string/*!*/ _environment = "";
@@ -78,7 +79,19 @@ namespace Microsoft.Boogie { }
}
- public string/*!*/ FileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');
+ private string/*!*/ _fileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.');
+
+ public string FileTimestamp {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this._fileTimestamp;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._fileTimestamp = value;
+ }
+ }
+
public void ExpandFilename(ref string pattern, string logPrefix, string fileTimestamp) {
if (pattern != null) {
pattern = pattern.Replace("@PREFIX@", logPrefix).Replace("@TIME@", fileTimestamp);
@@ -358,10 +371,6 @@ namespace Microsoft.Boogie { /// superset of Boogie's options.
/// </summary>
public class CommandLineOptions : CommandLineOptionEngine {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(FileTimestamp != null);
- }
public CommandLineOptions()
: base("Boogie", "Boogie program verifier") {
|