Implement support for case statements in Ada

gnat2goto/driver/tree_walk.adb

@@ -146,6 +146,10 @@ package body Tree_Walk is
    with Pre  => Nkind (N) = N_Loop_Statement,
         Post => Kind (Do_Loop_Statement'Result) in Class_Code;
 
+   function Do_Case_Statement (N : Node_Id) return Irep
+   with Pre  => Nkind (N) = N_Case_Statement,
+        Post => Kind (Do_Case_Statement'Result) = I_Code_Block;
+
    function Do_N_Block_Statement (N : Node_Id) return Irep
    with Pre  => Nkind (N) = N_Block_Statement,
         Post => Kind (Do_N_Block_Statement'Result) = I_Code_Block;
@@ -1764,6 +1768,80 @@ package body Tree_Walk is
       Do_Type_Declaration (New_Type, Typedef);
    end Do_Itype_Reference;
 
+   -----------------------
+   -- Do_Case_Statement --
+   -----------------------
+
+   function Do_Case_Statement (N : Node_Id) return Irep is
+      Ret : constant Irep := New_Irep (I_Code_Block);
+      Value : constant Irep := Do_Expression (Expression (N));
+
+      --  Auxiliary function to create a single test case
+      --  to emplace in a condition from a list of alternative
+      --  values.
+      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, Make_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
+         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
+      pragma Assert (List_Length (Alternatives (N)) >= 1);
+      --  Do-while loop because there must be at least one alternative.
+      loop
+         declare
+            This_Stmt : constant Irep :=
+             Process_Statements (Statements (This_Alt));
+            This_Alt_Copy : constant Node_Id := This_Alt;
+            This_Test : Irep;
+         begin
+            Next (This_Alt);
+            if not Present (This_Alt) then
+               --  Omit test, this is either `others`
+               --  or the last case of complete coverage
+               This_Test := This_Stmt;
+               Append_Op (Ret, This_Test);
+            else
+               This_Test := New_Irep (I_Code_Ifthenelse);
+               Set_Cond (This_Test,
+                         Make_Case_Test
+                           (Discrete_Choices (This_Alt_Copy)));
+               Set_Then_Case (This_Test, This_Stmt);
+               Append_Op (Ret, This_Test);
+            end if;
+         end;
+         exit when not Present (This_Alt);
+      end loop;
+      return Ret;
+   end Do_Case_Statement;
+
    -----------------------
    -- Do_Loop_Statement --
    -----------------------
@@ -4031,7 +4109,7 @@ package body Tree_Walk is
             Append_Op (Block, Do_If_Statement (N));
 
          when N_Case_Statement =>
-            Warn_Unhandled_Construct (Statement, "case");
+            Append_Op (Block, Do_Case_Statement (N));
 
          when N_Loop_Statement =>
             Append_Op (Block, Do_Loop_Statement (N));

testsuite/gnat2goto/tests/case_statement/case_statement.adb

@@ -0,0 +1,18 @@
+procedure Case_Statement is
+  function Case_Statement_Return return Integer is
+    type Sensor_Type is (Elevation, Azimuth, Distance);
+    Sensor : Sensor_Type := Elevation;
+  begin
+    case Sensor is
+      when Elevation => return 1;
+      when Azimuth   => return 2;
+      when Distance  => return 3;
+      when others    => return 4;
+    end case;
+  end Case_Statement_Return;
+
+  Result : Integer := Case_Statement_Return;
+begin
+  pragma Assert (Result = 1);
+  pragma Assert (Result /= 4);
+end Case_Statement;

testsuite/gnat2goto/tests/case_statement/test.out

@@ -0,0 +1,3 @@
+[1] file case_statement.adb line 16 assertion: SUCCESS
+[2] file case_statement.adb line 17 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_statement/test.py

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

testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb

@@ -0,0 +1,14 @@
+procedure Case_Statement_Others_Only is
+  function Case_Statement_Return return Integer is
+    type Sensor_Type is (Elevation, Azimuth, Distance);
+    Sensor : Sensor_Type := Elevation;
+  begin
+    case Sensor is
+      when others => return 1;
+    end case;
+  end Case_Statement_Return;
+
+  Result : Integer := Case_Statement_Return;
+begin
+  pragma Assert (Result = 1);
+end Case_Statement_Others_Only;

testsuite/gnat2goto/tests/case_statement_others_only/test.out

@@ -0,0 +1,2 @@
+[1] file case_statement_others_only.adb line 13 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_statement_others_only/test.py

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

testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb

@@ -0,0 +1,10 @@
+function Case_Statement_Range return String is
+  type T is range 0 .. 10;
+  X : T := 6;
+begin
+  case X is
+    when 0 .. 5  => return "Zero to five";
+    when 6 .. 10 => return "Six to ten";
+    when others  => return "Invalid";
+  end case;
+end Case_Statement_Range;

testsuite/gnat2goto/tests/case_statement_range/test.opt

@@ -0,0 +1 @@
+ALL XFAIL gnat2goto can't handle ranges in case statements

testsuite/gnat2goto/tests/case_statement_range/test.out

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

testsuite/gnat2goto/tests/case_statement_range/test.py

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

testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb

@@ -0,0 +1,17 @@
+procedure Case_Statement_Vals is
+  function Case_Statement_Return return Integer is
+    I : Integer := 3;
+  begin
+    case I is
+      when 0 | 1 | 2 => return 0;
+      when 3         => return 1;
+      when others    => return 2;
+    end case;
+  end Case_Statement_Return;
+
+  Result : Integer := Case_Statement_Return;
+begin
+  pragma Assert (Result /= 0);
+  pragma Assert (Result = 1);
+  pragma Assert (Result /= 2);
+end Case_Statement_Vals;

testsuite/gnat2goto/tests/case_statement_vals/test.out

@@ -0,0 +1,4 @@
+[1] file case_statement_vals.adb line 14 assertion: SUCCESS
+[2] file case_statement_vals.adb line 15 assertion: SUCCESS
+[3] file case_statement_vals.adb line 16 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/case_statement_vals/test.py

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