Implement support for case statements in Ada

gnat2goto/driver/tree_walk.adb

@@ -1779,16 +1779,37 @@ package body Tree_Walk is
       --  Auxiliary function to create a single test case
       --  to emplace in a condition from a list of alternative
       --  values.
-      function Make_Single_Test (Alt : Node_Id) return Irep;
-      function Make_Single_Test (Alt : Node_Id) return Irep is
-         Ret : constant Irep := New_Irep (I_Op_Eq);
-         Rhs : constant Irep := Do_Expression (Alt);
+      function Make_Case_Test (Alts : List_Id) return Irep;
+      function Make_Case_Test (Alts : List_Id) return Irep is
+         function Make_Single_Test (Alt : Node_Id) return Irep;
+         function Make_Single_Test (Alt : Node_Id) return Irep is
+            Ret : constant Irep := New_Irep (I_Op_Eq);
+            Rhs : constant Irep := Do_Expression (Alt);
+         begin
+            Set_Lhs (Ret, Value);
+            Set_Rhs (Ret, Rhs);
+            Set_Type (Ret, New_Irep (I_Bool_Type));
+            return Ret;
+         end Make_Single_Test;
+         First_Alt_Test : constant Irep := Make_Single_Test (First (Alts));
+         This_Alt : Node_Id := First (Alts);
       begin
-         Set_Lhs (Ret, Value);
-         Set_Rhs (Ret, Rhs);
-         Set_Type (Ret, New_Irep (I_Bool_Type));
-         return Ret;
-      end Make_Single_Test;
+         Next (This_Alt);
+         if not Present (This_Alt) then
+            return First_Alt_Test;
+         end if;
+         declare
+            Big_Or : constant Irep := New_Irep (I_Op_Or);
+         begin
+            Append_Op (Big_Or, First_Alt_Test);
+            Set_Type (Big_Or, New_Irep (I_Bool_Type));
+            while Present (This_Alt) loop
+               Append_Op (Big_Or, Make_Single_Test (This_Alt));
+               Next (This_Alt);
+            end loop;
+            return Big_Or;
+         end;
+      end Make_Case_Test;
 
       This_Alt : Node_Id := First (Alternatives (N));
    begin
@@ -1809,8 +1830,8 @@ package body Tree_Walk is
             else
                This_Test := New_Irep (I_Code_Ifthenelse);
                Set_Cond (This_Test,
-                         Make_Single_Test
-                           (First (Discrete_Choices (This_Alt_Copy))));
+                         Make_Case_Test
+                           (Discrete_Choices (This_Alt_Copy)));
                Set_Then_Case (This_Test, This_Stmt);
                Append_Op (Ret, This_Test);
             end if;

testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb

@@ -0,0 +1,9 @@
+function Case_Statement_Vals return String is
+  I : Integer := 3;
+begin
+  case I is
+    when 0 | 1 | 2 => return "Valid ternary";
+    when 3         => return "Invalid ternary";
+    when others    => return "";
+  end case;
+end Case_Statement_Vals;

testsuite/gnat2goto/tests/case_statement_vals/test.out

@@ -0,0 +1 @@
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_statement_vals/test.py

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