Add tests for case expressions

gnat2goto/driver/tree_walk.adb

@@ -828,6 +828,7 @@ package body Tree_Walk is
          declare
             Big_Or : constant Irep := New_Irep (I_Op_Or);
          begin
+            Set_Type (Big_Or, Make_Bool_Type);
             Append_Op (Big_Or, First_Alt_Test);
             while Present (This_Alt) loop
                Append_Op (Big_Or, Make_Single_Test (This_Alt));

testsuite/gnat2goto/tests/case_expression/case_expression.adb

@@ -0,0 +1,24 @@
+procedure Case_Expression is
+  type Weekday is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
+  Day : Weekday := Tue;
+  Hours : Integer;
+  --  We need this to avoid the front-end's
+  --  constant folding mess up with the validity
+  --  of this test.
+  function Nested_Case_Expr (WDay : Weekday) 
+    return Integer is
+  begin
+     return (case WDay is
+              when Mon => 1,
+              when Tue => 2,
+              when Wed => 3,
+              when Thu => 4,
+              when Fri => 5,
+              when Sat => 6,
+              when Sun => 7);
+  end Nested_Case_Expr;
+begin
+  Hours := Nested_Case_Expr (Day);
+  pragma Assert (Hours = 2);
+  pragma Assert (Hours /= 1);
+end Case_Expression;

testsuite/gnat2goto/tests/case_expression/test.out

@@ -0,0 +1,3 @@
+[1] file case_expression.adb line 22 assertion: SUCCESS
+[2] file case_expression.adb line 23 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_expression/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/case_expression_others/case_expression_others.adb

@@ -0,0 +1,20 @@
+procedure Case_Expression_Others is
+  Invalid_Ternary : Integer := 3;
+  Valid_Result : Integer;
+  --  We need this to make sure that the
+  --  frontend's constant folding isn't
+  --  causing us to test something other
+  --  than what we originally expected.
+  function Nested_One (Ternary : Integer) return Integer is
+  begin
+    return (case Invalid_Ternary is
+            when 0 => 0,
+            when 1 => 0,
+            when 2 => 0,
+            when others => 1);
+  end Nested_One;
+begin
+  Valid_Result := Nested_One (Invalid_Ternary);
+  pragma Assert (Valid_Result = 1);
+  pragma Assert (Valid_Result /= 0);
+end Case_Expression_Others;

testsuite/gnat2goto/tests/case_expression_others/test.out

@@ -0,0 +1,3 @@
+[1] file case_expression_others.adb line 18 assertion: SUCCESS
+[2] file case_expression_others.adb line 19 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_expression_others/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/case_expression_range/case_expression_range.adb

@@ -0,0 +1,12 @@
+procedure Case_Expression_Range is
+  Random_Val : Integer := 10;
+  Result : Integer;
+begin
+  Result := (case Random_Val is
+    when 1..10 => 1,
+    when 11..20 => 2,
+    when others => 3);
+
+  pragma Assert (Result = 1);
+  pragma Assert (Result /= 3);
+end Case_Expression_Range;

testsuite/gnat2goto/tests/case_expression_range/test.opt

@@ -0,0 +1 @@
+ALL XFAIL gnat2goto throws exceptions but produces something that crashes CBMC even harder

testsuite/gnat2goto/tests/case_expression_range/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

testsuite/gnat2goto/tests/case_expression_vals/case_expression_or.adb

@@ -0,0 +1,13 @@
+procedure Case_Expression_Or is
+  type Weekday is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
+  Day : Weekday := Tue;
+  Hours : Integer;
+begin
+  Hours := (case Day is
+            when Mon | Tue => 1,
+            when Wed | Thu => 2,
+            when Fri | Sat => 3,
+            when Sun       => 0);
+  pragma Assert (Hours = 1);
+  pragma Assert (Hours /= 2);
+end Case_Expression_Or;

testsuite/gnat2goto/tests/case_expression_vals/test.out

@@ -0,0 +1,3 @@
+[1] file case_expression_or.adb line 11 assertion: SUCCESS
+[2] file case_expression_or.adb line 12 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_expression_vals/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()