From 3a8a3e1ff9ae85b87d8f79de1e0b3faa9fa959b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Sun, 5 Mar 2017 23:50:39 +0100 Subject: [PATCH] Modification of compile_sdc_run test script Test script compile_sdc_run: handling of different controller synthesis algorithms. In a test file, put a special comment : (* SDC algorithm *) on a single line, to activate synthesis algorithm "algorithm" for this test file. Examples: (* SDC sB *) (* SDC sS *) (* SDC sS:d={P:D} *) NB: assertions not yet handled. --- test/scripts/compile_sdc_run | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/test/scripts/compile_sdc_run b/test/scripts/compile_sdc_run index 8dde955..68474a6 100755 --- a/test/scripts/compile_sdc_run +++ b/test/scripts/compile_sdc_run @@ -4,7 +4,8 @@ source scripts/config progpath=$1 shift -bzreaxoption="$* --heptc ../${COMPILER_DIR}/${COMPILER} --ctrl2ept ${CTRL2EPT}" +bzreaxoption="$*" +hept_comp_opts="--heptc ../${COMPILER_DIR}/${COMPILER} --ctrl2ept ${CTRL2EPT}" # run the program: no by default run=0 @@ -17,18 +18,24 @@ pushd $checkdir > /dev/null heptprog=`basename $progpath` heptroot=`basename $heptprog .ept` -assert_node=$(eval grep CHECK $heptprog | awk '{ print $3 }') - -if [ -n "$assert_node" ]; then - bzreaxoption="$bzreaxoption --heptc-opts \"-assert $assert_node\"" - run=1 -fi - if grep "node main()" $heptprog >/dev/null; then bzreaxoption="$bzreaxoption main -s" run=1 fi +# assert_node=$(eval grep CHECK $heptprog | awk '{ print $3 }') + +# if [ -n "$assert_node" ]; then +# bzreaxoption="$bzreaxoption --heptc-opts '-assert $assert_node'" +# run=1 +# fi + +algo_sdc=$(eval grep SDC $heptprog | awk '{ print $3 }') +if [ -n "$algo_sdc" ]; then + bzreaxoption="$bzreaxoption -a '$algo_sdc'" +fi + +bzreaxoption="$bzreaxoption $hept_comp_opts" echo $BZREAX $heptprog $bzreaxoption if $BZREAX $heptprog $bzreaxoption; then