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 #[serde(default)]
635 pub file: String,
636
637 pub lines: Vec<u32>,
639
640 pub count: u32,
645
646 #[serde(default)]
653 pub line_count: u32,
654
655 pub source_line: u32,
657
658 pub target_line: u32,
660
661 pub path_exists: bool,
663
664 pub function: String,
666
667 pub explanation: Option<String>,
669}
670
671impl ChopResult {
672 pub fn same_line(line: u32, function: impl Into<String>) -> Self {
674 Self {
675 file: String::new(),
676 lines: vec![line],
677 count: 1,
678 line_count: 1,
679 source_line: line,
680 target_line: line,
681 path_exists: true,
682 function: function.into(),
683 explanation: Some(format!("Source and target are the same line ({}).", line)),
684 }
685 }
686
687 pub fn no_path(source: u32, target: u32, function: impl Into<String>) -> Self {
689 Self {
690 file: String::new(),
691 lines: vec![],
692 count: 0,
693 line_count: 0,
694 source_line: source,
695 target_line: target,
696 path_exists: false,
697 function: function.into(),
698 explanation: Some(format!(
699 "No dependency path from line {} to line {}. \
700 The source line does not affect the target line.",
701 source, target
702 )),
703 }
704 }
705}
706
707#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
715pub struct IntervalWarning {
716 pub line: u32,
718
719 pub kind: String,
721
722 pub variable: String,
724
725 pub bounds: Interval,
727
728 pub message: String,
730}
731
732#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
738pub struct ContractsReport {
739 pub function: String,
741
742 pub file: PathBuf,
744
745 pub preconditions: Vec<Condition>,
747
748 pub postconditions: Vec<Condition>,
750
751 pub invariants: Vec<Condition>,
753}
754
755#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
757pub struct FunctionInvariants {
758 pub function_name: String,
760
761 pub preconditions: Vec<Invariant>,
763
764 pub postconditions: Vec<Invariant>,
766
767 pub observation_count: u32,
769}
770
771#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
773pub struct InvariantsSummary {
774 pub total_observations: u32,
776
777 pub total_invariants: u32,
779
780 pub by_kind: HashMap<String, u32>,
782
783 #[serde(default)]
788 pub test_files_scanned: u32,
789
790 #[serde(default)]
794 pub test_functions_scanned: u32,
795}
796
797#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
799pub struct InvariantsReport {
800 pub functions: Vec<FunctionInvariants>,
802
803 pub summary: InvariantsSummary,
805}
806
807#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
809pub struct FunctionSpecs {
810 pub function_name: String,
812
813 pub summary: String,
815
816 pub test_count: u32,
818
819 pub input_output_specs: Vec<InputOutputSpec>,
821
822 pub exception_specs: Vec<ExceptionSpec>,
824
825 pub property_specs: Vec<PropertySpec>,
827}
828
829#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
831pub struct SpecsByType {
832 pub input_output: u32,
834
835 pub exception: u32,
837
838 pub property: u32,
840}
841
842#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
844pub struct SpecsSummary {
845 pub total_specs: u32,
847
848 pub by_type: SpecsByType,
850
851 pub test_functions_scanned: u32,
853
854 pub test_files_scanned: u32,
856
857 pub functions_found: u32,
859}
860
861#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
863pub struct SpecsReport {
864 pub functions: Vec<FunctionSpecs>,
866
867 pub summary: SpecsSummary,
869}
870
871#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
873pub struct BoundsResult {
874 pub function: String,
876
877 pub bounds: HashMap<u32, HashMap<String, Interval>>,
879
880 pub warnings: Vec<IntervalWarning>,
882
883 pub converged: bool,
885
886 pub iterations: u32,
888}
889
890#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
892pub struct DeadStoresReport {
893 pub function: String,
895
896 pub file: PathBuf,
898
899 pub dead_stores_ssa: Vec<DeadStore>,
901
902 pub count: u32,
904
905 pub dead_stores_live_vars: Option<Vec<DeadStore>>,
907
908 pub live_vars_count: Option<u32>,
910}
911
912#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
914#[serde(rename_all = "snake_case")]
915pub enum SubAnalysisStatus {
916 Success,
918 Partial,
920 Failed,
922 Skipped,
924}
925
926impl SubAnalysisStatus {
927 pub fn is_success(&self) -> bool {
929 matches!(self, Self::Success | Self::Partial)
930 }
931}
932
933#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
935pub struct SubAnalysisResult {
936 pub name: String,
938
939 pub status: SubAnalysisStatus,
941
942 pub items_found: u32,
944
945 pub elapsed_ms: u64,
947
948 pub error: Option<String>,
950
951 pub data: Option<serde_json::Value>,
953}
954
955impl SubAnalysisResult {
956 pub fn success(&self) -> bool {
958 self.status.is_success()
959 }
960}
961
962#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
974pub struct CoverageInfo {
975 pub constrained_functions: u32,
977
978 pub total_functions: u32,
982
983 pub coverage_pct: f64,
987
988 #[serde(default = "default_coverage_scope")]
992 pub scope: String,
993}
994
995fn default_coverage_scope() -> String {
997 "constraint-relevant functions (subset of all project functions; see verify docs)".to_string()
998}
999
1000#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
1002pub struct VerifySummary {
1003 pub spec_count: u32,
1005
1006 pub invariant_count: u32,
1008
1009 pub contract_count: u32,
1011
1012 pub annotated_count: u32,
1014
1015 pub behavioral_count: u32,
1017
1018 pub pattern_count: u32,
1020
1021 pub pattern_high_confidence: u32,
1023
1024 pub coverage: CoverageInfo,
1026}
1027
1028#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
1030pub struct VerifyReport {
1031 pub path: PathBuf,
1033
1034 pub sub_results: HashMap<String, SubAnalysisResult>,
1036
1037 pub summary: VerifySummary,
1039
1040 pub total_elapsed_ms: u64,
1042
1043 pub files_analyzed: u32,
1045
1046 pub files_failed: u32,
1048
1049 pub partial_results: bool,
1051}
1052
1053#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
1059pub enum OutputFormat {
1060 #[default]
1062 Json,
1063
1064 Text,
1066}
1067
1068impl std::fmt::Display for OutputFormat {
1069 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
1070 match self {
1071 Self::Json => write!(f, "json"),
1072 Self::Text => write!(f, "text"),
1073 }
1074 }
1075}
1076
1077#[cfg(test)]
1082mod tests {
1083 use super::*;
1084
1085 #[test]
1090 fn test_confidence_enum_serialization() {
1091 assert_eq!(
1092 serde_json::to_string(&Confidence::High).unwrap(),
1093 "\"high\""
1094 );
1095 assert_eq!(
1096 serde_json::to_string(&Confidence::Medium).unwrap(),
1097 "\"medium\""
1098 );
1099 assert_eq!(serde_json::to_string(&Confidence::Low).unwrap(), "\"low\"");
1100 }
1101
1102 #[test]
1103 fn test_confidence_enum_deserialization() {
1104 assert_eq!(
1105 serde_json::from_str::<Confidence>("\"high\"").unwrap(),
1106 Confidence::High
1107 );
1108 assert_eq!(
1109 serde_json::from_str::<Confidence>("\"medium\"").unwrap(),
1110 Confidence::Medium
1111 );
1112 assert_eq!(
1113 serde_json::from_str::<Confidence>("\"low\"").unwrap(),
1114 Confidence::Low
1115 );
1116 }
1117
1118 #[test]
1119 fn test_confidence_default() {
1120 assert_eq!(Confidence::default(), Confidence::Medium);
1121 }
1122
1123 #[test]
1128 fn test_condition_struct_fields() {
1129 let cond = Condition::high("x", "x >= 0", 10);
1130 assert_eq!(cond.variable, "x");
1131 assert_eq!(cond.constraint, "x >= 0");
1132 assert_eq!(cond.source_line, 10);
1133 assert_eq!(cond.confidence, Confidence::High);
1134 }
1135
1136 #[test]
1137 fn test_condition_serialization() {
1138 let cond = Condition::high("x", "x >= 0", 10);
1139 let json = serde_json::to_string(&cond).unwrap();
1140 assert!(json.contains("\"variable\":\"x\""));
1141 assert!(json.contains("\"confidence\":\"high\""));
1142 }
1143
1144 #[test]
1149 fn test_interval_const_val() {
1150 let i = Interval::const_val(5.0);
1151 assert_eq!(i.lo, 5.0);
1152 assert_eq!(i.hi, 5.0);
1153 assert!(i.contains(5.0));
1154 assert!(!i.contains(4.0));
1155 assert!(!i.contains(6.0));
1156 }
1157
1158 #[test]
1159 fn test_interval_basic_operations() {
1160 let i = Interval { lo: 0.0, hi: 10.0 };
1161 assert!(i.contains(0.0));
1162 assert!(i.contains(5.0));
1163 assert!(i.contains(10.0));
1164 assert!(!i.contains(-1.0));
1165 assert!(!i.contains(11.0));
1166 }
1167
1168 #[test]
1169 fn test_interval_bottom_top_detection() {
1170 assert!(Interval::bottom().is_bottom());
1171 assert!(!Interval::top().is_bottom());
1172 assert!(Interval::top().is_top());
1173 assert!(!Interval::bottom().is_top());
1174 assert!(!Interval::const_val(5.0).is_bottom());
1175 assert!(!Interval::const_val(5.0).is_top());
1176 }
1177
1178 #[test]
1179 fn test_interval_contains_zero() {
1180 assert!(Interval { lo: -5.0, hi: 5.0 }.contains_zero());
1181 assert!(Interval { lo: 0.0, hi: 10.0 }.contains_zero());
1182 assert!(Interval { lo: -10.0, hi: 0.0 }.contains_zero());
1183 assert!(!Interval { lo: 1.0, hi: 10.0 }.contains_zero());
1184 assert!(!Interval {
1185 lo: -10.0,
1186 hi: -1.0
1187 }
1188 .contains_zero());
1189 }
1190
1191 #[test]
1192 fn test_interval_join() {
1193 let a = Interval { lo: 0.0, hi: 5.0 };
1194 let b = Interval { lo: 3.0, hi: 10.0 };
1195 let joined = a.join(&b);
1196 assert_eq!(joined.lo, 0.0);
1197 assert_eq!(joined.hi, 10.0);
1198 }
1199
1200 #[test]
1201 fn test_interval_meet() {
1202 let a = Interval { lo: 0.0, hi: 5.0 };
1203 let b = Interval { lo: 3.0, hi: 10.0 };
1204 let met = a.meet(&b);
1205 assert_eq!(met.lo, 3.0);
1206 assert_eq!(met.hi, 5.0);
1207 }
1208
1209 #[test]
1210 fn test_interval_add() {
1211 let a = Interval { lo: 1.0, hi: 5.0 };
1212 let b = Interval { lo: 2.0, hi: 3.0 };
1213 let sum = a.add(&b);
1214 assert_eq!(sum.lo, 3.0);
1215 assert_eq!(sum.hi, 8.0);
1216 }
1217
1218 #[test]
1219 fn test_interval_sub() {
1220 let a = Interval { lo: 5.0, hi: 10.0 };
1221 let b = Interval { lo: 1.0, hi: 3.0 };
1222 let diff = a.sub(&b);
1223 assert_eq!(diff.lo, 2.0); assert_eq!(diff.hi, 9.0); }
1226
1227 #[test]
1228 fn test_interval_mul() {
1229 let a = Interval { lo: 2.0, hi: 3.0 };
1230 let b = Interval { lo: 4.0, hi: 5.0 };
1231 let prod = a.mul(&b);
1232 assert_eq!(prod.lo, 8.0);
1233 assert_eq!(prod.hi, 15.0);
1234 }
1235
1236 #[test]
1237 fn test_interval_mul_negative() {
1238 let a = Interval { lo: -2.0, hi: 3.0 };
1239 let b = Interval { lo: -1.0, hi: 2.0 };
1240 let prod = a.mul(&b);
1241 assert_eq!(prod.lo, -4.0);
1243 assert_eq!(prod.hi, 6.0);
1244 }
1245
1246 #[test]
1247 fn test_interval_div() {
1248 let a = Interval { lo: 10.0, hi: 20.0 };
1249 let b = Interval { lo: 2.0, hi: 5.0 };
1250 let (quot, div_zero) = a.div(&b);
1251 assert!(!div_zero);
1252 assert_eq!(quot.lo, 2.0); assert_eq!(quot.hi, 10.0); }
1255
1256 #[test]
1257 fn test_interval_div_by_zero() {
1258 let a = Interval { lo: 10.0, hi: 20.0 };
1259 let b = Interval { lo: -1.0, hi: 1.0 }; let (_, div_zero) = a.div(&b);
1261 assert!(div_zero);
1262 }
1263
1264 #[test]
1265 fn test_interval_widen() {
1266 let a = Interval { lo: 0.0, hi: 10.0 };
1267 let b = Interval { lo: -5.0, hi: 15.0 };
1268 let widened = a.widen(&b);
1269 assert_eq!(widened.lo, f64::NEG_INFINITY);
1270 assert_eq!(widened.hi, f64::INFINITY);
1271 }
1272
1273 #[test]
1278 fn test_dead_store_struct() {
1279 let ds = DeadStore {
1280 variable: "x".to_string(),
1281 ssa_name: "x_2".to_string(),
1282 line: 10,
1283 block_id: 1,
1284 is_phi: false,
1285 };
1286 assert_eq!(ds.variable, "x");
1287 assert_eq!(ds.ssa_name, "x_2");
1288 assert_eq!(ds.line, 10);
1289 assert!(!ds.is_phi);
1290 }
1291
1292 #[test]
1293 fn test_dead_store_serialization() {
1294 let ds = DeadStore {
1295 variable: "x".to_string(),
1296 ssa_name: "x_2".to_string(),
1297 line: 10,
1298 block_id: 1,
1299 is_phi: false,
1300 };
1301 let json = serde_json::to_string(&ds).unwrap();
1302 assert!(json.contains("\"variable\":\"x\""));
1303 assert!(json.contains("\"ssa_name\":\"x_2\""));
1304 }
1305
1306 #[test]
1311 fn test_chop_result_struct() {
1312 let result = ChopResult {
1313 file: "test.py".to_string(),
1314 lines: vec![2, 3, 4],
1315 count: 3,
1316 line_count: 3,
1317 source_line: 2,
1318 target_line: 4,
1319 path_exists: true,
1320 function: "example".to_string(),
1321 explanation: Some("Found path".to_string()),
1322 };
1323 assert_eq!(result.count, 3);
1324 assert!(result.path_exists);
1325 }
1326
1327 #[test]
1328 fn test_chop_result_same_line() {
1329 let result = ChopResult::same_line(5, "test_func");
1330 assert_eq!(result.lines, vec![5]);
1331 assert_eq!(result.count, 1);
1332 assert!(result.path_exists);
1333 }
1334
1335 #[test]
1336 fn test_chop_result_no_path() {
1337 let result = ChopResult::no_path(2, 10, "test_func");
1338 assert!(result.lines.is_empty());
1339 assert_eq!(result.count, 0);
1340 assert!(!result.path_exists);
1341 }
1342
1343 #[test]
1348 fn test_contracts_report_struct() {
1349 let report = ContractsReport {
1350 function: "process_data".to_string(),
1351 file: PathBuf::from("test.py"),
1352 preconditions: vec![Condition::high("x", "x >= 0", 10)],
1353 postconditions: vec![],
1354 invariants: vec![],
1355 };
1356 assert_eq!(report.function, "process_data");
1357 assert_eq!(report.preconditions.len(), 1);
1358 }
1359
1360 #[test]
1365 fn test_invariant_kind_serialization() {
1366 assert_eq!(
1367 serde_json::to_string(&InvariantKind::Type).unwrap(),
1368 "\"type\""
1369 );
1370 assert_eq!(
1371 serde_json::to_string(&InvariantKind::NonNull).unwrap(),
1372 "\"non_null\""
1373 );
1374 assert_eq!(
1375 serde_json::to_string(&InvariantKind::NonNegative).unwrap(),
1376 "\"non_negative\""
1377 );
1378 }
1379
1380 #[test]
1385 fn test_output_format_default() {
1386 assert_eq!(OutputFormat::default(), OutputFormat::Json);
1387 }
1388
1389 #[test]
1390 fn test_output_format_display() {
1391 assert_eq!(OutputFormat::Json.to_string(), "json");
1392 assert_eq!(OutputFormat::Text.to_string(), "text");
1393 }
1394}