diff --git a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs index 1368e30..0b243d0 100644 --- a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs +++ b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.expanded.rs @@ -73,7 +73,7 @@ pub fn test_edge_cases() { } } pub fn test_spec_with_method_calls() { - let expr = <[_]>::into_vec(::alloc::boxed::box_new([1, 2, 3])); + let expr = [1, 2, 3]; { let _rule_name = "method_check"; let _spec = expr.len() > 0; diff --git a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs index a5649d9..baeef2e 100644 --- a/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs +++ b/cvlr-macros/tests/expand/test_cvlr_rule_for_spec.rs @@ -115,7 +115,7 @@ pub fn test_edge_cases() { } pub fn test_spec_with_method_calls() { - let expr = vec![1, 2, 3]; + let expr = [1, 2, 3]; // Test with method calls in spec cvlr_rule_for_spec! { diff --git a/cvlr-spec/src/lib.rs b/cvlr-spec/src/lib.rs index 5af3123..2d535eb 100644 --- a/cvlr-spec/src/lib.rs +++ b/cvlr-spec/src/lib.rs @@ -1,3 +1,4 @@ +#![no_std] //! Specification language for CVL (Certora Verification Language) in Rust. //! //! This module provides a framework for writing specifications with preconditions