diff options
| -rw-r--r-- | Source/Houdini/Checker.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 7 | ||||
| -rw-r--r-- | Test/houdini/test10.bpl | 47 |
3 files changed, 49 insertions, 7 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index e36d32ef..1cb27648 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -25,7 +25,7 @@ namespace Microsoft.Boogie.Houdini { private ProverInterface.ErrorHandler handler;
ConditionGeneration.CounterexampleCollector collector;
- public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl, string logFilePath, bool appendLogFile) {
+ public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl) {
descriptiveName = impl.Name;
collector = new ConditionGeneration.CounterexampleCollector();
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index ce02d173..0b331356 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -327,12 +327,7 @@ namespace Microsoft.Boogie.Houdini { try {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Generating VC for {0}", impl.Name);
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
- }
- HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl);
houdiniSessions.Add(impl, session);
}
catch (VCGenException) {
diff --git a/Test/houdini/test10.bpl b/Test/houdini/test10.bpl new file mode 100644 index 00000000..abb993f7 --- /dev/null +++ b/Test/houdini/test10.bpl @@ -0,0 +1,47 @@ +var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+ sdv_21 := sdv_7;
+ sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := sdv_21;
+ havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7));
+{
+ call push(2);
+ call pop();
+ call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate} b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+ call push(1);
+ call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := 0;
+ call foo();
+}
+
|