diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 55d631d12..dc9ffd7ab 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/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)); diff --git a/testsuite/gnat2goto/tests/case_statement/case_statement.adb b/testsuite/gnat2goto/tests/case_statement/case_statement.adb new file mode 100644 index 000000000..46e8c0fa6 --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/case_statement/test.out b/testsuite/gnat2goto/tests/case_statement/test.out new file mode 100644 index 000000000..db3e9010f --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/case_statement/test.py b/testsuite/gnat2goto/tests/case_statement/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb b/testsuite/gnat2goto/tests/case_statement_others_only/case_statement_others_only.adb new file mode 100644 index 000000000..9ee676f87 --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/test.out b/testsuite/gnat2goto/tests/case_statement_others_only/test.out new file mode 100644 index 000000000..bf6e7ad67 --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/case_statement_others_only/test.py b/testsuite/gnat2goto/tests/case_statement_others_only/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_others_only/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb b/testsuite/gnat2goto/tests/case_statement_range/case_statement_range.adb new file mode 100644 index 000000000..3aa95a72e --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.opt b/testsuite/gnat2goto/tests/case_statement_range/test.opt new file mode 100644 index 000000000..7fbffec2f --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.opt @@ -0,0 +1 @@ +ALL XFAIL gnat2goto can't handle ranges in case statements diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.out b/testsuite/gnat2goto/tests/case_statement_range/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/case_statement_range/test.py b/testsuite/gnat2goto/tests/case_statement_range/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_range/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb b/testsuite/gnat2goto/tests/case_statement_vals/case_statement_vals.adb new file mode 100644 index 000000000..898229f04 --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/case_statement_vals/test.out b/testsuite/gnat2goto/tests/case_statement_vals/test.out new file mode 100644 index 000000000..13f950fef --- /dev/null +++ b/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 diff --git a/testsuite/gnat2goto/tests/case_statement_vals/test.py b/testsuite/gnat2goto/tests/case_statement_vals/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/case_statement_vals/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove()