Fix unittest run.sh and test.sh files.

anmaped · Oct 21, 2024 · 6063362 · 6063362
1 parent 6bb3961
commit 6063362
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 11 deletions.
diff --git a/readme.md b/readme.md
@@ -63,7 +63,7 @@ Alternatively, you may explore the [Documentation](#documentation) section of rm
 ## Building from Git
 
 ![builds and tests workflow](https://github.com/anmaped/rmtld3synth/actions/workflows/builds-and-tests.yml/badge.svg)
-
+![Windows build](https://github.com/anmaped/rmtld3synth/actions/workflows/windows-build.yml/badge.svg)
 
 ### To compile rmtld3synth for Linux and macOS using Opam and Ocaml version >= 4.04.0
 

diff --git a/unittests/integration/run.sh b/unittests/integration/run.sh
@@ -8,6 +8,14 @@ err_report() {
 
 trap 'err_report $LINENO' ERR
 
+function path(){
+if [[ $(uname -s) == CYGWIN* ]];then
+  cygpath -w $1
+else 
+  echo $1
+fi
+}
+
 SCRIPT_PATH="$(dirname -- "${BASH_SOURCE[0]}")"
 SCRIPT_PATH="$(realpath -e -- "$SCRIPT_PATH")"
 echo $SCRIPT_PATH
@@ -16,11 +24,11 @@ OUTPUT_DIR=$SCRIPT_PATH/../../_build_tests/_integration
 mkdir -p $OUTPUT_DIR
 OUTPUT_DIR="$(realpath -e -- "$OUTPUT_DIR")"
 
-rmtld3synth --synth-cpp11 --input-dsl "a" --out-src $OUTPUT_DIR
+rmtld3synth --synth-cpp11 --input-dsl "a" --out-src="$(path "$OUTPUT_DIR")"
 
 cp "$SCRIPT_PATH/sample_monitor.cpp" "$OUTPUT_DIR"
 cp "$SCRIPT_PATH/sample_instrumentation.cpp" "$OUTPUT_DIR"
 
 pushd $OUTPUT_DIR
-gcc -I$SCRIPT_PATH/../../rtmlib2/src/ "sample_monitor.cpp" "sample_instrumentation.cpp" -o test -latomic -fno-rtti -fno-exceptions -DRTMLIB_ENABLE_DEBUG_RMTLD3
+gcc -I"$(path "$SCRIPT_PATH/../../rtmlib2/src/")" "sample_monitor.cpp" "sample_instrumentation.cpp" -o test -latomic -fno-rtti -fno-exceptions -DRTMLIB_ENABLE_DEBUG_RMTLD3
 popd
diff --git a/unittests/test.sh b/unittests/test.sh
@@ -9,6 +9,14 @@ err_report() {
 
 trap 'err_report $LINENO' ERR
 
+function path(){
+if [[ $(uname -s) == CYGWIN* ]];then
+  cygpath -w $1
+else 
+  echo $1
+fi
+}
+
 RED='\033[0;31m'
 GREEN='\033[0;32m'
 NC='\033[0m' # No Color
@@ -220,27 +228,27 @@ declare -a arrayrmtld_sat_expected_result=(
 
   echo "Generating Test Units for Monitor Generation using Ocaml"
 
-  $CMDGENOCAML --input-sexp "(Or (Until 10 (Prop D) (Or (Prop A) (Not (Prop B)))) (LessThan (Duration (Constant 2) (Prop S) ) (FPlus (Constant 3) (Constant 4)) ))" --out-file="$TEST_DIR/mon1.ml"
+  $CMDGENOCAML --input-sexp "(Or (Until 10 (Prop D) (Or (Prop A) (Not (Prop B)))) (LessThan (Duration (Constant 2) (Prop S) ) (FPlus (Constant 3) (Constant 4)) ))" --out-file="$(path "$TEST_DIR/mon1.ml")"
 
-  $CMDGENOCAML --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-file="$TEST_DIR/mon2.ml"
+  $CMDGENOCAML --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-file="$(path "$TEST_DIR/mon2.ml")"
 
-  $CMDGENOCAML --input-latexeq "\always_{< 4} a \rightarrow \eventually_{= 2} b" --out-file="$TEST_DIR/mon3.ml"
+  $CMDGENOCAML --input-latexeq "\always_{< 4} a \rightarrow \eventually_{= 2} b" --out-file="$(path "$TEST_DIR/mon3.ml")"
 
   echo "Generating Test Units for Cpp11"
 
-  $CMDGENCPP --input-sexp "(Or (Until 10 (Prop D) (Or (Prop A) (Not (Prop B)))) (LessThan (Duration (Constant 2) (Prop S) ) (FPlus (Constant 3) (Constant 4)) ))" --out-src="$TEST_DIR/mon1" --verbose 2 >/dev/null 2>&1
+  $CMDGENCPP --input-sexp "(Or (Until 10 (Prop D) (Or (Prop A) (Not (Prop B)))) (LessThan (Duration (Constant 2) (Prop S) ) (FPlus (Constant 3) (Constant 4)) ))" --out-src="$(path "$TEST_DIR/mon1")" --verbose 2 >/dev/null 2>&1
 
-  $CMDGENCPP --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-src="$TEST_DIR/mon2" --verbose 2 >/dev/null 2>&1
+  $CMDGENCPP --input-latexeq "(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-src="$(path "$TEST_DIR/mon2")" --verbose 2 >/dev/null 2>&1
 
-  $CMDGENCPP --input-latexeq "\always_{< 4} a \rightarrow \eventually_{= 2} b" --out-src="$TEST_DIR/mon3" --verbose 2 >/dev/null 2>&1
+  $CMDGENCPP --input-latexeq "\always_{< 4} a \rightarrow \eventually_{= 2} b" --out-src="$(path "$TEST_DIR/mon3")" --verbose 2 >/dev/null 2>&1
 
   # Automatic generation of monitors from a set of formulas
   sample=10 # this sample can be changed
   for ((i = 1; i < ${arrayrmtldlength} + 1; i++)); do
     REP=${arrayrmtld[$i - 1]//b1/$sample}
     REPP=${REP//b2/$sample}
     $CMDSAT --trace-style "tcum" --input-latexeq "$REPP" >$TEST_DIR/cpp/res$i.trace
-    $CMDGENCPP --input-latexeq "$REPP" --out-src="$TEST_DIR/cpp/mon$i" >/dev/null 2>&1
+    $CMDGENCPP --input-latexeq "$REPP" --out-src="$(path "$TEST_DIR/cpp/mon$i")" >/dev/null 2>&1
   done
 
   echo "Generating Unit tests for smtlibv2"
@@ -251,7 +259,7 @@ declare -a arrayrmtld_sat_expected_result=(
     REPP=${REP//b2/$sample}
     $CMDSAT_DEBUG --input-latexeq "$REPP" >$TEST_DIR/res$i.smt2
     $CMDSAT --trace-style "tinterval" --input-latexeq "$REPP" >$TEST_DIR/res$i.trace
-    $CMDGENOCAML --input-latexeq "$REPP" --out-file="$TEST_DIR/res$i.ml"
+    $CMDGENOCAML --input-latexeq "$REPP" --out-file="$(path "$TEST_DIR/res$i.ml")"
   done
 
   echo "Generating the Makefile...."