diff --git a/examples/resource.rs b/examples/resource.rs index 586939308a788065c6caddf2a7c679b7ee2ae93e..eaa6d46b876de5c8b516c4566d891cb4a4c5890d 100644 --- a/examples/resource.rs +++ b/examples/resource.rs @@ -51,7 +51,7 @@ fn exti1(t: &mut Threshold, EXTI1::Resources { X, mut Y }: EXTI1::Resources) { Y.claim_mut(t1, |y, _| { if *x < 10 { for _ in 0..*x { - *y += 1; + *y = y.wrapping_add(1); } } }); @@ -72,7 +72,7 @@ fn exti2(t: &mut Threshold, mut r: EXTI2::Resources) { #[allow(non_snake_case)] fn exti3(t: &mut Threshold, mut r: EXTI3::Resources) { r.X.claim_mut(t, |x, _| { - *x += 1; + *x = x.wrapping_add(1); }) } @@ -126,18 +126,27 @@ fn idle() -> ! { // // How many tests were generated for task EXIT1? // ** your answer here ** +// 11 +// // Why that many, (look at the code and the generted tests). // ** your answer here ** +// one test for every lop iteration and the exstrem out sider // // How many tests were generated for task EXIT2? // ** your answer here ** +// 2 +// // Why that many, (look at the code and the generted tests). // ** your answer here ** +// the extreams // // How many tests were generated for task EXIT3? // ** your answer here ** +// 2 +// // Why that many, (look at the code and the generted tests). // ** your answer here ** +// the extreams // // (There will be one additional "dymmy" test for testing "no task".) // @@ -152,15 +161,19 @@ fn idle() -> ! { // // How many errors were identified? // ** your answer here ** +// 2 // // For one of the arithmetic operations, no error was found. // Explain why this is no error. // ** your answer here ** +// In the exterams is the add/sub working in the right diraktion so it never wraps // // Why didn't KLEE report all the errors initially? // Scroll back and compare the stack traces of the generated errors. // Hint, for each line in the code KLEE will spot ONE error. // ** your answer here ** +// It is the some type of error and klee only finds one of a spesefick type at the time. +// // // Assignment 2. // KLEE has now generated tests covering EACH feasible path for EACH task.