From a8524aee404167951d28369426f951ad5f8a5fe2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20Tj=C3=A4der?= <henrik@tjaders.com>
Date: Mon, 26 Feb 2018 11:01:03 +0100
Subject: [PATCH] Spellcheck and modded gitignore
---
.gitignore | 4 ++++
examples/panic3.rs | 14 +++++++-------
examples/panic4.rs | 6 +++---
3 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/.gitignore b/.gitignore
index 29204d6..eda9f7d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,7 @@
.gdb_history
Cargo.lock
target/
+*.swp
+tags
+klee/tasks.txt
+output/
diff --git a/examples/panic3.rs b/examples/panic3.rs
index da3ac12..7351386 100644
--- a/examples/panic3.rs
+++ b/examples/panic3.rs
@@ -73,13 +73,13 @@ fn idle() -> ! {
// with a non atomic data type (u64), amounting to sequential reads
// (which are 32 bit on the ARM Cortex M).
//
-// However the framework analysis is clever enought to realize that the tasks
+// However the framework analysis is clever enough to realize that the tasks
// `EXTI1` and `EXTI2` can never preempt each other, hence we can
-// can access the data without "claiming" the resouce.
+// can access the data without "claiming" the resource.
//
-// Access is done by "dereferencing" `*r.X`, and we can now assert the
-// the value to be `*r.X`. However, as tasks operetate concurrently,
-// (without knowlegde on other tasks in the system), our analysis here
+// Access is done by "dereferencing" `*r.X`, and we can now assert
+// the value to be `*r.X`. However, as tasks operate concurrently,
+// (without knowledge on other tasks in the system), our analysis here
// marks `X` as a (implicitly) symbolic.
//
// Compile and run the example in KLEE.
@@ -94,9 +94,9 @@ fn idle() -> ! {
// ["EXTI1", "EXTI2"]
//
// In this case EXTI => task 0, EXTI2 = task 1, but they might be swapped
-// due to the underlyind data structure being an (unordered) hash-map.
+// due to the underlying data structure being an (unordered) hash-map.
//
-// Now uncomment the code in `exiti2` and comment out the assertion in `exti1`.
+// Now uncomment the code in `exti2` and comment out the assertion in `exti1`.
//
// Run the KLEE tool and find the failing assertion.
//
diff --git a/examples/panic4.rs b/examples/panic4.rs
index a6e1a7b..4340ca7 100644
--- a/examples/panic4.rs
+++ b/examples/panic4.rs
@@ -48,10 +48,10 @@ fn exti1(t: &mut Threshold, mut r: EXTI1::Resources) {
}
fn exti2(t: &mut Threshold, r: EXTI2::Resources) {
- // k_assume(*r.X > _ && *r.X < _); // pre-contition on X
+ // k_assume(*r.X > _ && *r.X < _); // pre-condition on X
let b = r.A[*r.X as usize];
*r.I = b;
- // as we don't change X post-condtiton is trivially true
+ // as we don't change X post-condition is trivially true
}
// The `init` function
@@ -91,7 +91,7 @@ fn idle() -> ! {
// You should not change the code, just enable the contacts
// The `_` should be filled with concrete values
//
-// Can you find a type invariant that satisfies BOTH pre- and post-condtitons
+// Can you find a type invariant that satisfies BOTH pre- and post-conditions
// at the same time.
//
// If not, why is that not possible?
--
GitLab