diff --git a/app/bcc1/alarm1/verify_a.py b/app/bcc1/alarm1/verify_a.py
index 36731d3a4cd09f15b2744770925a80a7d1be8be1..523af7e8c62761845b1a3fc3f6444ea1df3bd355 100644
--- a/app/bcc1/alarm1/verify_a.py
+++ b/app/bcc1/alarm1/verify_a.py
@@ -1,31 +1,26 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
# H1 and H3 are not activated
- syscalls.update(set(H1.get_syscalls()))
- syscalls.update(set(H3.get_syscalls()))
+ t.mark_syscalls_in_function(H1)
+ t.mark_syscalls_in_function(H3)
- test(StartOS, "StartOS", [], # =>
- [Idle])
+ t.reachability(StartOS, "StartOS", [], # =>
+ [Idle])
- activated_test(analysis, [Idle], # =>
- H2)
+ t.activate([Idle], # =>
+ H2)
- test(H2, "TerminateTask", [], # =>
- [Idle])
+ t.reachability(H2, "TerminateTask", [], # =>
+ [Idle])
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
-
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/alarm1/verify_b.py b/app/bcc1/alarm1/verify_b.py
index 121a361afabb1b76e70da55a5714e4569017b3c9..0716ee7be694c855ba4f27f8e42bac7f7a8489da 100644
--- a/app/bcc1/alarm1/verify_b.py
+++ b/app/bcc1/alarm1/verify_b.py
@@ -1,36 +1,31 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
# H3 are not activated
- syscalls.update(set(H3.get_syscalls()))
+ t.mark_syscalls_in_function(H3)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- activated_test(analysis, [Idle], # =>
- H2)
+ t.activate([Idle], # =>
+ H2)
- test(H2, "ActivateTask", [H1], # =>
+ t.reachability(H2, "ActivateTask", [H1], # =>
[H1])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[Idle])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2])
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
-
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/alarm1/verify_c.py b/app/bcc1/alarm1/verify_c.py
index b0d4de91ba9d19da45ad4cdd8b03f3b326e96ecc..6f5dc42d4e09c9d091bb050abc26674b0d5e389d 100644
--- a/app/bcc1/alarm1/verify_c.py
+++ b/app/bcc1/alarm1/verify_c.py
@@ -1,33 +1,27 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
-
+ t = RunningTaskToolbox(analysis)
# H3 are not activated
- syscalls.update(set(H3.get_syscalls()))
+ t.mark_syscalls_in_function(H3)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- activated_test(analysis, [Idle, H1], # =>
- H2)
+ t.activate([Idle, H1], # =>
+ H2)
- test(H2, "ChainTask", [H1], # =>
+ t.reachability(H2, "ChainTask", [H1], # =>
[H1])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, Idle])
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
-
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/alarm1/verify_d.py b/app/bcc1/alarm1/verify_d.py
index 31d0c85ae2014e7c2d3b7f7b722b9888e8da1806..ca826c1256c93eaf41b3415f22e86399a7a75017 100644
--- a/app/bcc1/alarm1/verify_d.py
+++ b/app/bcc1/alarm1/verify_d.py
@@ -1,36 +1,32 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
- test(StartOS, "StartOS", [], # =>
+
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- activated_test(analysis, [Idle, H1, H3], # =>
- H2)
+ t.activate([Idle, H1, H3], # =>
+ H2)
- test(H1, "ActivateTask", [H3], # =>
+ t.reachability(H1, "ActivateTask", [H3], # =>
[H1])
- test(H2, "ChainTask", [H1], # =>
+ t.reachability(H2, "ChainTask", [H1], # =>
[H1])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, H3])
- test(H3, "TerminateTask", [], # =>
+ t.reachability(H3, "TerminateTask", [], # =>
[Idle])
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
-
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/alarm1/verify_e.py b/app/bcc1/alarm1/verify_e.py
index 98f50c0f34bc5f02c0baa7092d15bfc47352fc6b..d36f6241e1a2ea92bdd69b4c6d1383920811f39f 100644
--- a/app/bcc1/alarm1/verify_e.py
+++ b/app/bcc1/alarm1/verify_e.py
@@ -1,42 +1,38 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- activated_test(analysis, [Idle, H1, H3], # =>
- H2)
+ t.activate([Idle, H1, H3], # =>
+ H2)
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, H3])
- test(H2, "ActivateTask", [H3], # =>
+ t.reachability(H2, "ActivateTask", [H3], # =>
[H2])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[H3, Idle])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, H3])
- test(H3, "ActivateTask", [H1], # =>
+ t.reachability(H3, "ActivateTask", [H1], # =>
[H1])
- test(H3, "TerminateTask", [], # =>
+ t.reachability(H3, "TerminateTask", [], # =>
[Idle])
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/complex1/verify_a.py b/app/bcc1/complex1/verify_a.py
index 515eb31d999ea6fb57cd6b07802c16bbad2d7869..efbfbdbe01a6f1502b6cc98d424e8ac297cab6bd 100644
--- a/app/bcc1/complex1/verify_a.py
+++ b/app/bcc1/complex1/verify_a.py
@@ -1,35 +1,29 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
- syscalls.update(set(H3.get_syscalls()))
- syscalls.update(set(ISR1.get_syscalls()))
+ t = RunningTaskToolbox(analysis)
+ t.mark_syscalls_in_function(H3)
+ t.mark_syscalls_in_function(ISR1)
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
- return abb
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[Idle])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, # Activated by Alarm
Idle,
])
- activated_test(analysis, [Idle, H1], # =>
- H2)
+ t.activate([Idle, H1], # =>
+ H2)
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \
- %(analysis.system.get_syscalls(), syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/complex1/verify_b.py b/app/bcc1/complex1/verify_b.py
index 5b7047a007191e0d2c8d13d75114da306907fd6a..2e9847bcc814bfe255f66ce10c88664b1581dec7 100644
--- a/app/bcc1/complex1/verify_b.py
+++ b/app/bcc1/complex1/verify_b.py
@@ -1,36 +1,30 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
- syscalls.update(set(H1.get_syscalls()))
- syscalls.update(set(ISR1.get_syscalls()))
+ t = RunningTaskToolbox(analysis)
+ t.mark_syscalls_in_function(H1)
+ t.mark_syscalls_in_function(ISR1)
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
- return abb
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[Idle, H3]) # H3 could be activated by ISR1
- test(H3, "TerminateTask", [], # =>
+ t.reachability(H3, "TerminateTask", [], # =>
[Idle])
- activated_test(analysis, [Idle, H3], # =>
+ t.activate([Idle, H3], # =>
H2)
# H2.entry can be reached by H3.entry, when alarm was running
assert H2.entry_abb in H3.entry_abb.get_outgoing_nodes('global')
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \
- %(analysis.system.get_syscalls(), syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/complex1/verify_c.py b/app/bcc1/complex1/verify_c.py
index c8521f515f5d07dc9042f5a083b17f497a46f28d..ccb5a5f63e338eb6500056619d8b450b85cfba40 100644
--- a/app/bcc1/complex1/verify_c.py
+++ b/app/bcc1/complex1/verify_c.py
@@ -1,46 +1,40 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
- syscalls.update(set(H1.get_syscalls()))
- syscalls.update(set(ISR1.get_syscalls()))
+ t = RunningTaskToolbox(analysis)
+ t.mark_syscalls_in_function(H1)
+ t.mark_syscalls_in_function(ISR1)
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
- return abb
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[Idle, H3]) # H3 could be activated by ISR1
- test(H3, "ChainTask", [H1], # =>
+ t.reachability(H3, "ChainTask", [H1], # =>
[H1])
- test(H1, "TerminateTask", [], # =>
+ t.reachability(H1, "TerminateTask", [], # =>
[H2, # Could be activated by Alarm
H3, # Could be activated by ISR
Idle, # Nothing could have happended
])
- activated_test(analysis, [Idle, H3, H1], # =>
- H2)
+ t.activate([Idle, H3, H1], # =>
+ H2)
- activated_test(analysis, [H3], # =>
- H1)
+ t.activate([H3], # =>
+ H1)
# H2.entry can be reached by H3.entry, when alarm was running
assert H2.entry_abb in H3.entry_abb.get_outgoing_nodes('global')
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \
- %(analysis.system.get_syscalls(), syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/isr2/verify_a.py b/app/bcc1/isr2/verify_a.py
index 3aacaa8607bbec5e1a8ba726d5518709f84ea22e..517c166a5f83b04a69ee2e7eaae42ad66b74a3ec 100644
--- a/app/bcc1/isr2/verify_a.py
+++ b/app/bcc1/isr2/verify_a.py
@@ -1,33 +1,26 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
- syscalls.update(set(H1.get_syscalls()))
- syscalls.update(set(H3.get_syscalls()))
- syscalls.update(set(ISR1.get_syscalls()))
+ t = RunningTaskToolbox(analysis)
+ t.mark_syscalls_in_function(H1)
+ t.mark_syscalls_in_function(H3)
+ t.mark_syscalls_in_function(ISR1)
-
-
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[Idle])
- activated_test(analysis, [Idle], # =>
- H2)
+ t.activate([Idle], # =>
+ H2)
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \
- %(analysis.system.get_syscalls(), syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/isr2/verify_b.py b/app/bcc1/isr2/verify_b.py
index 15f9d32106e6190eb80d9596e4ea85b2ffa161e9..015326d4492da5450306a3073d232325a1779dde 100644
--- a/app/bcc1/isr2/verify_b.py
+++ b/app/bcc1/isr2/verify_b.py
@@ -1,39 +1,32 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
- syscalls.update(set(H1.get_syscalls()))
- syscalls.update(set(ISR1.get_syscalls()))
+ t = RunningTaskToolbox(analysis)
+ t.mark_syscalls_in_function(H1)
+ t.mark_syscalls_in_function(ISR1)
-
-
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Idle])
- test(H2, "ActivateTask", [H3], # =>
+ t.reachability(H2, "ActivateTask", [H3], # =>
[H2])
- test(H2, "TerminateTask", [], # =>
+ t.reachability(H2, "TerminateTask", [], # =>
[H3])
- test(H3, "TerminateTask", [], # =>
+ t.reachability(H3, "TerminateTask", [], # =>
[Idle])
- activated_test(analysis, [Idle, H3], # =>
- H2)
+ t.activate([Idle, H3], # =>
+ H2)
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/isr2/verify_c.py b/app/bcc1/isr2/verify_c.py
index 94cef5d0b8313ecf9812b3beb910b467cf017b1a..21f19e68cb85f02b2e8495c292d39d38747e6e1a 100644
--- a/app/bcc1/isr2/verify_c.py
+++ b/app/bcc1/isr2/verify_c.py
@@ -1,49 +1,45 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
-
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
- return abb
+ t = RunningTaskToolbox(analysis)
# In H2:
- AT3 = test(H2, "ActivateTask", [H3], # =>
- [H2])
+ AT3 = t.reachability(H2, "ActivateTask", [H3], # =>
+ [H2])
state_before_AT3 = analysis.for_abb(AT3)
- state_after_AT3 = analysis.for_abb(AT3.get_outgoing_nodes('global')[0])
+ state_after_AT3 = analysis.for_abb(AT3.definite_after('local'))
# Could be entered by H3 or Idle loop
assert state_before_AT3.is_unsure_ready_state(H3)
assert state_after_AT3.is_surely_ready(H3)
## Before ActivateTask(H1) the state of H3 is known
- AT1 = test(H2, "ActivateTask", [H1], # =>
- [H1])
+ AT1 = t.reachability(H2, "ActivateTask", [H1], # =>
+ [H1])
state_before_AT1 = analysis.for_abb(AT1)
assert state_before_AT1.is_surely_ready(H3)
- TT3 = test(H2, "TerminateTask", [], # =>
- [H3])
+ TT3 = t.reachability(H2, "TerminateTask", [], # =>
+ [H3])
returned_nodes = TT3.get_outgoing_nodes('global')
+ assert len(returned_nodes) == 2
# When H3 was not preempted, then we start in the entry node
assert H3.entry_abb in returned_nodes
# When H3 was interrupted by ISR1, then it was preempted, and
# should continue after the computation block
assert H3.entry_abb.definite_after('local') in returned_nodes
- test(StartOS, "StartOS", [], # =>
- [Idle])
+ t.reachability(StartOS, "StartOS", [], # =>
+ [Idle])
- activated_test(analysis, [Idle, H3], # =>
- H2)
+ t.activate([Idle, H3], # =>
+ H2)
# Idle handler is never left
- test(Idle, "Idle", [], # =>
- [Idle])
+ t.reachability(Idle, "Idle", [], # =>
+ [Idle])
diff --git a/app/bcc1/isr2/verify_d.py b/app/bcc1/isr2/verify_d.py
index 560f93a09041a57a0cf9fe8b3cf9be356ceb4c83..7b3fc721c44d8b9043e850282826ab6960f70230 100644
--- a/app/bcc1/isr2/verify_d.py
+++ b/app/bcc1/isr2/verify_d.py
@@ -1,20 +1,16 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(H1, H2, H3, Idle, StartOS, ISR1) = \
get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"])
- syscalls = set()
+ t = RunningTaskToolbox(analysis)
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
-
- test(H1, "TerminateTask", [], # =>
- [H3, # If interrupt was triggered
- Idle, # If Interrupt wasn't triggered
- ])
+ t.reachability(H1, "TerminateTask", [], # =>
+ [H3, # If interrupt was triggered
+ Idle, # If Interrupt wasn't triggered
+ ])
isr_entry_state = analysis.for_abb(ISR1.entry_abb)
for st in (H1, H2, H3):
diff --git a/app/bcc1/task1/verify_a.py b/app/bcc1/task1/verify_a.py
index a77cb42d094023629673e592e00f6d4a595858c8..b7454076366b3cf2d5ed3d91fdf8213ec354916f 100644
--- a/app/bcc1/task1/verify_a.py
+++ b/app/bcc1/task1/verify_a.py
@@ -1,43 +1,38 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS) = \
- get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
+ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
# Handler11 has higher priority than Handler12
- test(StartOS, "StartOS", [], # =>
- [Handler11])
+ t.reachability(StartOS, "StartOS", [], # =>
+ [Handler11])
# Handler11 has higher priority than Handler12
- test(Handler11, "ActivateTask", [Handler12], # =>
- [Handler11])
+ t.reachability(Handler11, "ActivateTask", [Handler12], # =>
+ [Handler11])
# Handler13 is directly started
- test(Handler11, "ActivateTask", [Handler13], # =>
- [Handler13])
+ t.reachability(Handler11, "ActivateTask", [Handler13], # =>
+ [Handler13])
# Handler12 is always activated afterwards
- test(Handler13, "TerminateTask", [], # =>
- [Handler11])
+ t.reachability(Handler13, "TerminateTask", [], # =>
+ [Handler11])
# Handler12 is always activated afterwards
- test(Handler11, "TerminateTask", [], # =>
- [Handler12])
+ t.reachability(Handler11, "TerminateTask", [], # =>
+ [Handler12])
# Handler12 is always activated afterwards
- test(Handler12, "TerminateTask", [], # =>
- [Idle])
+ t.reachability(Handler12, "TerminateTask", [], # =>
+ [Idle])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
- [Idle])
-
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
+ t.reachability(Idle, "Idle", [], # =>
+ [Idle])
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_b.py b/app/bcc1/task1/verify_b.py
index 0c6f2ea110578ba63b493209f60bbcf528324dd9..181c42e1165c24d060dde6370ea401153f947edf 100644
--- a/app/bcc1/task1/verify_b.py
+++ b/app/bcc1/task1/verify_b.py
@@ -1,4 +1,4 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_CurrentRunningSubtask(analysis):
(Handler11, bar) = \
@@ -22,39 +22,35 @@ def after_RunningTaskAnalysis(analysis):
(Handler11, Handler12, Handler13, bar, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
# Handler11 has higher priority than Handler12
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
# Handler11 has higher priority than Handler12
- test(Handler11, "ActivateTask", [Handler12], # =>
+ t.reachability(Handler11, "ActivateTask", [Handler12], # =>
[Handler11])
# Handler13 is directly started
- test(Handler11, "ChainTask", [Handler13], # =>
+ t.reachability(Handler11, "ChainTask", [Handler13], # =>
[Handler13])
# bar is called by Handler11
- test(bar, "ActivateTask", [Handler12], # =>
+ t.reachability(bar, "ActivateTask", [Handler12], # =>
[Handler11])
# Handler 13 does always lead to the activated handler 12
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler12])
# Handler12 is always activated afterwards
- test(Handler12, "TerminateTask", [], # =>
+ t.reachability(Handler12, "TerminateTask", [], # =>
[Idle])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- # All system calls were checked
- assert set(analysis.system.get_syscalls()) == syscalls
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_c.py b/app/bcc1/task1/verify_c.py
index 208ce6f465f52382b53ae33336dc78dec3a978f2..85763c4be30c35f5b1954339b95205f710fa1b40 100644
--- a/app/bcc1/task1/verify_c.py
+++ b/app/bcc1/task1/verify_c.py
@@ -1,4 +1,4 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_CurrentRunningSubtask(analysis):
(Handler11, bar) = \
@@ -22,35 +22,31 @@ def after_RunningTaskAnalysis(analysis):
(Handler11, Handler12, Handler13, bar, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
-
+ t = RunningTaskToolbox(analysis)
# Handler11 has higher priority than Handler12
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
# Handler13 is directly started
- test(Handler11, "ChainTask", [Handler13], # =>
+ t.reachability(Handler11, "ChainTask", [Handler13], # =>
[Handler13])
# bar is called by Handler11
- test(bar, "ActivateTask", [Handler12], # =>
+ t.reachability(bar, "ActivateTask", [Handler12], # =>
[Handler11])
# Handler 13 does always lead to the activated handler 12
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler12, Idle])
# Handler12 is always activated afterwards
- test(Handler12, "TerminateTask", [], # =>
+ t.reachability(Handler12, "TerminateTask", [], # =>
[Idle])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_d.py b/app/bcc1/task1/verify_d.py
index 47c3e747f8823b23076cdf8ba089b4bcaaa7ae43..086b688550a7b2dccaa4f4f3de8752ec0a9dbfb3 100644
--- a/app/bcc1/task1/verify_d.py
+++ b/app/bcc1/task1/verify_d.py
@@ -1,4 +1,4 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_CurrentRunningSubtask(analysis):
(Handler11, bar) = \
@@ -22,35 +22,31 @@ def after_RunningTaskAnalysis(analysis):
(Handler11, Handler12, Handler13, bar, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
-
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
- test(Handler11, "ActivateTask", [Handler12], # =>
+ t.reachability(Handler11, "ActivateTask", [Handler12], # =>
[Handler11])
- test(bar, "ActivateTask", [Handler13], # =>
+ t.reachability(bar, "ActivateTask", [Handler13], # =>
[Handler13])
- test(Handler11, "ActivateTask", [Handler13], # =>
+ t.reachability(Handler11, "ActivateTask", [Handler13], # =>
[Handler13])
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler11])
- test(Handler11, "TerminateTask", [], # =>
+ t.reachability(Handler11, "TerminateTask", [], # =>
[Handler12, Idle])
- test(Handler12, "TerminateTask", [], # =>
+ t.reachability(Handler12, "TerminateTask", [], # =>
[Idle])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_e.py b/app/bcc1/task1/verify_e.py
index 4f516ced5106e2b36dd858fdada0db08d42b20eb..e7fa842c2ccbe0d31aaac7348958437e7b782bad 100644
--- a/app/bcc1/task1/verify_e.py
+++ b/app/bcc1/task1/verify_e.py
@@ -1,36 +1,33 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
- test(Handler13, "ActivateTask", [Handler12], # =>
+ t.reachability(Handler13, "ActivateTask", [Handler12], # =>
[Handler13])
- test(Handler11, "ActivateTask", [Handler13], # =>
+ t.reachability(Handler11, "ActivateTask", [Handler13], # =>
[Handler13])
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler11])
# Handler13 did non nessecary run!
- test(Handler11, "TerminateTask", [], # =>
+ t.reachability(Handler11, "TerminateTask", [], # =>
[Handler12, Idle])
- test(Handler12, "TerminateTask", [], # =>
+ t.reachability(Handler12, "TerminateTask", [], # =>
[Idle])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[Idle])
- assert set(analysis.system.get_syscalls()) == syscalls
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_f.py b/app/bcc1/task1/verify_f.py
index 7e64e39962ec2c89a0f01437f54fa52cdc880833..992da4cc86b59b76e1d3d2197593840775372ad6 100644
--- a/app/bcc1/task1/verify_f.py
+++ b/app/bcc1/task1/verify_f.py
@@ -1,33 +1,29 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
- test(Handler11, "ChainTask", [Handler13], # =>
+ t.reachability(Handler11, "ChainTask", [Handler13], # =>
[Handler13])
- test(Handler13, "ActivateTask", [Handler12], # =>
+ t.reachability(Handler13, "ActivateTask", [Handler12], # =>
[Handler13])
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler12])
- test(Handler12, "ChainTask", [Handler11], # =>
+ t.reachability(Handler12, "ChainTask", [Handler11], # =>
[Handler11])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[])
- assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \
- %(analysis.system.get_syscalls(), syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task1/verify_g.py b/app/bcc1/task1/verify_g.py
index 18632c26a073454996e32a726360388449e50f1d..e9fb05476bbb9904f5028fc4b38ae17fe07c4296 100644
--- a/app/bcc1/task1/verify_g.py
+++ b/app/bcc1/task1/verify_g.py
@@ -1,36 +1,32 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS, bar) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS", "bar"])
- syscalls = set()
- def test(func, syscall, args, expected_subtasks):
- abb = reachability_test(analysis, func, syscall, args, expected_subtasks)
- syscalls.add(abb)
+ t = RunningTaskToolbox(analysis)
- test(StartOS, "StartOS", [], # =>
+ t.reachability(StartOS, "StartOS", [], # =>
[Handler11])
- test(Handler11, "ChainTask", [Handler13], # =>
+ t.reachability(Handler11, "ChainTask", [Handler13], # =>
[Handler13])
- test(Handler13, "ActivateTask", [Handler12], # =>
+ t.reachability(Handler13, "ActivateTask", [Handler12], # =>
[Handler13])
- test(Handler13, "TerminateTask", [], # =>
+ t.reachability(Handler13, "TerminateTask", [], # =>
[Handler12, Handler11])
- test(Handler12, "ChainTask", [Handler11], # =>
+ t.reachability(Handler12, "ChainTask", [Handler11], # =>
[Handler11])
- test(bar, "ActivateTask", [Handler13], # =>
+ t.reachability(bar, "ActivateTask", [Handler13], # =>
[Handler13])
# Idle handler is never left
- test(Idle, "Idle", [], # =>
+ t.reachability(Idle, "Idle", [], # =>
[])
- assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \
- %(set(analysis.system.get_syscalls()) - syscalls)
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task2/verify_a.py b/app/bcc1/task2/verify_a.py
index 34e7a75e5f3bca83abcf54360ba43cce4cb812b5..06a5e97561fa2e47556be86b7c376e6307010ffe 100644
--- a/app/bcc1/task2/verify_a.py
+++ b/app/bcc1/task2/verify_a.py
@@ -1,48 +1,46 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
- def reachability(function, syscall, arguments, reaching_subtasks):
- syscall = analysis.system.find_syscall(function, syscall, arguments)
- assert syscall
- reachable_tasks = analysis.reachable_subtasks_from_abb(syscall)
- assert(reachable_tasks == set(reachable_tasks))
+ t = RunningTaskToolbox(analysis)
# Handler11 has higher priority than Handler12
- reachability(StartOS, "StartOS", [],
+ t.reachability(StartOS, "StartOS", [],
# =>
[Handler11])
# Handler11 has higher priority than Handler12
- reachability(Handler11, "ActivateTask", [Handler12],
+ t.reachability(Handler11, "ActivateTask", [Handler12],
# =>
[Handler11])
# Handler11 is preemptable
- reachability(Handler11, "ActivateTask", [Handler13],
+ t.reachability(Handler11, "ActivateTask", [Handler13],
# =>
[Handler11])
# Handler12 is always activated afterwards
- reachability(Handler11, "TerminateTask", [],
+ t.reachability(Handler11, "TerminateTask", [],
# =>
[Handler13])
# Handler12 is always activated afterwards
- reachability(Handler13, "TerminateTask", [],
+ t.reachability(Handler13, "TerminateTask", [],
# =>
[Handler12])
# Handler12 is always activated afterwards
- reachability(Handler12, "TerminateTask", [],
+ t.reachability(Handler12, "TerminateTask", [],
# =>
[Idle])
# Idle handler is never left
- reachability(Idle, "Idle", [],
- # =>
- [])
+ t.reachability(Idle, "Idle", [],
+ # =>
+ [Idle])
+
+ t.promise_all_syscalls_checked()
diff --git a/app/bcc1/task2/verify_b.py b/app/bcc1/task2/verify_b.py
index 3dd8019a91f02be6629d126e309719d20001705d..686a26453d019efd42c04f88093d6b7b97160f52 100644
--- a/app/bcc1/task2/verify_b.py
+++ b/app/bcc1/task2/verify_b.py
@@ -1,28 +1,24 @@
-from generator.graph.common import *
+from generator.graph.verifier_tools import *
def after_RunningTaskAnalysis(analysis):
# Find all three systemcall handlers
(Handler11, Handler12, Handler13, Idle, StartOS) = \
get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"])
- def reachability(function, syscall, arguments, reaching_subtasks):
- syscall = analysis.system.find_syscall(function, syscall, arguments)
- assert syscall
- reachable_tasks = analysis.reachable_subtasks_from_abb(syscall)
- assert(reachable_tasks == set(reachable_tasks))
+ t = RunningTaskToolbox(analysis)
# Handler11 has higher priority than Handler12
- reachability(StartOS, "StartOS", [],
+ t.reachability(StartOS, "StartOS", [],
# =>
[Handler11])
# Handler11 has higher priority than Handler12
- reachability(Handler11, "ActivateTask", [Handler12],
+ t.reachability(Handler11, "ActivateTask", [Handler12],
# =>
[Handler11])
# Handler11 is preemptable
- reachability(Handler11, "ActivateTask", [Handler13],
+ t.reachability(Handler11, "ActivateTask", [Handler13],
# =>
[Handler11])
@@ -32,19 +28,21 @@ def after_RunningTaskAnalysis(analysis):
for x in syscalls:
tasks = set(analysis.reachable_subtasks_from_abb(x))
assert tasks == set([Handler12]) or tasks == set([Handler13])
+ t.mark_syscall(x)
# Handler12 is always activated afterwards
- reachability(Handler13, "TerminateTask", [],
+ t.reachability(Handler13, "TerminateTask", [],
# =>
[Handler12])
# Handler12 is always activated afterwards
- reachability(Handler12, "TerminateTask", [],
+ t.reachability(Handler12, "TerminateTask", [],
# =>
[Idle])
# Idle handler is never left
- reachability(Idle, "Idle", [],
+ t.reachability(Idle, "Idle", [],
# =>
- [])
+ [Idle])
+ t.promise_all_syscalls_checked()
diff --git a/generator/graph/RunningTask.py b/generator/graph/RunningTask.py
index f0103b323e94d40edc91cc3d1b23d7ecd7545794..a87a770f19126e989e690205790ac7205139583a 100644
--- a/generator/graph/RunningTask.py
+++ b/generator/graph/RunningTask.py
@@ -450,12 +450,14 @@ class RunningTaskAnalysis(Analysis):
subtasks.add(st)
return subtasks
- def activated_by(self, subtask):
+ def activating_subtasks(self, subtask):
subtasks = set()
+ abbs = set()
for reaching in subtask.entry_abb.get_incoming_nodes('global'):
st = self.running_task.for_abb(reaching)
subtasks.add(st)
- return subtasks
+ abbs.add(reaching)
+ return subtasks, abbs
def for_abb(self, abb):
return self.before_abb_states[abb]
diff --git a/generator/graph/common.py b/generator/graph/common.py
index ad9c627053efbdeab4b0e771e705079d1d16b013..fea23dd7009fd713b90a880e167469792b0ae49b 100644
--- a/generator/graph/common.py
+++ b/generator/graph/common.py
@@ -144,38 +144,6 @@ class FixpointIteraton:
def is_local_edge(edge):
return edge.is_local()
-def get_functions(system, names):
- """A helper for verify scripts to find quickly a set of subtask handlers"""
- ret = []
- for x in names:
- for name, func in system.functions.items():
- if x == name or \
- "OSEKOS_TASK_" + x == name or \
- "OSEKOS_ISR_" + x == name:
- ret.append(func)
- return tuple(ret)
-
-def syscall_test(analysis, function, syscall_name, arguments):
- """Tests wheter a syscall exists and returns it"""
- syscall = analysis.system.find_syscall(function, syscall_name, arguments)
- assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments)
- return syscall
-
-
-def reachability_test(analysis, function, syscall_name, arguments, possible_subtasks):
- syscall = analysis.system.find_syscall(function, syscall_name, arguments)
- assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments)
- reachable_subtasks = analysis.reachable_subtasks_from_abb(syscall)
- assert(set(reachable_subtasks) == set(possible_subtasks)), "%s:%s(%s)::: %s != %s" %(
- function.function_name, syscall_name, arguments, list(possible_subtasks), list(reachable_subtasks))
-
- return syscall
-
-def activated_test(analysis, possible_subtasks, function):
- reachable_subtasks = analysis.activated_by(function)
- assert(set(reachable_subtasks) == set(possible_subtasks)), "SetReady(%s):: %s != %s" %(
- function.function_name, list(possible_subtasks), list(reachable_subtasks))
-
# Hook for coloured tracebacks on the console :-)
def myexcepthook(type, value, tb):
diff --git a/generator/graph/verifier_tools.py b/generator/graph/verifier_tools.py
new file mode 100644
index 0000000000000000000000000000000000000000..7c44687a4f20d0278aadf403ab352cb7b774759f
--- /dev/null
+++ b/generator/graph/verifier_tools.py
@@ -0,0 +1,55 @@
+def get_functions(system, names):
+ """A helper for verify scripts to find quickly a set of subtask handlers"""
+ ret = []
+ for x in names:
+ for name, func in system.functions.items():
+ if x == name or \
+ "OSEKOS_TASK_" + x == name or \
+ "OSEKOS_ISR_" + x == name:
+ ret.append(func)
+ return tuple(ret)
+
+class RunningTaskToolbox:
+ def __init__(self, analysis):
+ self.analysis = analysis
+ self.checked_syscalls = set()
+
+ def mark_syscall(self, syscall):
+ """Mark syscall as checked"""
+ self.checked_syscalls.add(syscall)
+
+ def mark_syscalls_in_function(self, function):
+ """Mark all syscalls in functions as checked"""
+ for syscall in function.get_syscalls():
+ self.mark_syscall(syscall)
+
+ def promise_all_syscalls_checked(self):
+ assert set(self.analysis.system.get_syscalls()) == self.checked_syscalls, "missing %s" \
+ %(set(self.analysis.system.get_syscalls()) - self.checked_syscalls)
+
+ def syscall(self, function, syscall_name, arguments):
+ """Tests wheter a syscall exists and returns it"""
+ syscall = self.analysis.system.find_syscall(function, syscall_name, arguments)
+ assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments)
+ return syscall
+
+ def reachability(self, function, syscall_name, arguments, possible_subtasks):
+ """Check to which subtasks a certain syscall can dispatch. Syscall is
+ marked as visited"""
+
+ syscall = self.syscall(function, syscall_name, arguments)
+ reachable_subtasks = self.analysis.reachable_subtasks_from_abb(syscall)
+ assert(set(reachable_subtasks) == set(possible_subtasks)), "%s:%s(%s)::: %s != %s" %(
+ function.function_name, syscall_name, arguments, list(possible_subtasks), list(reachable_subtasks))
+ self.checked_syscalls.add(syscall)
+
+ return syscall
+
+ def activate(self, possible_subtasks, function):
+ """Check which subtasks can activate a given function. The activating
+ ABBs are returned"""
+ activating_subtasks, activating_abbs = self.analysis.activating_subtasks(function)
+ assert(set(activating_subtasks) == set(possible_subtasks)), "SetReady(%s):: %s != %s" %(
+ function.function_name, list(activating_subtasks), list(reachable_subtasks))
+
+ return activating_abbs
diff --git a/toolchain/app.cmake b/toolchain/app.cmake
index 0748ec0541a2cab318d020da24e675f7b43a91e1..39508a04897e829f6be3b6496eba406754433e3a 100644
--- a/toolchain/app.cmake
+++ b/toolchain/app.cmake
@@ -125,5 +125,5 @@ MACRO(COREDOS_BINARY)
coredos_executable(${NAME} EXCLUDE_FROM_ALL
${COREDOS_SOURCE_SYSTEM_OBJECT} ${COREDOS_GENERATED_SOURCE})
- add_test(${NAME}-test make ${NAME}-generate)
+ add_test(${NAME}-test make ${NAME}-clean ${NAME}-generate)
ENDMACRO(COREDOS_BINARY)