Implement support for case statements in Ada

gnat2goto/driver/tree_walk.adb

@@ -1805,6 +1805,7 @@ package body Tree_Walk is
                --  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,

testsuite/gnat2goto/tests/case_statement/case_statement.adb

@@ -0,0 +1,11 @@
+function Case_Statement return String is
+  type Sensor_Type is (Elevation, Azimuth, Distance);
+  Sensor : Sensor_Type := Elevation;
+begin
+  case Sensor is
+    when Elevation => return "Elevation sensor";
+    when Azimuth   => return "Azimuth sensor";
+    when Distance  => return "Distance sensor";
+    when others    => return "";
+  end case;
+end Case_Statement;

testsuite/gnat2goto/tests/case_statement/test.out

@@ -0,0 +1 @@
+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,8 @@
+function Case_Statement_Others_Only return String is
+  type Sensor_Type is (Elevation, Azimuth, Distance);
+  Sensor : Sensor_Type := Elevation;
+begin
+  case Sensor is
+    when others    => return "";
+  end case;
+end Case_Statement_Others_Only;

testsuite/gnat2goto/tests/case_statement_others_only/test.out

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

testsuite/gnat2goto/tests/case_statement_others_only/test.py

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