Merge pull request #261 from tjj2017/char_subtype

Add a failing test for a character subtype

Author: chrisr-diffblue

testsuite/gnat2goto/tests/character_subtype/char_subtype.adb

@@ -0,0 +1,8 @@
+procedure Char_Subtype is
+   subtype Capitals is Character range 'A' .. 'Z';
+
+   Var_C : Capitals;
+begin
+   Var_C := 'C';
+   pragma Assert (Var_C in Capitals);
+end Char_Subtype;

testsuite/gnat2goto/tests/character_subtype/test.opt

@@ -0,0 +1 @@
+ALL XFAIL gnat2goto reports invalid range types and cbmc fails with an invariant violation

testsuite/gnat2goto/tests/character_subtype/test.out

@@ -0,0 +1,60 @@
+Standard_Output from gnat2goto char_subtype:
+N_Character_Literal "QU41" (Node_Id=2264) (source,analyzed)
+ Parent = N_Range (Node_Id=2265)
+ Sloc = 12353  char_subtype.adb:2:40
+ Chars = "QU41" (Name_Id=300001450)
+ Is_Static_Expression = True
+ Etype = N_Defining_Identifier "character" (Entity_Id=100s)
+ Char_Literal_Value = 65 (Uint = 600032833)
+N_Character_Literal "QU5a" (Node_Id=2266) (source,analyzed)
+ Parent = N_Range (Node_Id=2265)
+ Sloc = 12360  char_subtype.adb:2:47
+ Chars = "QU5a" (Name_Id=300001451)
+ Is_Static_Expression = True
+ Etype = N_Defining_Identifier "character" (Entity_Id=100s)
+ Char_Literal_Value = 90 (Uint = 600032858)
+N_In (Node_Id=2286) (source,analyzed)
+ Parent = N_Pragma_Argument_Association <No_Name> (Node_Id=2290)
+ Sloc = 12434  char_subtype.adb:7:25
+ Left_Opnd = N_Identifier "var_c" (Node_Id=2283)
+ Right_Opnd = N_Identifier "capitals" (Node_Id=2285)
+ Etype = N_Defining_Identifier "boolean" (Entity_Id=16s)
+
+Standard_Error from gnat2goto char_subtype:
+----------At: Do_Base_Range_Constraint----------
+----------unsupported lower range kind----------
+----------At: Do_Base_Range_Constraint----------
+----------unsupported upper range kind----------
+----------At: Do_Expression----------
+----------In----------
+
+Error from cbmc char_subtype:
+--- begin invariant violation report ---
+Invariant check failed
+File: symex_assign.cpp:35 function: symex_assign
+Condition: lhs.type() == rhs.type()
+Reason: assignments must be type consistent
+Backtrace:
+0   cbmc                                0x0000000108a5edba _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
+1   cbmc                                0x0000000108a5f38c _Z13get_backtracev + 252
+2   cbmc                                0x000000010880b6ac _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
+3   cbmc                                0x00000001087cf784 _ZN11goto_symext12symex_assignER17goto_symex_statetRK12code_assignt + 1236
+4   cbmc                                0x00000001087f0e6e _ZN11goto_symext24execute_next_instructionERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 718
+5   cbmc                                0x00000001087f0b2a _ZN11goto_symext10symex_stepERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 42
+6   cbmc                                0x00000001086db94c _ZN10symex_bmct10symex_stepERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER17goto_symex_statet + 588
+7   cbmc                                0x00000001087ee80d _ZN11goto_symext19symex_threaded_stepER17goto_symex_statetRKNSt3__18functionIFRK14goto_functiontRK8dstringtEEE + 29
+8   cbmc                                0x00000001087eeb3f _ZN11goto_symext16symex_with_stateER17goto_symex_statetRKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER13symbol_tablet + 191
+9   cbmc                                0x00000001087efadd _ZN11goto_symext25symex_from_entry_point_ofERKNSt3__18functionIFRK14goto_functiontRK8dstringtEEER13symbol_tablet + 61
+10  cbmc                                0x00000001086c69ea _ZN30multi_path_symex_only_checkert17generate_equationEv + 74
+11  cbmc                                0x00000001086c5303 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 83
+12  cbmc                                0x0000000108ae8e64 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 52
+13  cbmc                                0x0000000108ae176d _ZN19cbmc_parse_optionst4doitEv + 4125
+14  cbmc                                0x0000000108a77619 _ZN19parse_options_baset4mainEv + 249
+15  cbmc                                0x0000000108add09d main + 45
+16  libdyld.dylib                       0x00007fff7c363015 start + 1
+
+
+--- end invariant violation report ---
+
+ERROR code  -6 returned by cbmc when processing char_subtype
+

testsuite/gnat2goto/tests/character_subtype/test.py

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