diff --git a/.gitignore b/.gitignore
index 1280fb74b6358d88d5bc8c8d488d981b1569472f..c4204e5ff6e7981f0a1fa70898438580dd785939 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,6 +55,7 @@ autom4te.cache
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
+/tests/spec/preprocess_dos.c
/tests/*/*.opt
/tests/pdg/*.dot
@@ -92,6 +93,8 @@ autom4te.cache
/doc/acsl/
+/doc/aorai/aorai-example.tgz
+/doc/aorai/aorai-example/
/doc/aorai/frama-c-aorai-example.tgz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
diff --git a/Makefile b/Makefile
index 5ff002277f9313e9675975904459bdca593ddb92..9c91110466759f5eb47597511f8bf3d340c9addb 100644
--- a/Makefile
+++ b/Makefile
@@ -2339,7 +2339,29 @@ PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
# that does not contain a 'tests' dir
PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
-ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG)
+ifneq ("$(PTESTS_CONFIG)","")
+GENERATED_TESTS:=tests/spec/preprocess_dos.c
+else
+GENERATED_TESTS:=
+endif
+
+tests/spec/preprocess_dos.c: tests/spec/preprocess_dos.c.in \
+ Makefile share/Makefile.config
+ $(RM) $@
+ $(SED) -e "s|@UNIX2DOS@|$(PP_DOS_UNIX2DOS)|g" \
+ -e "s|@DONTRUN@|$(PP_DOS_DONTRUN)|g" \
+ $< > $@
+ $(CHMOD_RO) $@
+
+ifneq ("$(HAS_UNIX2DOS)","no")
+tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=$(UNIX2DOS)
+tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=
+else
+tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=unix2dos
+tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=DONTRUN: no unix2dos found
+endif
+
+ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG) $(GENERATED_TESTS)
bin/ptests.byte$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
@@ -2351,7 +2373,7 @@ bin/ptests.opt$(EXE): $(PTESTS_SRC)
$(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
-GENERATED+=ptests/ptests_config.ml tests/ptests_config
+GENERATED+=ptests/ptests_config.ml tests/ptests_config $(GENERATED_TESTS)
#######################
# Source distribution #
diff --git a/configure.in b/configure.in
index 284e9f5cea3280ba307aa6962ea4ad07f207f5ca..364940906cb9c955115ee9d81cca18b36168df30 100644
--- a/configure.in
+++ b/configure.in
@@ -657,14 +657,6 @@ REQUIRE_LABLGTK=
USE_LABLGTK=
HAS_LABLGTK=
-# Tool declarations
-####################
-
-DOT=
-REQUIRE_DOT=
-USE_DOT=
-HAS_DOT=
-
### Now plugin declarations
PLUGINS_FORCE_LIST=
@@ -957,6 +949,11 @@ configure_library([LABLGTK],
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
+configure_tool([UNIX2DOS],[unix2dos],
+ [unix2dos not found: you should install tofrodos],no)
+
+plugin_use_external(tests,unix2dos)
+
########################
# Plug-in dependencies #
########################
@@ -974,8 +971,6 @@ EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
-AC_SUBST(DOT)
-AC_SUBST(HAS_DOT)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
diff --git a/nix/default.nix b/nix/default.nix
index 5b892f99684c6fbc9350df9a936c175b73a09bdd..c8e4966f3f26110ec5cfa96fd6629275292a6864 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -2,7 +2,7 @@
{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_05.ocaml", plugins ? { } }:
let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
- [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which] ++ nixPackages ++ opam2nix.build {
+ [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages ++ opam2nix.build {
specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson"
{ name = "coq"; constraint = "=8.11.1"; }
{ name = "why3" ; constraint = "=1.3.1"; }
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 6b316854a46960544bb38a7812c206217cb4304b..3202933a25a1a124dc0eda2ae77bae5763a43943 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -819,13 +819,16 @@ let scan_options dir scan_buffer default =
r := (List.assoc name config_options) dir opt !r
with Not_found ->
lock_eprintf "@[unknown configuration option: %s@\n%!@]" name)
- with Scanf.Scan_failure _ ->
+ with
+ | Scanf.Scan_failure _ ->
if str_string_match end_comment s 0
then raise End_of_file
else ()
+ | End_of_file -> (* ignore blank lines. *) ()
in
try
while true do
+ if Scanf.Scanning.end_of_input scan_buffer then raise End_of_file;
Scanf.bscanf scan_buffer "%s@\n" treat_line
done;
assert false
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 5b485c09b90a8ca699170b6a3e6f649d48946a9a..653d91fad5e4696a2cb7398993aad983048684d5 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -138,6 +138,9 @@ HAS_DOT ?=@HAS_DOT@
HEADACHE ?= headache -c $(FRAMAC_SRC)/headers/headache_config.txt
+UNIX2DOS ?= @UNIX2DOS@
+HAS_UNIX2DOS ?= @HAS_UNIX2DOS@
+
###########################
# Miscellaneous variables #
###########################
diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index ff9d1acb52dd5ff53b0f2045c5f11ade20418656..34ea01b4d6bda1c8a16eb82d54425fc1b82b90ef 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -94,13 +94,14 @@
let content = Buffer.create 80 in
let rec ignore_content () =
let s = input_line file in
- if s <> annot_beg then ignore_content ()
+ if not (Extlib.string_prefix annot_beg s) then ignore_content ()
in
let rec get_annot first =
let s = input_line file in
- if s = annot_end then false, Buffer.contents content
- else if s = annot_end_nl then true, Buffer.contents content
- else if s = annot_end_comment then begin
+ if Extlib.string_prefix annot_end s then false, Buffer.contents content
+ else if Extlib.string_prefix annot_end_nl s then
+ true, Buffer.contents content
+ else if Extlib.string_prefix annot_end_comment s then begin
Buffer.add_char content '\n';
false, Buffer.contents content
end else begin
diff --git a/tests/spec/oracle/preprocess_dos.res.oracle b/tests/spec/oracle/preprocess_dos.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..875a7eae29550f7c2bc14248aa39a15614d7216a
--- /dev/null
+++ b/tests/spec/oracle/preprocess_dos.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/spec/preprocess_dos.c (with preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int a = 0;
+ /*@ assert a ≡ 0; */ ;
+ return a;
+}
+
+
diff --git a/tests/spec/preprocess_dos.c.in b/tests/spec/preprocess_dos.c.in
new file mode 100644
index 0000000000000000000000000000000000000000..abae8ad374b159cd60043731308ac57df1f96498
--- /dev/null
+++ b/tests/spec/preprocess_dos.c.in
@@ -0,0 +1,13 @@
+/* run.config*
+COMMENT: Don't edit directly preprocess_dos.c, but preprocess_dos.c.in
+@DONTRUN@
+OPT: -cpp-command="@PTEST_DIR@/@PTEST_NAME@.sh @UNIX2DOS@ %i %o" -cpp-frama-c-compliant -print
+*/
+
+int main() {
+ int a = 0;
+ /*@
+ assert a == 0;
+ */
+ return a;
+}
diff --git a/tests/spec/preprocess_dos.sh b/tests/spec/preprocess_dos.sh
new file mode 100755
index 0000000000000000000000000000000000000000..a63a982d043b5847b333d4e556892393f97c8a7d
--- /dev/null
+++ b/tests/spec/preprocess_dos.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+gcc -C -E -I. -o $3 $2
+$1 -q $3