diff options
Diffstat (limited to 'Test/smoke/smoke0.bpl')
-rw-r--r-- | Test/smoke/smoke0.bpl | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl new file mode 100644 index 00000000..85deb324 --- /dev/null +++ b/Test/smoke/smoke0.bpl @@ -0,0 +1,53 @@ +procedure a(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+procedure b(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
+
+procedure c(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ assert false;
+ } else {
+ y := 2;
+ }
+}
+
+procedure d(x:int)
+ requires x>0;
+{
+ var y : int;
+
+ if(x<0) {
+ assert false;
+ y := 1;
+ } else {
+ y := 2;
+ }
+}
+
+
|