Convert conc. playback int. values into ASCII

adpaco-aws · Sep 12, 2023 · 113482f · 113482f
1 parent 72a5e7a
commit 113482f
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 5 deletions.
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
@@ -380,10 +380,22 @@ mod concrete_vals_extractor {
                         next_num.push(next_byte);
                     }
 
-                    return Some(ConcreteVal {
-                        byte_arr: next_num,
-                        interp_val: interp_concrete_val.to_string(),
-                    });
+                    // In ARM64 Linux, CBMC will produce a character instead of a number for
+                    // interpreted values because the char type is unsigned in that platform.
+                    // For example, for the value `101` it will produce `'e'` instead of `101`.
+                    // To correct this, we check if the value starts and ends with `'`, and
+                    // convert the character into its ASCII value in that case.
+                    let interp_val = {
+                        let interp_val_str = interp_concrete_val.to_string();
+                        if interp_val_str.starts_with("\'") && interp_val_str.ends_with("\'") {
+                            let interp_num = interp_val_str.chars().nth(1).unwrap() as u8;
+                            interp_num.to_string()
+                        } else {
+                            interp_val_str
+                        }
+                    };
+
+                    return Some(ConcreteVal { byte_arr: next_num, interp_val: interp_val });
                 }
             }
         }

diff --git a/tests/ui/concrete-playback/i8/expected b/tests/ui/concrete-playback/i8/expected
@@ -11,7 +11,7 @@ fn kani_concrete_playback_harness
         vec![155],
         // 0
         vec![0],
-        // 'e'
+        // 101
         vec![101],
         // 127
         vec![127]