Merge branch 'main' into kk-fix-scatterplot-crash

library/std/src/lib.rs

@@ -135,14 +135,14 @@ macro_rules! eprint {
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! println {
-    () => { };
+    () => { $crate::print!("\n") };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! eprintln {
-    () => { };
+    () => { $crate::eprint!("\n") };
     ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
 }
 

tests/kani/Print/no_semicolon.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that the (e)println with no arguments do not require a trailing semicolon
+
+fn println() {
+    println!()
+}
+fn eprintln() {
+    eprintln!()
+}
+
+#[kani::proof]
+fn main() {
+    println();
+    eprintln();
+}