backup

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.