fix verify and defaults

src/main/scala/Main.scala

@@ -42,7 +42,7 @@ object Main {
       analysisResultsDot: Option[String]
   )
 
-  def main(args: Iterable[String]): Unit = {
+  def main(args: Array[String]): Unit = {
     val parser = ParserForClass[Config]
     val parsed = parser.constructEither(args.toSeq)
 

src/test/make/lift-directories.mk

@@ -9,7 +9,7 @@ NAME=$(notdir $(shell pwd))
 GIT_ROOT?=$(realpath ../../../../)
 
 GCC ?= aarch64-linux-gnu-gcc
-CLANG ?= clang
+CLANG ?= clang-15
 CC ?= $(GCC)
 #CFLAGS=-fno-pic -fno-plt
 TARGET=aarch64-linux-gnu
@@ -21,7 +21,7 @@ BASIL=$(GIT_ROOT)/target/scala-3.3.1/wptool-boogie-assembly-0.0.1.jar
 C_SOURCE ?=$(realpath $(wildcard *.c))
 SPEC ?=$(realpath $(wildcard *.spec))
 EXTRA_SPEC ?=$(realpath $(wildcard *.bpl))
-BASIL_FLAGS ?= --boogie-use-lambda-stores
+BASIL_FLAGS ?= 
 #BOOGIE_FLAGS=/proverOpt:O:smt.array.extensional=false
 BOOGIE_FLAGS ?= /useArrayAxioms
 

src/test/make/lift.mk

@@ -5,10 +5,14 @@ $(LIFT_ARTEFACTS): a.out
 	$(BAP) a.out -d adt:$(NAME).adt -d bir:$(NAME).bir
 	$(READELF) -s -r -W a.out > $(NAME).relf
 
+
+ifdef $(SPEC) 
+BASIL_SPECARG = --spec $(SPEC) 
+endif
+
 # optional; create basil
 $(NAME).bpl: $(LIFT_ARTEFACTS) $(SPEC) $(BASIL)
-	echo $(BASIL)
-	java -jar $(BASIL) $(BASIL_FLAGS) --adt $(NAME).adt --relf $(NAME).relf -o $(NAME).bpl --spec $(SPEC)
+	java -jar $(BASIL) $(BASIL_FLAGS) --adt $(NAME).adt --relf $(NAME).relf -o $(NAME).bpl $(BASIL_SPECARG)
 
 .PHONY=$(BASIL)
 $(BASIL): 
@@ -27,14 +31,16 @@ recompile: a.out
 $(NAME)_result.txt: $(NAME).bpl $(EXTRA_SPEC)
 	bash -c "time boogie $(NAME).bpl $(EXTRA_SPEC) $(BOOGIE_FLAGS) | tee $(NAME)_result.txt"
 
-cleanall: clean cleanlift cleanbin
+cleanall: clean cleanlift cleanbin cleantest
+
+cleantest: 
+	rm -rf $(NAME).bpl
+	rm -rf $(NAME)_result.txt
 
 cleanbin:
 	rm -rf a.out
 
-clean: cleanbin
-	rm -rf $(NAME).bpl
-	rm -rf $(NAME)_result.txt
+clean: cleanlift cleanbin
 
 cleanlift:
 	rm -rf $(NAME).adt