Commit 7682c057 authored by Thibault Martin's avatar Thibault Martin
Browse files

Fix itc non-natural loop, update Makefile

parent 086e8fc5
......@@ -100,13 +100,12 @@ help::
QUICK_TARGETS=$(filter-out polarssl gzip124 libmodbus monocypher chrony,$(TARGETS))
all: $(TARGETS)
all-nowp: $(TARGETS)
summary:
frama-c/share/analysis-scripts/summary.py
$(TARGETS):
+$(MAKE) -C $@/.frama-c
+$(MAKE) -C $@/.frama-c ltest-nowp
quick: $(QUICK_TARGETS)
......
# eva is loaded due to 'unroll' annotations
LANNOTFLAGS=-no-autoload-plugins -load-module eva,variadic,postdominators,lannotate -lannot=DUC
LANNOTFLAGS=-no-autoload-plugins -load-module eva,variadic,postdominators,lannotate -lannot=DUC -print-libc
LUNCOVFLAGS=-luncov-wp -wp-prover qed -luncov-timeout 36000
EQ=-lannot-no-clean
NA=-lannot-no-clean-equiv
......@@ -20,12 +21,12 @@ $(1)_NA_Eq: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-log a:$$@ -lannot-o $$(basename $(1))_NA_Eq_labels.c
$(1)_VA: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) $(NO_CLEAN) -lannot-log a:$$@.1 -lannot-o $$(basename $(1))_VA_labels.c
$(RUN_FC) $$(basename $(1))_VA_labels.c $(LOADEVA) $(EVAFLAGS) -luncov-eva -luncov-log a:$$@.2
$(RUN_FC) $$(basename $(1))_VA_labels.c $(LOADEVA) $(EVAFLAGS) -luncov-eva -luncov-log a:$$@.2
cat $$@.1 $$@.2 > $$@
rm -f $$@.1 $$@.2
$(1)_WP: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) $(NO_CLEAN) -lannot-log a:$$@.1 -lannot-o $$(basename $(1))_WP_labels.c
$(RUN_FC) $$(basename $(1))_WP_labels.c $(LOADWP) -luncov-wp -wp-prover qed -luncov-log a:$$@.2
$(RUN_FC) $$(basename $(1))_WP_labels.c $(LOADWP) $(LUNCOVFLAGS) -luncov-log a:$$@.2
cat $$@.1 $$@.2 > $$@
rm -f $$@.1 $$@.2
$(1)_NA_Eq_VA: $(2)
......@@ -35,11 +36,17 @@ $(1)_NA_Eq_VA: $(2)
rm -f $$@.1 $$@.2
$(1)_NA_Eq_WP: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-log a:$$@.1 -lannot-o $$(basename $(1))_NA_Eq_WP_labels.c
$(RUN_FC) $$(basename $(1))_NA_Eq_WP_labels.c $(LOADWP) -luncov-wp -wp-prover qed -luncov-log a:$$@.2
$(RUN_FC) $$(basename $(1))_NA_Eq_WP_labels.c $(LOADWP) $(LUNCOVFLAGS) -luncov-log a:$$@.2
cat $$@.1 $$@.2 > $$@
rm -f $$@.1 $$@.2
TARGETS+=$(1)_Candidate $(1)_NA $(1)_NA_Eq $(1)_Eq $(1)_VA $(1)_WP $(1)_NA_Eq_VA $(1)_NA_Eq_WP
$(1)_NA_Eq_VA_WP: $(2)
$(RUN_FC) $$^ $(LANNOTFLAGS) -lannot-log a:$$@.1 -lannot-o $$(basename $(1))_NA_Eq_VA_WP_labels.c
$(RUN_FC) $$(basename $(1))_NA_Eq_VA_WP_labels.c $(LOADEVA) $(EVAFLAGS) -luncov-eva -luncov-log a:$$@.2
$(RUN_FC) $$(basename $(1))_NA_Eq_VA_WP_labels.c $(LOADWP) $(LUNCOVFLAGS) -luncov-log a:$$@.3
cat $$@.1 $$@.2 $$@.3 > $$@
rm -f $$@.1 $$@.2 $$@.3
TARGETS+=$(1)_Candidate $(1)_NA $(1)_NA_Eq $(1)_Eq $(1)_VA $(1)_WP $(1)_NA_Eq_VA $(1)_NA_Eq_WP $(1)_NA_Eq_VA_WP
endef
filter-out-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
......@@ -48,6 +55,7 @@ filter-in-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),$(v),))
ltest: $$(TARGETS)
ltest-wp: $$(call filter-in-substring,_WP,$$(TARGETS))
ltest-vawp: $$(call filter-in-substring,_VA_WP,$$(TARGETS))
ltest-nowp: $$(call filter-out-substring,_WP,$$(TARGETS))
clean::
......
......@@ -278,8 +278,7 @@ void null_pointer_016()
int flag=0,i,j;
null_pointer_016_gbl_doubleptr=NULL;
goto label;
// Frama-C/Eva: applied patch from https://github.com/dwightguth/itc-benchmarks
label2:
if(null_pointer_016_func_001(flag)==ZERO)
{
for(i=0;i<10;i++)
......@@ -300,7 +299,6 @@ label:
{
null_pointer_016_func_002();
}
goto label2;
}
/*
......
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