Merge branch 'stable/titanium'

04fe5b44 · Allan Blanchard · 4f6dff77 · 70760544 · 04fe5b44 · 04fe5b44
Commit 04fe5b44 authored 4 years ago by Allan Blanchard
--- a/opam/opam
+++ b/opam/opam
@@ -98,7 +98,10 @@ install: [
 ]
 run-test: [
-  [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"]
+  [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] { arch != "ppc64" }
+  # tests are disabled on PPC64 due to floating-point oracle differences
+  # (some ULPs in libc trigonometric functions) and due to the lack of
+  # available hardware to test them locally
 ]
 depends: [
@@ -115,6 +118,7 @@ depends: [
  "conf-graphviz" { post }
  "yojson"
  "why3" { >= "1.3.3" }
+  "conf-time" { with-test }
 ]
 depopts: [

--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -2,7 +2,6 @@
   NOFRAMAC: testing frama-c-script, not frama-c itself
   EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err cd @PTEST_DIR@ && PTESTS_TESTING= ../../bin/frama-c-script make-template result < make_template.input > result/make_template.res 2> result/make_template.err
   EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
-   EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg
   EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err
   EXECNOW: LOG find_fun2.res LOG find_fun2.err bin/frama-c-script find-fun main3 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun2.res 2> @PTEST_DIR@/result/find_fun2.err
   EXECNOW: LOG find_fun3.res LOG find_fun3.err bin/frama-c-script find-fun false_positive @PTEST_DIR@ > @PTEST_DIR@/result/find_fun3.res 2> @PTEST_DIR@/result/find_fun3.err

--- a/tests/fc_script/oracle/flamegraph.err
+++ b/tests/fc_script/oracle/flamegraph.err
--- a/tests/fc_script/oracle/flamegraph.html
+++ b/tests/fc_script/oracle/flamegraph.html
-<!DOCTYPE html>
-<html lang="en">
-  <head>
-    <meta charset="utf-8">
-    <title>Eva Flamegraph</title>
-  </head>
-  <body>
-    <embed src="flamegraph.svg" style="max-width:100%;width:1400px;min-width:1000px">
-  </body>
-</html>
--- a/tests/fc_script/oracle/flamegraph.res
+++ b/tests/fc_script/oracle/flamegraph.res
--- a/tests/misc/pragma-pack.c
+++ b/tests/misc/pragma-pack.c
 /*run.config
  STDOPT: #"-machdep gcc_x86_64 -kernel-msg-key typing:pragma"
-  STDOPT: #"-cpp-command=\"gcc -E -C -I. -m32\" -cpp-frama-c-compliant"
+  STDOPT: #"-machdep gcc_x86_32"
  STDOPT: #"-machdep msvc_x86_64"
 */

--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
 /* run.config*
-   FILTER: sed "s:/[^ ]*/cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::"
+   FILTER: sed "s:/[^ ]*/cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::; s: -m32::"
   OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
   OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
   OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""

--- a/tests/syntax/oracle/cpp-command.0.res.oracle
+++ b/tests/syntax/oracle/cpp-command.0.res.oracle
 [kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [ -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32]
+[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [ -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc]
--- a/tests/syntax/oracle/cpp-command.1.res.oracle
+++ b/tests/syntax/oracle/cpp-command.1.res.oracle
 [kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-%1 = cpp-command.c %2 = TMPDIR/FILE.i %args =  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32
+%1 = cpp-command.c %2 = TMPDIR/FILE.i %args =  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc
--- a/tests/syntax/oracle/cpp-command.4.res.oracle
+++ b/tests/syntax/oracle/cpp-command.4.res.oracle
 [kernel] Preprocessing command:
-  gcc -E -C -I.  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'
+  gcc -E -C -I.  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'