Verified Commit a09deded authored by Julien's avatar Julien
Browse files

[build|test] adding counter-examples and their related error logs

It is important to test that malformed programs are rejected by the
typechecker.
This work starts with a few counter-examples which should fail.
parent 67b2d8f1
Pipeline #142192181 failed with stage
in 9 minutes and 18 seconds
......@@ -66,6 +66,7 @@ all: $(COQ_DIR)/Makefile $(COQ_FILES) all-vo compiler
test: compiler
make -C examples
make -C counter-examples
full: all doc test
......
COMPILER=dune exec --no-print-directory -- ../extraction/albert_comp.exe
ALB=$(wildcard *.alb)
MICH=$(ALB:%.alb=%.tz)
all:$(MICH)
echo:
@echo "COMPILER=\"$(COMPILER)\""
@echo "ALB=\"$(ALB)\""
@echo "MICH=\"$(MICH)\""
%.tz : %.alb
@echo "checking $<";! ( ($(COMPILER) $< 2>&1 ) > $*.log && echo "ERROR Compilation of $< should not succeed" )
clean :
rm -f $(MICH)
def main : { param : int ; storage : int } -> { op : list operation ; storage : int } =
x = amount;
x = "a" ;
y = x;
drop param;
drop x;
drop y;
op = ([] : list operation)
def compare_timestamp : { t1 : timestamp } -> { b : bool } =
carthage_activation = a-dummy-timestamp;
b2 = carthage_activation < current_timestamp;
b = b1 && b2
Syntax error in program at :2:35 when reading token -
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment