[rtems-central commit] pythin tests
Sebastian Huber
sebh at rtems.org
Wed Jan 18 11:35:17 UTC 2023
Module: rtems-central
Branch: master
Commit: 1056ddb22c79975d76811c9a81798c3e2ca9b115
Changeset: http://git.rtems.org/rtems-central/commit/?id=1056ddb22c79975d76811c9a81798c3e2ca9b115
Author: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>
Date: Tue Jan 10 19:57:52 2023 +0000
pythin tests
---
formal/promela/src/src/tests/__init__.py | 0
formal/promela/src/src/tests/library.coco | 154 ++++++++
.../src/src/tests/test_coverage_spin2test.coco | 144 ++++++++
.../src/src/tests/test_coverage_testgen.coco | 394 +++++++++++++++++++++
formal/promela/src/src/tests/test_optional.coco | 46 +++
5 files changed, 738 insertions(+)
diff --git a/formal/promela/src/src/tests/__init__.py b/formal/promela/src/src/tests/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/formal/promela/src/src/tests/library.coco b/formal/promela/src/src/tests/library.coco
new file mode 100644
index 00000000..50f9d1d0
--- /dev/null
+++ b/formal/promela/src/src/tests/library.coco
@@ -0,0 +1,154 @@
+ # SPDX-License-Identifier: BSD-2-Clause
+
+ ##############################################################################
+ # Library Test
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ # * Redistributions of source code must retain the above copyright
+ # notice, this list of conditions and the following disclaimer.
+ #
+ # * Redistributions in binary form must reproduce the above
+ # copyright notice, this list of conditions and the following
+ # disclaimer in the documentation and/or other materials provided
+ # with the distribution.
+ #
+ # * Neither the name of the copyright holders nor the names of its
+ # contributors may be used to endorse or promote products derived
+ # from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.library import *
+from src import testgen
+
+#
+
+import os
+import random
+
+#
+
+cwd = os.getcwd () + '/'
+cons_cwd = path -> cwd + path
+app_cwd = f -> f cwd
+
+models = '../../../models/'
+models_chains = models + 'chains/src/'
+models_events = models + 'events/src/'
+
+model_checker = '../examples/model_checker/spin.pml'
+
+not_exist_command = 'not_exist_command_' + str (random.random ())
+
+name_b = check_unparse_parse -> '1' if check_unparse_parse else '0'
+name_ml = (fic, check_unparse_parse) -> f'pytest_{name_b (check_unparse_parse)}_ml_{fic}.auto_output'
+name_yaml = (fic, check_unparse_parse) -> f'pytest_{name_b (check_unparse_parse)}_yaml_{fic}.auto_output'
+
+def gen_main (argv, check_unparse_parse, input_output_yaml):
+ testgen.main ( 0
+ , argv + ([ '--promela', r' /*@ check_unparse_parse'
+ r' */' ]
+ if check_unparse_parse else [])
+ , input_output_yaml )
+
+def main_ml_promela0 (model_checker, refine, check_unparse_parse, dir0, fic, fic_out):
+ cfg = fileinput_input0 (cons_cwd (dir0 + 'testsuites.cfg'))
+ assert (r'export_dir \<open>_\<close>' in cfg)
+ assert not os.path.exists ('_')
+ gen_main ( list (map (app_cwd, [ model_checker
+ , cwd -> cwd + dir0 + fic + '.pml'
+ , refine dir0 fic ]))
+ + [ '--promela', cfg ]
+ , check_unparse_parse
+ , False)
+ os.rename ('_', name_ml (fic_out, check_unparse_parse))
+
+main_ml_promela_arg_model_checker = cwd -> cwd + model_checker
+main_ml_promela_arg_refine = (dir0, fic) -> cwd -> cwd + dir0 + fic + '.rfn'
+main_ml_promela = (check_unparse_parse, dir0, fic) -> main_ml_promela0 (main_ml_promela_arg_model_checker, main_ml_promela_arg_refine, check_unparse_parse, dir0, fic, fic)
+
+def symlink (dir0, dir1, fic):
+ os.symlink (dir0 + fic, dir1 + fic)
+
+def main_yaml_promela (check_unparse_parse, dir0, fic):
+ rfn = fileinput_input0 (cons_cwd (dir0 + fic + '.rfn'))
+ assert r'export_input_yaml \<open>_\<close>' in rfn
+ assert r'export_input_only_content' in rfn
+ dir1 = name_ml (fic, check_unparse_parse) + '/_/'
+ assert all <| map (os.path.exists <.. testgen.export_yml_ext $ dir1, ['', '0', '1', '2', '3'])
+ if r'enclose_file \<open>enclose_1_head.c\<close>' in rfn and r'\<open>enclose_2_foot.c\<close>' in rfn:
+ symlink (cons_cwd dir0, dir1, 'enclose_1_head.c')
+ symlink (cons_cwd dir0, dir1, 'enclose_2_foot.c')
+ else:
+ assert r'enclose_file \<open>enclose_1_head.yml\<close>' in rfn and r'\<open>enclose_2_foot.yml\<close>' in rfn
+ symlink (cons_cwd dir0, dir1, 'enclose_1_head.yml')
+ symlink (cons_cwd dir0, dir1, 'enclose_2_foot.yml')
+ if r'refine_generic_file \<open>../examples/only_generic/chains-rfn.yml\<close>' in rfn:
+ symlink (cons_cwd (dir0 + '../'), dir1 + '../', 'examples')
+ else:
+ assert r'refine_generic_file' not in rfn # not yet implemented: regular expression to match the file name
+ if r'enclose_uniform_file \<open>enclose_init_1_head.c\<close>' in rfn and r'\<open>enclose_init_2_foot.c\<close>' in rfn:
+ symlink (cons_cwd dir0, dir1, 'enclose_init_1_head.c')
+ symlink (cons_cwd dir0, dir1, 'enclose_init_2_foot.c')
+ else:
+ assert r'enclose_uniform_file' not in rfn # not yet implemented: regular expression to match the file name
+ gen_main ( [ '--annotation_file', cons_cwd (testgen.export_yml_ext (dir1, '0'))
+ , cons_cwd (dir0 + fic + '.pml')
+ , '--annotation_file', cons_cwd (testgen.export_yml_ext (dir1, '2'))
+ , '--annotation', fileinput_input0 (cons_cwd (testgen.export_yml_ext (dir1, '3'))) ]
+ , check_unparse_parse
+ , True)
+ os.rename ('_', name_yaml (fic, check_unparse_parse))
+
+def main_promela0 (check_unparse_parse, dir0, fic):
+ main_ml_promela (check_unparse_parse, dir0, fic)
+ main_yaml_promela (check_unparse_parse, dir0, fic)
+
+def main_promela (dir0, fic):
+ main_promela0 (False, dir0, fic)
+ main_promela0 (True, dir0, fic)
+
+def main_promela_events (fic):
+ main_promela (models_events, fic)
+
+def main_ram (arg1, arg2):
+ gen_main ( list (map (cons_cwd, arg1))
+ + arg2
+ , False
+ , False)
+
+def main0 (arg):
+ main_ram ([model_checker], ['-p' + arg])
+
+def main1 (arg):
+ main_ram ([], [arg])
+
+def main2 (arg):
+ main1 ('-p' + arg)
+
+def main3 (arg):
+ main0 (arg + r' ltl { true }')
+
+#
+
+def test_anonymous_not_exec ():
+ # this empty test is only present for coverage reasons (it can then be used as an 'anonymous' function, in situations where the function is not expected to be executed)
+ return
diff --git a/formal/promela/src/src/tests/test_coverage_spin2test.coco b/formal/promela/src/src/tests/test_coverage_spin2test.coco
new file mode 100644
index 00000000..6b63cf45
--- /dev/null
+++ b/formal/promela/src/src/tests/test_coverage_spin2test.coco
@@ -0,0 +1,144 @@
+# SPDX-License-Identifier: BSD-2-Clause
+"""Converts Annotated SPIN counter-examples to program test code"""
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+import src.refine_command as refine
+from src import spin2test
+
+#
+
+from itertools import chain
+import pytest
+
+#
+
+def test_spin2test1 ():
+ spin2test.main (0, '../../../models/events/rqmts-spec-level/', 'model-events-mgr')
+
+def test_spin2test2 ():
+ task_name = 'task_name'
+ decl_name = 'decl_name'
+ dclarray_name = 'dclarray_name'
+ ptr_name = 'ptr_name'
+ call_name0 = 'call_name0'
+ call_name1 = 'call_name1'
+ call_name2 = 'call_name2'
+ call_name3 = 'call_name3'
+ call_name4 = 'call_name4'
+ call_name5 = 'call_name5'
+ call_name6 = 'call_name6'
+ call_name7 = 'call_name7'
+ end_name = 'end_name'
+ scalar_name0 = 'scalar_name0'
+ scalar_name1 = 'scalar_name1'
+ state_name = 'state_name'
+ cmd1 = refine.command ({}, outputLOG = True, annoteComments = False, outputSWITCH = True)
+ cmd1.refineSPINLine_main ([])
+ cmd2 = refine.command (dict (chain ({ 'SUSPEND' : '{}{}{}'
+ , 'WAKEUP' : '{}{}{}'
+ , ptr_name + '_PTR' : '\n{}'
+ , ptr_name + '_FPTR' : '{}\n{}{}'
+ , call_name1 : '{}'
+ , call_name2 : '{}{}'
+ , call_name3 : '{}{}{}'
+ , call_name4 : '{}{}{}{}'
+ , call_name5 : '{}{}{}{}{}'
+ , call_name6 : '{}{}{}{}{}{}'
+ , call_name7 : '{}{}{}{}{}{}{}'
+ , scalar_name1 + '_FSCALAR' : '{}{}' }.items (),
+ {x: '' for x in [ 'NAME'
+ , 'INIT'
+ , task_name
+ , 'SIGNAL'
+ , 'WAIT'
+ , decl_name + '_DCL'
+ , dclarray_name + '_DCL'
+ , call_name0
+ , end_name + '_SEQ'
+ , scalar_name0
+ , state_name ]}.items ())),
+ outputSWITCH = True)
+ def cmd12 (cmds):
+ for cmd0 in cmds:
+ cmd = ['3'] + cmd0
+ cmd1.refineSPINLine_main cmd
+ cmd2.refineSPINLine_main cmd
+ cmd12 ([ ['LOG', 'Sender', '0', 'finished']
+ , ['NAME', '']
+ , ['INIT']
+ , ['TASK', task_name]
+ , ['SIGNAL', '']
+ , ['WAIT', '']
+ , ['DECL', '', decl_name]
+ , ['DCLARRAY', '', dclarray_name, '']
+ , ['PTR', ptr_name, '0']
+ , ['PTR', ptr_name, '1']
+ , ['PTR', ptr_name, '']
+ , ['END', '']
+ , ['STRUCT', '']
+ , ['PTR', ptr_name, '0']
+ , ['CALL', call_name0]
+ , ['CALL', call_name1, '']
+ , ['CALL', call_name2, '', '']
+ , ['CALL', call_name3, '', '', '']
+ , ['CALL', call_name4, '', '', '', '']
+ , ['CALL', call_name5, '', '', '', '', '']
+ , ['CALL', call_name6, '', '', '', '', '', '']
+ , ['CALL', call_name7, '', '', '', '', '', '', '']
+ , ['SCALAR', scalar_name1, '']
+ , ['SCALAR', scalar_name1, '', '']
+ , ['SEQ', '']
+ , ['END', end_name]
+ , ['SCALAR', '_', '']
+ , ['SCALAR', scalar_name0, '']
+ , ['SCALAR', scalar_name0, '', '']
+ , ['STATE', '', state_name]
+ , ['DON_T_KNOW_HOW_TO_REFINE']
+ , []])
+
+def test_spin2test3 ():
+ pid, name, task_name, value, typ, index, tid, state = 0, 0, 0, 0, 0, 0, 0, 0
+ rest = []
+ cmd = refine.command ({})
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'LOG']+rest, test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'NAME',name], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'INIT'], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'TASK',task_name], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'SIGNAL',value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'WAIT',value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'DEF',name,value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'DECL',typ,name]+rest, test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'DCLARRAY',typ,name,value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'PTR',name,value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'CALL',name]+rest, test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'STRUCT',name], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'SEQ',name], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'END',name], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR','_',value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR',name,value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'SCALAR',name,index,value], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid,'STATE',tid,state], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([pid], test = 'test')
+ with pytest.raises Exception: cmd.refineSPINLine ([], test = 'test')
diff --git a/formal/promela/src/src/tests/test_coverage_testgen.coco b/formal/promela/src/src/tests/test_coverage_testgen.coco
new file mode 100644
index 00000000..94314c8e
--- /dev/null
+++ b/formal/promela/src/src/tests/test_coverage_testgen.coco
@@ -0,0 +1,394 @@
+ # SPDX-License-Identifier: BSD-2-Clause
+
+ ##############################################################################
+ # Test Coverage TestGen
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ # * Redistributions of source code must retain the above copyright
+ # notice, this list of conditions and the following disclaimer.
+ #
+ # * Redistributions in binary form must reproduce the above
+ # copyright notice, this list of conditions and the following
+ # disclaimer in the documentation and/or other materials provided
+ # with the distribution.
+ #
+ # * Neither the name of the copyright holders nor the names of its
+ # contributors may be used to endorse or promote products derived
+ # from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.library import *
+from src import syntax_ml
+from src import syntax_pml
+from src.syntax_pml import src_comment, src_annotation, src_directive, arg_pml, arg_annotation
+from src import syntax_yaml
+from src import testgen
+from src.tests.library import *
+
+#
+
+import os
+import pytest
+import tempfile
+
+#
+
+def test_syntax_ml ():
+ with pytest.raises Exception:
+ syntax_ml.not_string ('', 0).parse ('')
+ syntax_ml.enclose_flat ('', '').parse ('')
+ syntax_ml.antiquotation.parse (r'\<ant>')
+ syntax_ml.parse_directive (r'# refine var_c \<^promela>\<open>var_pml\<close> remaining parsed tokens')
+ consume <| syntax_ml.unparse_annotation (None, None, None, None)
+
+def test_syntax_pml ():
+ with pytest.raises Exception:
+ syntax_pml.find_annot0 None
+ with pytest.raises Exception:
+ syntax_pml.find_annot0 ((1, 2), 3, zz = None)
+ consume <| syntax_pml.parse_comment ((arg_pml (), r'/**//*'
+ '\n'
+ r'*/'))
+ consume <| syntax_pml.parse_comment ((arg_pml (), r'/*'
+ '\n'
+ r'*//*'
+ '\n'
+ r'*/'))
+ syntax_pml.directives_refine.parse (r'#r c pml')
+ consume <| syntax_pml.unparse_source_directive (test_anonymous_not_exec, [None])
+
+ #
+
+ def map_source ( map_annotation = syntax_yaml.unparse_annotation
+ , parse_commands = syntax_ml.parse_commands
+ , only_content = False
+ , subst_lines = []
+ , lines = (arg_pml (), r'/*@*/')):
+ consume <| syntax_pml.map_source (map_annotation, parse_commands, only_content, subst_lines, lines)
+ map_source (subst_lines = [(2, [(1, ('', []))])])
+ map_source (subst_lines = [(0, [(1, ('', []))])])
+ def map_source2 (only_content):
+ map_source (parse_commands = (_ -> None), only_content = only_content, lines = (arg_annotation (), ''))
+ map_source2 False
+ map_source2 True
+
+ #
+
+ def parse (_):
+ yield None
+ consume <| syntax_pml.map_source0 (parse, syntax_yaml.unparse_annotation, test_anonymous_not_exec, False, [], (arg_annotation (), r''))
+
+def test_syntax_pml1 ():
+ main0 (r' /*@ no_printf_at */')
+
+def test_syntax_pml2 ():
+ main0 (r' /*@ no_printf_at \<open>zzz\<close> */')
+
+def test_syntax_pml3 ():
+ main0 (r' /*@ refine_uniform_at \<open>prop\<close>'
+ r' */'
+ r' init { true }'
+ r' ltl prop { true }')
+
+def test_syntax_yaml ():
+ syntax_yaml.safe_load (r':')
+ syntax_yaml.parse_directive (r'#refine a []')
+ syntax_yaml.parse_directive (r'#refine a [[1,2],3]')
+ consume <| syntax_pml.map_source (syntax_yaml.unparse_annotation, syntax_ml.parse_commands, False, [(1, [(1, ('', [src_directive, src_annotation ()]))])], (arg_pml (), r'/*@*/'))
+ with pytest.raises Exception:
+ consume <| syntax_yaml.unparse_annotation (src_annotation, None, None, None)
+ consume <| syntax_pml.map_source (syntax_yaml.unparse_annotation, syntax_ml.parse_commands, False, None, (arg_pml (), r'/*@*/'))
+ with pytest.raises Exception:
+ consume <| syntax_yaml.check_annotation (test_anonymous_not_exec, test_anonymous_not_exec, None, False, [], (arg_pml (), r''))
+
+def test_syntax_yaml_check ():
+ def unparse_annotation0 (cmds_generic, cmt_enclose, _, subst_bloc, cmds):
+ yield from syntax_yaml.unparse_annotation (cmt_enclose, cmds_generic, subst_bloc, cmds)
+
+ strip_find_annot1 = (_ -> ((x -> x), {}))
+ src_cmt = cmt_begin -> (src_comment (), ((41, cmt_begin), (41, '\n')))
+ bloc1 = []
+ bloc2 = [(0, [(1, [])])]
+
+ def check_annotation0 ( unparse_annotation = syntax_yaml.unparse_annotation
+ , parse_commands = syntax_yaml.parse_commands
+ , strip_find_annot = test_anonymous_not_exec
+ , group_max = test_anonymous_not_exec
+ , cmt_enclose = src_cmt ('//')
+ , cmds_generic = False
+ , subst_bloc = bloc1
+ , cmds = [('0.8444218515250481', ['1', '41', '0'])]):
+ syntax_yaml.check_annotation0 (unparse_annotation, parse_commands, strip_find_annot, group_max, cmt_enclose, cmds_generic, subst_bloc, cmds)
+
+ def unparse_annotation1 (*args):
+ yield from unparse_annotation0 <*| (True,) + args
+ check_annotation0 ( unparse_annotation = unparse_annotation1
+ , cmt_enclose = src_cmt ('@@')
+ , cmds = ['0', 'CALL', 'append', '21', '6'])
+
+ def unparse_annotation2 (*args):
+ yield from unparse_annotation0 <*| (False,) + args
+ check_annotation0 (unparse_annotation = unparse_annotation2, cmds_generic = True)
+
+ check_annotation0 (strip_find_annot = strip_find_annot1, group_max = (_ -> bloc2))
+
+ def unparse_annotation3 (cmt_enclose, cmds_generic, _, cmds):
+ yield from syntax_yaml.unparse_annotation (cmt_enclose, cmds_generic, bloc1, cmds)
+ check_annotation0 ( unparse_annotation = unparse_annotation3
+ , strip_find_annot = strip_find_annot1
+ , group_max = (_ -> bloc1)
+ , subst_bloc = bloc2)
+
+#
+
+def test_chains1 ():
+ main_promela0 (True, models_chains, 'testsuites_spfreechain01')
+
+def test_chains2 ():
+ # covering: the path without refine_uniform
+ dir0 = models_chains
+ dir1 = './'
+ cwd = os.getcwd ()
+ with tempfile.TemporaryDirectory () as dir_test:
+ os.chdir dir_test
+ def write_unlink0 (fic):
+ toks = (r'-p'
+ r' /*@ export_code \<open>init.c\<close>'
+ r' enclose_file \<open>enclose_1_head.c\<close>'
+ r' \<open>enclose_2_foot.c\<close>'
+ r' refine_generic_file \<open>chains-rfn.yml\<close>'
+ r' */')
+ fic.write (toks.encode ())
+ fic.close ()
+ symlink (cons_cwd dir0, dir1, 'enclose_1_head.c')
+ symlink (cons_cwd dir0, dir1, 'enclose_2_foot.c')
+ os.symlink (cons_cwd dir0 + '../examples/only_generic/chains-rfn.yml', dir1 + 'chains-rfn.yml')
+ fic0 = dir1 + os.path.basename fic.name
+ os.symlink (fic.name, fic0)
+ main_ml_promela0 ( main_ml_promela_arg_model_checker
+ , ((_1, _2) -> _0 -> fic0)
+ , False
+ , dir0
+ , 'testsuites_spfreechain01'
+ , 'testsuites_spfreechain01_no_uniform')
+ testgen.write_unlink (write_unlink0)
+ os.chdir cwd
+
+def test_events ():
+ main_promela_events ('testsuites_validation')
+
+def test_events_exec_all ():
+ main_ml_promela0 ( (_ -> r'-p'
+ r' /*@ model_checker_verifier \<open>spin\<close> \<open>-a\<close>'
+ r' model_checker_compile \<open>gcc\<close> \<open>-DVECTORSZ=4096\<close> \<open>-o\<close> \<open>pan\<close> \<open>pan.c\<close>'
+ r' model_checker_exec_one \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close>'
+ r' model_checker_exec_all \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close> \<open>-e\<close>'
+ r' model_checker_trail \<open>spin\<close> \<open>-p\<close> \<open>-T\<close> \<open>-t\<close> \<open>-k\<close>'
+ r' export_trail_num \<open>1\<close>'
+ r' export_trail_num \<open>4\<close>'
+ r' */')
+ , main_ml_promela_arg_refine
+ , False
+ , models_events
+ , 'testsuites_validation'
+ , 'testsuites_validation_exec_all')
+
+#
+
+def test_fail_fileinput ():
+ fic = 'not_exist_fic'
+ assert not os.path.exists fic
+ consume <| fileinput_input fic
+
+ assert os.path.isdir ('.')
+ consume <| fileinput_input ('.')
+
+def test_fail_mkdir ():
+ def write_unlink0 (fic):
+ fic.close ()
+ testgen.mkdir fic.name
+ testgen.mkdir (fic.name + '/_')
+ testgen.write_unlink write_unlink0
+
+def test_fail_copy1 ():
+ def write_unlink0 (fic1):
+ fic1.write('_'.encode())
+ fic1.close ()
+ testgen.copy_i fic1.name fic1.name
+ def write_unlink1 (fic2):
+ fic2.close ()
+ testgen.copy_i fic1.name fic2.name
+ testgen.write_unlink write_unlink1
+ with tempfile.TemporaryDirectory () as dir_test:
+ dir_test1 = dir_test + '/a'
+ fic2 = dir_test1 + '/' + os.path.basename fic1.name
+ testgen.copy_i (fic1.name, fic2)
+ os.symlink (fic1.name, dir_test1)
+ testgen.copy_i (fic1.name, fic2)
+ testgen.copy_i (dir_test, fic2)
+ testgen.write_unlink write_unlink0
+
+def test_fail_split_arg ():
+ consume <| testgen.split_arg ((_ -> None), [''])
+
+def test_fail_write_promela ():
+ st = testgen.read_eval_print (0, [], False)
+ with pytest.raises Exception:
+ st.write_promela (())
+ with pytest.raises Exception:
+ st.write_promela (st.init_top_elems (list (testgen.fold_prog st.argv), st.argv), a = '')
+
+#
+
+def test_fail_parse_syntax_yaml_refine_generic ():
+ main0 (r' /*@ refine_generic \<open>-\<close>'
+ r' */')
+
+def test_fail_parse_syntax_pml ():
+ main0 (r' -')
+
+def test_fail_command_not_found0 ():
+ main2 (r' /*@ model_checker_verifier \<open>' + not_exist_command + r'\<close>'
+ r' */'
+ r' ltl { true }')
+
+def test_fail_command_not_found1 ():
+ testgen.subprocess_exec (True, False, not_exist_command, [])
+
+def test_fail_command_empty ():
+ main2 (r' /*@ model_checker_verifier'
+ r' */'
+ r' ltl { true }')
+
+def test_fail_arg_missing_param ():
+ main2 ('')
+
+def test_fail_arg_unknown ():
+ main1 (r'--' + not_exist_command)
+
+def test_fail_arg_not_exist_fic ():
+ fic = 'not_exist_fic'
+ assert not os.path.exists fic
+ main1 fic
+
+def test_fail_vectorsz ():
+ main_ml_promela0 ( (_ -> r'-p'
+ r' /*@ model_checker_verifier \<open>spin\<close> \<open>-a\<close>'
+ r' model_checker_compile \<open>gcc\<close> \<open>-o\<close> \<open>pan\<close> \<open>pan.c\<close>'
+ r' model_checker_exec_one \<open>./pan\<close> \<open>-a\<close> \<open>-n\<close>'
+ r' model_checker_trail \<open>spin\<close> \<open>-p\<close> \<open>-T\<close> \<open>-t\<close> \<open>-k\<close>'
+ r' */')
+ , main_ml_promela_arg_refine
+ , False
+ , models_events
+ , 'testsuites_validation'
+ , 'testsuites_validation_vectorsz')
+
+def test_insert_print_non_seq1 ():
+ # covering: print_first (when combined with normal, 'sequence' or 'atomic')
+ # refine_uniform_strip, particularly when there is at least one newline in the refinement code
+ main3 (r' proctype f () { true }'
+ r' proctype g () { { int a = 0; int b = 0 } }'
+ r' proctype h () { atomic { int a = 0; int b = 0 } }'
+ r' /*@ export_code \<open>init.c\<close>'
+ r' refine_uniform_at \<open>f\<close>'
+ r' \<open>'
+ '\n' r'//\<close>'
+ r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+ r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+ r' print_first'
+ r' refine_uniform_strip'
+ r' */'
+ r' init { run f () }')
+
+def test_insert_print_non_seq2 ():
+ # covering: insertion of printf with print_first deactivated (when combined with normal, 'sequence' or 'atomic')
+ main3 (r' proctype f () { true }'
+ r' proctype g () { { int a = 0; int b = 0 } }'
+ r' proctype h () { atomic { int a = 0; int b = 0 } }'
+ r' /*@ export_code \<open>init.c\<close>'
+ r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+ r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+ r' */'
+ r' init { run f () }')
+
+def test_insert_print_non_seq3 ():
+ # covering: insertion of printf with print_first deactivated (when combined with normal, 'sequence' or 'atomic')
+ # no_printf for all proctypes (as it is written in the same line as all proctypes)
+ main3 (r' proctype f () { true }'
+ r' proctype g () { { int a = 0; int b = 0 } }'
+ r' proctype h () { atomic { int a = 0; int b = 0; true } }'
+ r' /*@ export_code \<open>init.c\<close>'
+ r' no_printf'
+ r' refine_uniform_at \<open>g\<close> \<open>//\<close>'
+ r' refine_uniform_at \<open>h\<close> \<open>//\<close>'
+ r' */'
+ r' init { run f () }')
+
+def test_toplevel_constructs ():
+ # covering: the use of different types of constructs at toplevel
+ main3 (r' int a = 0;'
+ r' proctype f () { true }'
+ r' init { true }')
+
+def test_refine_arg_similar ():
+ # covering: refine_uniform_force
+ # the use of similar parameters in proctype and inline
+ main3 (r' int a = 0;'
+ r' proctype f (int a; int a) { true }'
+ r' inline g (b, b) { true }'
+ r' /*@ refine_uniform_force'
+ r' */'
+ r' init { true }')
+
+def test_refine_not_serial_ty ():
+ # covering: not serializable type
+ main0 (r' int a = 0;'
+ r' proctype f (int b) { a = b }'
+ '\n'
+ r' /*@ refine_uniform_at \<open>f\<close> \<open>#refine aa\<close>'
+ r' */'
+ '\n'
+ r' init { run f (1) }'
+ r' ltl { <> ([] (a == 1)) }')
+
+def t_refine_redef_direct (arg):
+ main3 (r' proctype f (int a) { true }'
+ r' inline g (b) { true }' # note: removing this inline will decrease the coverage
+ r' /*@ refine_uniform_at \<open>f\<close>'
+ + arg +
+ r' */'
+ r' init { true }')
+
+def test_refine_redef_direct1 ():
+ # covering: redefinition of directives
+ t_refine_redef_direct (r' \<open>#refine a'
+ '\n' r'#refine a\<close>')
+
+def test_refine_redef_direct2 ():
+ # covering: definition of directives with a different type
+ t_refine_redef_direct (r' \<open>#refine a @{promela [bool]}\<close>')
+
+def test_refine_redef_direct3 ():
+ # covering: redefinition of directives with an array type
+ t_refine_redef_direct (r' \<open>#refine a'
+ '\n' r'#refine a @{promela ["int[8]"]}\<close>')
diff --git a/formal/promela/src/src/tests/test_optional.coco b/formal/promela/src/src/tests/test_optional.coco
new file mode 100644
index 00000000..833cc3c3
--- /dev/null
+++ b/formal/promela/src/src/tests/test_optional.coco
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: BSD-2-Clause
+
+##############################################################################
+ # Test Optional
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ # * Redistributions of source code must retain the above copyright
+ # notice, this list of conditions and the following disclaimer.
+ #
+ # * Redistributions in binary form must reproduce the above
+ # copyright notice, this list of conditions and the following
+ # disclaimer in the documentation and/or other materials provided
+ # with the distribution.
+ #
+ # * Neither the name of the copyright holders nor the names of its
+ # contributors may be used to endorse or promote products derived
+ # from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+from src.tests.library import *
+
+#
+
+def test_events ():
+ main_promela_events ('testsuites_spintrcritical10_1')
+ main_promela_events ('testsuites_spintrcritical10_2')
+ main_promela_events ('testsuites_spintrcritical10_3')
More information about the vc
mailing list