Commit 3e3bb6a5 authored by MARCHE Claude's avatar MARCHE Claude

jessie3: more robust generation of ptests_config

parent dd52585e
FRAMAC_TOPLEVEL = @FRAMAC@
FRAMAC_SHARE = @FRAMAC_SHARE@
FRAMAC_LIBDIR = @FRAMAC_LIBDIR@
PLUGIN_NAME = Jessie3
MODULES = literals ACSLtoWhy3 register
TESTS = basic demo
WHYLIB = ../../lib/why3
......@@ -41,10 +43,20 @@ test.opt:
frama-c -load-module ./Jessie3.cmxs -jessie3 tests/basic/forty-two.c
# -kernel-debug 2
tests::
tests:: tests/ptests_config
time -p ptests.opt
grep 'Task\|Ergo' tests/basic/result/*.res.log tests/demo/result/*.res.log
tests/ptests_config: Makefile
rm -rf tests/ptests_config
echo "DEFAULT_SUITES="$(TESTS) > tests/ptests_config
echo "TOPLEVEL_PATH="$(FRAMAC_TOPLEVEL) >> tests/ptests_config
echo "FRAMAC_SHARE="$(FRAMAC_SHARE) >> tests/ptests_config
echo "FRAMAC_PLUGIN=." >> tests/ptests_config
echo "FRAMAC_PLUGIN_GUI=./gui" >> tests/ptests_config
echo "FRAMAC_LIB="$(FRAMAC_LIBDIR) >> tests/ptests_config
echo "OCAMLRUNPARAM=" >> tests/ptests_config
chmod a-w tests/ptests_config
clean:
rm -f $(addsuffix .cmo, $(MODULES))
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/call.c"
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/call.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f
[jessie3] created program function f (738)
[jessie3] created program function f (67)
[jessie3] processing function g
[jessie3] created program function g (743)
[jessie3] created program function g (72)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 2 function(s)
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.Bool *)
(* use why3.Unit *)
(* use why3.Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use map.Map *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
goal WP_parameter_f :
forall x:int32.
0 <= to_int x /\ to_int x <= 1000 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 1 &&
(forall o1:int32.
to_int o1 = 1 ->
in_bounds (to_int x + to_int o1) &&
(forall o2:int32.
to_int o2 = (to_int x + to_int o1) ->
(forall us_retres:int32.
us_retres = o2 -> (to_int us_retres - to_int x) > 0))))
goal WP_parameter_g :
forall x:int32.
10 <= to_int x /\ to_int x <= 100 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 1 &&
(forall o1:int32.
to_int o1 = 1 ->
in_bounds (to_int x - to_int o1) &&
(forall o2:int32.
to_int o2 = (to_int x - to_int o1) ->
(0 <= to_int o2 /\ to_int o2 <= 1000) &&
(forall o3:int32.
(to_int o3 - to_int o2) > 0 ->
(forall y:int32. y = o3 -> (to_int y - to_int x) >= 0)))))
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Valid, Valid, Valid
[jessie3] failure: Exception raised during translation to Why3:
Ident f is not yet declared
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.AbortFatal("jessie3")
[kernel] Current source was: tests/basic/call.c:16
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/rec.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] creating logic symbol 68 (sum_upto)
[jessie3] processing function sum
[jessie3] created program function sum (70)
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "stmt Goto")
[kernel] Current source was: tests/basic/rec.c:36
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
This diff is collapsed.
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/f91.c (with preprocessing)
[kernel] user error: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
[kernel] Frama-C aborted: invalid user input.
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/flag.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "global: GEnumTag")
[kernel] Current source was: tests/demo/flag.c:57
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/mccarthy.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f91
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "named behaviors")
[kernel] Current source was: tests/demo/mccarthy.c:15
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/selection_sort.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "Dfun_or_pred with labels")
[kernel] Current source was: tests/demo/selection_sort.c:56
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/sparse_array.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "global: GType")
[kernel] Current source was: tests/demo/sparse_array.c:102
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/triangle.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "ctype TFun")
[kernel] Current source was: tests/demo/triangle.c:27
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
DEFAULT_SUITES= basic demo
TOPLEVEL_PATH=/usr/local/bin/frama-c
FRAMAC_SHARE=/usr/local/share/frama-c
FRAMAC_PLUGIN=.
FRAMAC_PLUGIN_GUI=./gui
FRAMAC_LIB=/usr/local/lib/frama-c
OCAMLRUNPARAM=
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