diff --git a/config/model.py b/config/model.py index 2e2c8ad02bf5a8e8f9186fbc8ab5b1022bbc4220..558496a4bd7d26657bf593bcb8f179aac1967cf5 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 84b3ec22423df5400f2e076ebfac9d8f1014d247..262fc2fb617d83b2f716e426ff769280fcb5d17e 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")