1use std::collections::HashMap;
12use std::path::PathBuf;
13
14use clap::ValueEnum;
15use serde::{Deserialize, Serialize};
16
17#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, Default)]
32#[serde(rename_all = "snake_case")]
33pub enum Confidence {
34 High,
36 #[default]
38 Medium,
39 Low,
41}
42
43impl std::fmt::Display for Confidence {
44 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45 match self {
46 Self::High => write!(f, "high"),
47 Self::Medium => write!(f, "medium"),
48 Self::Low => write!(f, "low"),
49 }
50 }
51}
52
53#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
72pub struct Condition {
73 pub variable: String,
75
76 pub constraint: String,
78
79 pub source_line: u32,
81
82 pub confidence: Confidence,
84}
85
86impl Condition {
87 pub fn high(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
89 Self {
90 variable: variable.into(),
91 constraint: constraint.into(),
92 source_line: line,
93 confidence: Confidence::High,
94 }
95 }
96
97 pub fn medium(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
99 Self {
100 variable: variable.into(),
101 constraint: constraint.into(),
102 source_line: line,
103 confidence: Confidence::Medium,
104 }
105 }
106
107 pub fn low(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
109 Self {
110 variable: variable.into(),
111 constraint: constraint.into(),
112 source_line: line,
113 confidence: Confidence::Low,
114 }
115 }
116}
117
118#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
130#[serde(rename_all = "snake_case")]
131pub enum InvariantKind {
132 Type,
134 NonNull,
136 NonNegative,
138 Positive,
140 Range,
142 Relation,
144 Length,
146}
147
148impl std::fmt::Display for InvariantKind {
149 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
150 match self {
151 Self::Type => write!(f, "type"),
152 Self::NonNull => write!(f, "non_null"),
153 Self::NonNegative => write!(f, "non_negative"),
154 Self::Positive => write!(f, "positive"),
155 Self::Range => write!(f, "range"),
156 Self::Relation => write!(f, "relation"),
157 Self::Length => write!(f, "length"),
158 }
159 }
160}
161
162#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
167pub struct Invariant {
168 pub variable: String,
170
171 pub kind: InvariantKind,
173
174 pub expression: String,
176
177 pub confidence: Confidence,
179
180 pub observations: u32,
182
183 pub counterexample_count: u32,
185}
186
187#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
195pub struct InputOutputSpec {
196 pub function: String,
198
199 pub inputs: Vec<serde_json::Value>,
201
202 pub output: serde_json::Value,
204
205 pub test_function: String,
207
208 pub line: u32,
210
211 pub confidence: Confidence,
213}
214
215#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
219pub struct ExceptionSpec {
220 pub function: String,
222
223 pub inputs: Vec<serde_json::Value>,
225
226 pub exception_type: String,
228
229 pub match_pattern: Option<String>,
231
232 pub test_function: String,
234
235 pub line: u32,
237
238 pub confidence: Confidence,
240}
241
242#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
246pub struct PropertySpec {
247 pub function: String,
249
250 pub property_type: String,
252
253 pub constraint: String,
255
256 pub test_function: String,
258
259 pub line: u32,
261
262 pub confidence: Confidence,
264}
265
266#[derive(Debug, Clone, Copy, PartialEq)]
281pub struct Interval {
282 pub lo: f64,
284
285 pub hi: f64,
287}
288
289impl Serialize for Interval {
291 fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
292 where
293 S: serde::Serializer,
294 {
295 use serde::ser::SerializeStruct;
296 let mut state = serializer.serialize_struct("Interval", 2)?;
297
298 if self.lo == f64::NEG_INFINITY {
300 state.serialize_field("lo", "-inf")?;
301 } else if self.lo == f64::INFINITY {
302 state.serialize_field("lo", "+inf")?;
303 } else if self.lo.is_nan() {
304 state.serialize_field("lo", "NaN")?;
305 } else {
306 state.serialize_field("lo", &self.lo)?;
307 }
308
309 if self.hi == f64::NEG_INFINITY {
311 state.serialize_field("hi", "-inf")?;
312 } else if self.hi == f64::INFINITY {
313 state.serialize_field("hi", "+inf")?;
314 } else if self.hi.is_nan() {
315 state.serialize_field("hi", "NaN")?;
316 } else {
317 state.serialize_field("hi", &self.hi)?;
318 }
319
320 state.end()
321 }
322}
323
324impl<'de> Deserialize<'de> for Interval {
326 fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
327 where
328 D: serde::Deserializer<'de>,
329 {
330 #[derive(Deserialize)]
331 struct IntervalHelper {
332 lo: serde_json::Value,
333 hi: serde_json::Value,
334 }
335
336 let helper = IntervalHelper::deserialize(deserializer)?;
337
338 fn parse_bound(v: serde_json::Value) -> Result<f64, String> {
339 match v {
340 serde_json::Value::Number(n) => {
341 n.as_f64().ok_or_else(|| "invalid number".to_string())
342 }
343 serde_json::Value::String(s) => match s.as_str() {
344 "-inf" | "-Infinity" => Ok(f64::NEG_INFINITY),
345 "+inf" | "inf" | "Infinity" => Ok(f64::INFINITY),
346 "NaN" => Ok(f64::NAN),
347 _ => s.parse::<f64>().map_err(|e| e.to_string()),
348 },
349 serde_json::Value::Null => Ok(f64::INFINITY), _ => Err("expected number or string".to_string()),
351 }
352 }
353
354 let lo = parse_bound(helper.lo).map_err(serde::de::Error::custom)?;
355 let hi = parse_bound(helper.hi).map_err(serde::de::Error::custom)?;
356
357 Ok(Interval { lo, hi })
358 }
359}
360
361impl Interval {
362 pub fn const_val(n: f64) -> Self {
364 Self { lo: n, hi: n }
365 }
366
367 pub fn top() -> Self {
369 Self {
370 lo: f64::NEG_INFINITY,
371 hi: f64::INFINITY,
372 }
373 }
374
375 pub fn bottom() -> Self {
377 Self {
378 lo: f64::INFINITY,
379 hi: f64::NEG_INFINITY,
380 }
381 }
382
383 pub fn is_bottom(&self) -> bool {
385 self.lo > self.hi
386 }
387
388 pub fn is_top(&self) -> bool {
390 self.lo == f64::NEG_INFINITY && self.hi == f64::INFINITY
391 }
392
393 pub fn contains(&self, n: f64) -> bool {
395 !self.is_bottom() && self.lo <= n && n <= self.hi
396 }
397
398 pub fn contains_zero(&self) -> bool {
400 self.contains(0.0)
401 }
402
403 pub fn join(&self, other: &Self) -> Self {
407 if self.is_bottom() {
408 return *other;
409 }
410 if other.is_bottom() {
411 return *self;
412 }
413 Self {
414 lo: self.lo.min(other.lo),
415 hi: self.hi.max(other.hi),
416 }
417 }
418
419 pub fn meet(&self, other: &Self) -> Self {
423 if self.is_bottom() || other.is_bottom() {
424 return Self::bottom();
425 }
426 Self {
428 lo: self.lo.max(other.lo),
429 hi: self.hi.min(other.hi),
430 }
431 }
432
433 pub fn widen(&self, other: &Self) -> Self {
438 if self.is_bottom() {
439 return *other;
440 }
441 if other.is_bottom() {
442 return *self;
443 }
444 Self {
445 lo: if other.lo < self.lo {
446 f64::NEG_INFINITY
447 } else {
448 self.lo
449 },
450 hi: if other.hi > self.hi {
451 f64::INFINITY
452 } else {
453 self.hi
454 },
455 }
456 }
457
458 pub fn add(&self, other: &Self) -> Self {
460 if self.is_bottom() || other.is_bottom() {
461 return Self::bottom();
462 }
463 Self {
464 lo: self.lo + other.lo,
465 hi: self.hi + other.hi,
466 }
467 }
468
469 pub fn sub(&self, other: &Self) -> Self {
471 if self.is_bottom() || other.is_bottom() {
472 return Self::bottom();
473 }
474 Self {
475 lo: self.lo - other.hi,
476 hi: self.hi - other.lo,
477 }
478 }
479
480 pub fn mul(&self, other: &Self) -> Self {
484 if self.is_bottom() || other.is_bottom() {
485 return Self::bottom();
486 }
487 let products = [
489 self.lo * other.lo,
490 self.lo * other.hi,
491 self.hi * other.lo,
492 self.hi * other.hi,
493 ];
494 Self {
495 lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
496 hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
497 }
498 }
499
500 pub fn div(&self, other: &Self) -> (Self, bool) {
505 if self.is_bottom() || other.is_bottom() {
506 return (Self::bottom(), false);
507 }
508
509 let may_div_zero = other.contains_zero();
510
511 if other.lo == 0.0 && other.hi == 0.0 {
513 return (Self::bottom(), true);
514 }
515
516 if may_div_zero {
518 return (Self::top(), true);
520 }
521
522 let products = [
524 self.lo / other.lo,
525 self.lo / other.hi,
526 self.hi / other.lo,
527 self.hi / other.hi,
528 ];
529 (
530 Self {
531 lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
532 hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
533 },
534 false,
535 )
536 }
537
538 pub fn neg(&self) -> Self {
540 if self.is_bottom() {
541 return Self::bottom();
542 }
543 Self {
544 lo: -self.hi,
545 hi: -self.lo,
546 }
547 }
548}
549
550impl Default for Interval {
551 fn default() -> Self {
552 Self::top()
553 }
554}
555
556impl std::fmt::Display for Interval {
557 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
558 if self.is_bottom() {
559 write!(f, "bottom")
560 } else if self.is_top() {
561 write!(f, "(-inf, +inf)")
562 } else if self.lo == self.hi {
563 write!(f, "[{}]", self.lo)
564 } else {
565 let lo_str = if self.lo == f64::NEG_INFINITY {
566 "-inf".to_string()
567 } else {
568 self.lo.to_string()
569 };
570 let hi_str = if self.hi == f64::INFINITY {
571 "+inf".to_string()
572 } else {
573 self.hi.to_string()
574 };
575 write!(f, "[{}, {}]", lo_str, hi_str)
576 }
577 }
578}
579
580#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
588pub struct DeadStore {
589 pub variable: String,
591
592 pub ssa_name: String,
594
595 pub line: u32,
597
598 pub block_id: u32,
600
601 pub is_phi: bool,
603}
604
605impl DeadStore {
606 pub fn to_dict(&self) -> serde_json::Value {
608 serde_json::json!({
609 "variable": self.variable,
610 "ssa_name": self.ssa_name,
611 "line": self.line,
612 "block_id": self.block_id,
613 "is_phi": self.is_phi,
614 })
615 }
616}
617
618#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
627pub struct ChopResult {
628 pub lines: Vec<u32>,
630
631 pub count: u32,
633
634 pub source_line: u32,
636
637 pub target_line: u32,
639
640 pub path_exists: bool,
642
643 pub function: String,
645
646 pub explanation: Option<String>,
648}
649
650impl ChopResult {
651 pub fn same_line(line: u32, function: impl Into<String>) -> Self {
653 Self {
654 lines: vec![line],
655 count: 1,
656 source_line: line,
657 target_line: line,
658 path_exists: true,
659 function: function.into(),
660 explanation: Some(format!("Source and target are the same line ({}).", line)),
661 }
662 }
663
664 pub fn no_path(source: u32, target: u32, function: impl Into<String>) -> Self {
666 Self {
667 lines: vec![],
668 count: 0,
669 source_line: source,
670 target_line: target,
671 path_exists: false,
672 function: function.into(),
673 explanation: Some(format!(
674 "No dependency path from line {} to line {}. \
675 The source line does not affect the target line.",
676 source, target
677 )),
678 }
679 }
680}
681
682#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
690pub struct IntervalWarning {
691 pub line: u32,
693
694 pub kind: String,
696
697 pub variable: String,
699
700 pub bounds: Interval,
702
703 pub message: String,
705}
706
707#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
713pub struct ContractsReport {
714 pub function: String,
716
717 pub file: PathBuf,
719
720 pub preconditions: Vec<Condition>,
722
723 pub postconditions: Vec<Condition>,
725
726 pub invariants: Vec<Condition>,
728}
729
730#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
732pub struct FunctionInvariants {
733 pub function_name: String,
735
736 pub preconditions: Vec<Invariant>,
738
739 pub postconditions: Vec<Invariant>,
741
742 pub observation_count: u32,
744}
745
746#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
748pub struct InvariantsSummary {
749 pub total_observations: u32,
751
752 pub total_invariants: u32,
754
755 pub by_kind: HashMap<String, u32>,
757}
758
759#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
761pub struct InvariantsReport {
762 pub functions: Vec<FunctionInvariants>,
764
765 pub summary: InvariantsSummary,
767}
768
769#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
771pub struct FunctionSpecs {
772 pub function_name: String,
774
775 pub summary: String,
777
778 pub test_count: u32,
780
781 pub input_output_specs: Vec<InputOutputSpec>,
783
784 pub exception_specs: Vec<ExceptionSpec>,
786
787 pub property_specs: Vec<PropertySpec>,
789}
790
791#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
793pub struct SpecsByType {
794 pub input_output: u32,
796
797 pub exception: u32,
799
800 pub property: u32,
802}
803
804#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
806pub struct SpecsSummary {
807 pub total_specs: u32,
809
810 pub by_type: SpecsByType,
812
813 pub test_functions_scanned: u32,
815
816 pub test_files_scanned: u32,
818
819 pub functions_found: u32,
821}
822
823#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
825pub struct SpecsReport {
826 pub functions: Vec<FunctionSpecs>,
828
829 pub summary: SpecsSummary,
831}
832
833#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
835pub struct BoundsResult {
836 pub function: String,
838
839 pub bounds: HashMap<u32, HashMap<String, Interval>>,
841
842 pub warnings: Vec<IntervalWarning>,
844
845 pub converged: bool,
847
848 pub iterations: u32,
850}
851
852#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
854pub struct DeadStoresReport {
855 pub function: String,
857
858 pub file: PathBuf,
860
861 pub dead_stores_ssa: Vec<DeadStore>,
863
864 pub count: u32,
866
867 pub dead_stores_live_vars: Option<Vec<DeadStore>>,
869
870 pub live_vars_count: Option<u32>,
872}
873
874#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
876#[serde(rename_all = "snake_case")]
877pub enum SubAnalysisStatus {
878 Success,
880 Partial,
882 Failed,
884 Skipped,
886}
887
888impl SubAnalysisStatus {
889 pub fn is_success(&self) -> bool {
891 matches!(self, Self::Success | Self::Partial)
892 }
893}
894
895#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
897pub struct SubAnalysisResult {
898 pub name: String,
900
901 pub status: SubAnalysisStatus,
903
904 pub items_found: u32,
906
907 pub elapsed_ms: u64,
909
910 pub error: Option<String>,
912
913 pub data: Option<serde_json::Value>,
915}
916
917impl SubAnalysisResult {
918 pub fn success(&self) -> bool {
920 self.status.is_success()
921 }
922}
923
924#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
926pub struct CoverageInfo {
927 pub constrained_functions: u32,
929
930 pub total_functions: u32,
932
933 pub coverage_pct: f64,
935}
936
937#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
939pub struct VerifySummary {
940 pub spec_count: u32,
942
943 pub invariant_count: u32,
945
946 pub contract_count: u32,
948
949 pub annotated_count: u32,
951
952 pub behavioral_count: u32,
954
955 pub pattern_count: u32,
957
958 pub pattern_high_confidence: u32,
960
961 pub coverage: CoverageInfo,
963}
964
965#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
967pub struct VerifyReport {
968 pub path: PathBuf,
970
971 pub sub_results: HashMap<String, SubAnalysisResult>,
973
974 pub summary: VerifySummary,
976
977 pub total_elapsed_ms: u64,
979
980 pub files_analyzed: u32,
982
983 pub files_failed: u32,
985
986 pub partial_results: bool,
988}
989
990#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
996pub enum OutputFormat {
997 #[default]
999 Json,
1000
1001 Text,
1003}
1004
1005impl std::fmt::Display for OutputFormat {
1006 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
1007 match self {
1008 Self::Json => write!(f, "json"),
1009 Self::Text => write!(f, "text"),
1010 }
1011 }
1012}
1013
1014#[cfg(test)]
1019mod tests {
1020 use super::*;
1021
1022 #[test]
1027 fn test_confidence_enum_serialization() {
1028 assert_eq!(
1029 serde_json::to_string(&Confidence::High).unwrap(),
1030 "\"high\""
1031 );
1032 assert_eq!(
1033 serde_json::to_string(&Confidence::Medium).unwrap(),
1034 "\"medium\""
1035 );
1036 assert_eq!(serde_json::to_string(&Confidence::Low).unwrap(), "\"low\"");
1037 }
1038
1039 #[test]
1040 fn test_confidence_enum_deserialization() {
1041 assert_eq!(
1042 serde_json::from_str::<Confidence>("\"high\"").unwrap(),
1043 Confidence::High
1044 );
1045 assert_eq!(
1046 serde_json::from_str::<Confidence>("\"medium\"").unwrap(),
1047 Confidence::Medium
1048 );
1049 assert_eq!(
1050 serde_json::from_str::<Confidence>("\"low\"").unwrap(),
1051 Confidence::Low
1052 );
1053 }
1054
1055 #[test]
1056 fn test_confidence_default() {
1057 assert_eq!(Confidence::default(), Confidence::Medium);
1058 }
1059
1060 #[test]
1065 fn test_condition_struct_fields() {
1066 let cond = Condition::high("x", "x >= 0", 10);
1067 assert_eq!(cond.variable, "x");
1068 assert_eq!(cond.constraint, "x >= 0");
1069 assert_eq!(cond.source_line, 10);
1070 assert_eq!(cond.confidence, Confidence::High);
1071 }
1072
1073 #[test]
1074 fn test_condition_serialization() {
1075 let cond = Condition::high("x", "x >= 0", 10);
1076 let json = serde_json::to_string(&cond).unwrap();
1077 assert!(json.contains("\"variable\":\"x\""));
1078 assert!(json.contains("\"confidence\":\"high\""));
1079 }
1080
1081 #[test]
1086 fn test_interval_const_val() {
1087 let i = Interval::const_val(5.0);
1088 assert_eq!(i.lo, 5.0);
1089 assert_eq!(i.hi, 5.0);
1090 assert!(i.contains(5.0));
1091 assert!(!i.contains(4.0));
1092 assert!(!i.contains(6.0));
1093 }
1094
1095 #[test]
1096 fn test_interval_basic_operations() {
1097 let i = Interval { lo: 0.0, hi: 10.0 };
1098 assert!(i.contains(0.0));
1099 assert!(i.contains(5.0));
1100 assert!(i.contains(10.0));
1101 assert!(!i.contains(-1.0));
1102 assert!(!i.contains(11.0));
1103 }
1104
1105 #[test]
1106 fn test_interval_bottom_top_detection() {
1107 assert!(Interval::bottom().is_bottom());
1108 assert!(!Interval::top().is_bottom());
1109 assert!(Interval::top().is_top());
1110 assert!(!Interval::bottom().is_top());
1111 assert!(!Interval::const_val(5.0).is_bottom());
1112 assert!(!Interval::const_val(5.0).is_top());
1113 }
1114
1115 #[test]
1116 fn test_interval_contains_zero() {
1117 assert!(Interval { lo: -5.0, hi: 5.0 }.contains_zero());
1118 assert!(Interval { lo: 0.0, hi: 10.0 }.contains_zero());
1119 assert!(Interval { lo: -10.0, hi: 0.0 }.contains_zero());
1120 assert!(!Interval { lo: 1.0, hi: 10.0 }.contains_zero());
1121 assert!(!Interval {
1122 lo: -10.0,
1123 hi: -1.0
1124 }
1125 .contains_zero());
1126 }
1127
1128 #[test]
1129 fn test_interval_join() {
1130 let a = Interval { lo: 0.0, hi: 5.0 };
1131 let b = Interval { lo: 3.0, hi: 10.0 };
1132 let joined = a.join(&b);
1133 assert_eq!(joined.lo, 0.0);
1134 assert_eq!(joined.hi, 10.0);
1135 }
1136
1137 #[test]
1138 fn test_interval_meet() {
1139 let a = Interval { lo: 0.0, hi: 5.0 };
1140 let b = Interval { lo: 3.0, hi: 10.0 };
1141 let met = a.meet(&b);
1142 assert_eq!(met.lo, 3.0);
1143 assert_eq!(met.hi, 5.0);
1144 }
1145
1146 #[test]
1147 fn test_interval_add() {
1148 let a = Interval { lo: 1.0, hi: 5.0 };
1149 let b = Interval { lo: 2.0, hi: 3.0 };
1150 let sum = a.add(&b);
1151 assert_eq!(sum.lo, 3.0);
1152 assert_eq!(sum.hi, 8.0);
1153 }
1154
1155 #[test]
1156 fn test_interval_sub() {
1157 let a = Interval { lo: 5.0, hi: 10.0 };
1158 let b = Interval { lo: 1.0, hi: 3.0 };
1159 let diff = a.sub(&b);
1160 assert_eq!(diff.lo, 2.0); assert_eq!(diff.hi, 9.0); }
1163
1164 #[test]
1165 fn test_interval_mul() {
1166 let a = Interval { lo: 2.0, hi: 3.0 };
1167 let b = Interval { lo: 4.0, hi: 5.0 };
1168 let prod = a.mul(&b);
1169 assert_eq!(prod.lo, 8.0);
1170 assert_eq!(prod.hi, 15.0);
1171 }
1172
1173 #[test]
1174 fn test_interval_mul_negative() {
1175 let a = Interval { lo: -2.0, hi: 3.0 };
1176 let b = Interval { lo: -1.0, hi: 2.0 };
1177 let prod = a.mul(&b);
1178 assert_eq!(prod.lo, -4.0);
1180 assert_eq!(prod.hi, 6.0);
1181 }
1182
1183 #[test]
1184 fn test_interval_div() {
1185 let a = Interval { lo: 10.0, hi: 20.0 };
1186 let b = Interval { lo: 2.0, hi: 5.0 };
1187 let (quot, div_zero) = a.div(&b);
1188 assert!(!div_zero);
1189 assert_eq!(quot.lo, 2.0); assert_eq!(quot.hi, 10.0); }
1192
1193 #[test]
1194 fn test_interval_div_by_zero() {
1195 let a = Interval { lo: 10.0, hi: 20.0 };
1196 let b = Interval { lo: -1.0, hi: 1.0 }; let (_, div_zero) = a.div(&b);
1198 assert!(div_zero);
1199 }
1200
1201 #[test]
1202 fn test_interval_widen() {
1203 let a = Interval { lo: 0.0, hi: 10.0 };
1204 let b = Interval { lo: -5.0, hi: 15.0 };
1205 let widened = a.widen(&b);
1206 assert_eq!(widened.lo, f64::NEG_INFINITY);
1207 assert_eq!(widened.hi, f64::INFINITY);
1208 }
1209
1210 #[test]
1215 fn test_dead_store_struct() {
1216 let ds = DeadStore {
1217 variable: "x".to_string(),
1218 ssa_name: "x_2".to_string(),
1219 line: 10,
1220 block_id: 1,
1221 is_phi: false,
1222 };
1223 assert_eq!(ds.variable, "x");
1224 assert_eq!(ds.ssa_name, "x_2");
1225 assert_eq!(ds.line, 10);
1226 assert!(!ds.is_phi);
1227 }
1228
1229 #[test]
1230 fn test_dead_store_serialization() {
1231 let ds = DeadStore {
1232 variable: "x".to_string(),
1233 ssa_name: "x_2".to_string(),
1234 line: 10,
1235 block_id: 1,
1236 is_phi: false,
1237 };
1238 let json = serde_json::to_string(&ds).unwrap();
1239 assert!(json.contains("\"variable\":\"x\""));
1240 assert!(json.contains("\"ssa_name\":\"x_2\""));
1241 }
1242
1243 #[test]
1248 fn test_chop_result_struct() {
1249 let result = ChopResult {
1250 lines: vec![2, 3, 4],
1251 count: 3,
1252 source_line: 2,
1253 target_line: 4,
1254 path_exists: true,
1255 function: "example".to_string(),
1256 explanation: Some("Found path".to_string()),
1257 };
1258 assert_eq!(result.count, 3);
1259 assert!(result.path_exists);
1260 }
1261
1262 #[test]
1263 fn test_chop_result_same_line() {
1264 let result = ChopResult::same_line(5, "test_func");
1265 assert_eq!(result.lines, vec![5]);
1266 assert_eq!(result.count, 1);
1267 assert!(result.path_exists);
1268 }
1269
1270 #[test]
1271 fn test_chop_result_no_path() {
1272 let result = ChopResult::no_path(2, 10, "test_func");
1273 assert!(result.lines.is_empty());
1274 assert_eq!(result.count, 0);
1275 assert!(!result.path_exists);
1276 }
1277
1278 #[test]
1283 fn test_contracts_report_struct() {
1284 let report = ContractsReport {
1285 function: "process_data".to_string(),
1286 file: PathBuf::from("test.py"),
1287 preconditions: vec![Condition::high("x", "x >= 0", 10)],
1288 postconditions: vec![],
1289 invariants: vec![],
1290 };
1291 assert_eq!(report.function, "process_data");
1292 assert_eq!(report.preconditions.len(), 1);
1293 }
1294
1295 #[test]
1300 fn test_invariant_kind_serialization() {
1301 assert_eq!(
1302 serde_json::to_string(&InvariantKind::Type).unwrap(),
1303 "\"type\""
1304 );
1305 assert_eq!(
1306 serde_json::to_string(&InvariantKind::NonNull).unwrap(),
1307 "\"non_null\""
1308 );
1309 assert_eq!(
1310 serde_json::to_string(&InvariantKind::NonNegative).unwrap(),
1311 "\"non_negative\""
1312 );
1313 }
1314
1315 #[test]
1320 fn test_output_format_default() {
1321 assert_eq!(OutputFormat::default(), OutputFormat::Json);
1322 }
1323
1324 #[test]
1325 fn test_output_format_display() {
1326 assert_eq!(OutputFormat::Json.to_string(), "json");
1327 assert_eq!(OutputFormat::Text.to_string(), "text");
1328 }
1329}