From be25c3e7a125655c827f0f39b154717d526376c0 Mon Sep 17 00:00:00 2001
From: Christian Dietrich <christian.dietrich@informatik.uni-erlangen.de>
Date: Mon, 24 Oct 2016 16:40:30 +0200
Subject: [PATCH] generate-ssm: added option
The verify.generate-mockup option also enables this option,
which uses application state machines to extract a more compact STG.
---
config/model.py | 2 ++
generator/main.py | 5 +++++
2 files changed, 7 insertions(+)
diff --git a/config/model.py b/config/model.py
index 2e2c8ad0..558496a4 100644
--- a/config/model.py
+++ b/config/model.py
@@ -62,6 +62,8 @@ model = ConfigurationTree({
},
'verify' : {
'generate-mockup': Boolean(short_help = "A application mockup is generated"),
+ 'generate-ssm': Boolean(short_help = "Use SSE to generate a more compact STG",
+ default_value=expr("generate-mockup")),
},
'app': {
'name': String(short_help = "Name of one application"),
diff --git a/generator/main.py b/generator/main.py
index 84b3ec22..262fc2fb 100755
--- a/generator/main.py
+++ b/generator/main.py
@@ -220,6 +220,11 @@ if __name__ == "__main__":
pass_manager.enqueue_analysis("InterruptControlAnalysis")
syscall_rules = FullSystemCalls()
+ if conf.verify.generate_ssm:
+ pass_manager.get_pass("sse").use_app_fsm = True
+ pass_manager.enqueue_analysis("app-fsm")
+ pass_manager.enqueue_analysis("system-fsm")
+
elif conf.os.systemcalls == "fsm_pla":
pass_manager.get_pass("sse").use_app_fsm = True
pass_manager.enqueue_analysis("app-fsm")
--
GitLab