Remove erroneous Z in RFC epoch format const

Also remove the Kani visualizations -- if it fails I run it in VSCode or locally

Signed-off-by: Christopher Rabotin <[email protected]>

Author: ChristopherRabotin

.github/workflows/formal_verification.yml

@@ -37,7 +37,7 @@ jobs:
           # Remove `cdylib` from targets in Cargo.toml because it confuses Kani
           sed '17d' Cargo.toml > Cargo.toml.new
           mv Cargo.toml.new Cargo.toml
-          cargo kani | (cargo kani --visualize && exit 1) # Re-run for artifacts if it has failed.
+          cargo kani
 
       - name: Save formal verification artifacts
         uses: actions/upload-artifact@v3

src/efmt/consts.rs

@@ -176,7 +176,7 @@ pub const RFC3339: Format = Format {
         Some(Item {
             token: Token::Second,
             sep_char: Some('.'),
-            second_sep_char: Some('Z'),
+            second_sep_char: None,
             optional: false,
         }),
         Some(Item {

src/efmt/format.rs

@@ -185,6 +185,10 @@ impl Format {
                         ts = TimeScale::from_str(s[idx..].trim())?;
                     }
                     break;
+                } else if char == 'Z' {
+                    // This is a single character to represent UTC
+                    // UTC is the default time scale, so we don't need to do anything.
+                    break;
                 }
                 prev_item = cur_item;
                 prev_token = cur_token;

tests/epoch.rs

@@ -1803,7 +1803,7 @@ fn test_epoch_formatter() {
     let init_str = "1994-11-05T08:15:30-05:00";
     let e = Epoch::from_str(init_str).unwrap();
 
-    let fmt = Format::from_str("%Y-%m-%dT%H:%M:%S.Z%f%z").unwrap();
+    let fmt = Format::from_str("%Y-%m-%dT%H:%M:%S.%f%z").unwrap();
     assert_eq!(fmt, RFC3339);
 
     let fmtd = Formatter::with_timezone(e, Duration::from_str("-05:00").unwrap(), RFC3339_FLEX);