Add CI regression run for the write_goto_binary

Modified `call_single_file.rs` so that write_goto_binary
can be enabled by defining the KANI_ENABLE_WRITE_GOTO_BINARY
env variable.

.github/workflows/kani.yml

@@ -33,6 +33,25 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
+  write-goto-binary-regression:
+    runs-on: ubuntu-20.04
+    env:
+      KANI_ENABLE_WRITE_GOTO_BINARY: 1
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-20.04
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh
+
   experimental-features-regression:
     runs-on: ubuntu-20.04
     env:

kani-driver/src/call_single_file.rs

@@ -68,6 +68,13 @@ impl KaniSession {
     pub fn kani_compiler_flags(&self) -> Vec<String> {
         let mut flags = vec![];
 
+        // Read write_goto_binary option from env
+        let env_var = "KANI_ENABLE_WRITE_GOTO_BINARY";
+        let enable_write_goto_binary = match std::env::var_os(env_var) {
+            Some(str) => !str.is_empty() && str != "0",
+            None => false,
+        };
+
         if self.args.debug {
             flags.push("--log-level=debug".into());
         } else if self.args.verbose {
@@ -86,7 +93,7 @@ impl KaniSession {
         if self.args.ignore_global_asm {
             flags.push("--ignore-global-asm".into());
         }
-        if self.args.write_goto_binary {
+        if self.args.write_goto_binary || enable_write_goto_binary {
             flags.push("--write-goto-binary".into());
         }
         if self.args.enable_stubbing {